Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Metrology.Z

Contents

The Z datatype
- Defunctionalization symbols (these can be ignored)
Conversions
Type-level operations
- Arithmetic
- Comparisons
Synonyms for certain numbers
Deprecated synonyms

Description

This module defines a datatype and operations to represent type-level integers. Though it's defined as part of the units package, it may be useful beyond dimensional analysis. If you have a compelling non-units use of this package, please let me (Richard, rae at cs.brynmawr.edu) know.

Synopsis

data Z
- = Zero
- | S Z
- | P Z
data family Sing (a :: k) :: Type
type SZ = (Sing :: Z -> Type)
type ZeroSym0 = Zero
data SSym0 :: (~>) Z Z
type SSym1 (t6989586621679083877 :: Z) = S t6989586621679083877
data PSym0 :: (~>) Z Z
type PSym1 (t6989586621679083879 :: Z) = P t6989586621679083879
zToInt :: Z -> Int
szToInt :: Sing (z :: Z) -> Int
type family Succ (z :: Z) :: Z where ...
type family Pred (z :: Z) :: Z where ...
type family Negate (z :: Z) :: Z where ...
type family (a :: Z) #+ (b :: Z) :: Z where ...
type family (a :: Z) #- (b :: Z) :: Z where ...
type family (a :: Z) #* (b :: Z) :: Z where ...
type family (a :: Z) #/ (b :: Z) :: Z where ...
sSucc :: Sing z -> Sing (Succ z)
sPred :: Sing z -> Sing (Pred z)
sNegate :: Sing z -> Sing (Negate z)
type family (a :: Z) < (b :: Z) :: Bool where ...
type family NonNegative z :: Constraint where ...
type One = S Zero
type Two = S One
type Three = S Two
type Four = S Three
type Five = S Four
type MOne = P Zero
type MTwo = P MOne
type MThree = P MTwo
type MFour = P MThree
type MFive = P MFour
sZero :: Sing Zero
sOne :: Sing (S Zero)
sTwo :: Sing (S (S Zero))
sThree :: Sing (S (S (S Zero)))
sFour :: Sing (S (S (S (S Zero))))
sFive :: Sing (S (S (S (S (S Zero)))))
sMOne :: Sing (P Zero)
sMTwo :: Sing (P (P Zero))
sMThree :: Sing (P (P (P Zero)))
sMFour :: Sing (P (P (P (P Zero))))
sMFive :: Sing (P (P (P (P (P Zero)))))
pZero :: Sing Zero
pOne :: Sing (S Zero)
pTwo :: Sing (S (S Zero))
pThree :: Sing (S (S (S Zero)))
pFour :: Sing (S (S (S (S Zero))))
pFive :: Sing (S (S (S (S (S Zero)))))
pMOne :: Sing (P Zero)
pMTwo :: Sing (P (P Zero))
pMThree :: Sing (P (P (P Zero)))
pMFour :: Sing (P (P (P (P Zero))))
pMFive :: Sing (P (P (P (P (P Zero)))))
pSucc :: Sing z -> Sing (Succ z)
pPred :: Sing z -> Sing (Pred z)

The `Z` datatype

data Z Source #

The datatype for type-level integers.

Constructors

Zero
S Z
P Z

Instances

Eq Z Source #
Instance details Defined in Data.Metrology.Z Methods (==) :: Z -> Z -> Bool # (/=) :: Z -> Z -> Bool #
SEq Z => SEq Z Source #
Instance details Defined in Data.Metrology.Z Methods (%==) :: Sing a -> Sing b -> Sing (a == b) # (%/=) :: Sing a -> Sing b -> Sing (a /= b) #
PEq Z Source #
Instance details Defined in Data.Metrology.Z Associated Types type x == y :: Bool # type x /= y :: Bool #
SDecide Z => SDecide Z Source #
Instance details Defined in Data.Metrology.Z Methods (%~) :: Sing a -> Sing b -> Decision (a :~: b) #
SingKind Z Source #
Instance details Defined in Data.Metrology.Z Associated Types type Demote Z = (r :: Type) # Methods fromSing :: Sing a -> Demote Z # toSing :: Demote Z -> SomeSing Z #
SingI Zero Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing Zero #
SingI n => SingI (S n :: Z) Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing (S n) #
SingI n => SingI (P n :: Z) Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing (P n) #
SuppressUnusedWarnings PSym0 Source #
Instance details Defined in Data.Metrology.Z Methods suppressUnusedWarnings :: () #
SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Data.Metrology.Z Methods suppressUnusedWarnings :: () #
SingI PSym0 Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing PSym0 #
SingI SSym0 Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing SSym0 #
SingI (TyCon1 S) Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing (TyCon1 S) #
SingI (TyCon1 P) Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing (TyCon1 P) #
data Sing (a :: Z) Source #
Instance details Defined in Data.Metrology.Z data Sing (a :: Z) where SZero :: forall (a :: Z). Sing Zero SS :: forall (a :: Z) (n :: Z). Sing n -> Sing (S n) SP :: forall (a :: Z) (n :: Z). Sing n -> Sing (P n)
type Demote Z Source #
Instance details Defined in Data.Metrology.Z type Demote Z = Z
type (x :: Z) /= (y :: Z) Source #
Instance details Defined in Data.Metrology.Z type (x :: Z) /= (y :: Z) = Not (x == y)
type (a :: Z) == (b :: Z) Source #
Instance details Defined in Data.Metrology.Z type (a :: Z) == (b :: Z)
type Apply PSym0 (t6989586621679083879 :: Z) Source #
Instance details Defined in Data.Metrology.Z type Apply PSym0 (t6989586621679083879 :: Z) = P t6989586621679083879
type Apply SSym0 (t6989586621679083877 :: Z) Source #
Instance details Defined in Data.Metrology.Z type Apply SSym0 (t6989586621679083877 :: Z) = S t6989586621679083877

data family Sing (a :: k) :: Type #

The singleton kind-indexed data family.

Instances

data Sing (a :: Bool)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Bool) where SFalse :: forall (a :: Bool). Sing False STrue :: forall (a :: Bool). Sing True
data Sing (a :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Ordering) where SLT :: forall (a :: Ordering). Sing LT SEQ :: forall (a :: Ordering). Sing EQ SGT :: forall (a :: Ordering). Sing GT
data Sing (n :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Nat) where SNat :: forall (n :: Nat). KnownNat n => Sing n
data Sing (n :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal data Sing (n :: Symbol) where SSym :: forall (n :: Symbol). KnownSymbol n => Sing n
data Sing (a :: ())
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: ()) where STuple0 :: forall (a :: ()). Sing ()
data Sing (a :: Z) Source #
Instance details Defined in Data.Metrology.Z data Sing (a :: Z) where SZero :: forall (a :: Z). Sing Zero SS :: forall (a :: Z) (n :: Z). Sing n -> Sing (S n) SP :: forall (a :: Z) (n :: Z). Sing n -> Sing (P n)
data Sing (a :: Void)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: All) where SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)
data Sing (a :: Any)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: Any) where SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)
data Sing (b :: [a])
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: [a]) where SNil :: forall a (b :: [a]). Sing ([] :: [a]) SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)
data Sing (b :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Maybe a) where SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a) SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)
data Sing (b :: Min a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Min a) where SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)
data Sing (b :: Max a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Max a) where SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)
data Sing (a :: WrappedMonoid m)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)
data Sing (b :: Option a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Option a) where SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)
data Sing (b :: Identity a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: Identity a) where SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)
data Sing (b :: First a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: First a) where SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)
data Sing (b :: Last a)
Instance details Defined in Data.Singletons.Prelude.Monoid data Sing (b :: Last a) where SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)
data Sing (b :: Dual a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Dual a) where SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)
data Sing (b :: Sum a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Sum a) where SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)
data Sing (b :: Product a)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (b :: Product a) where SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)
data Sing (b :: Down a)
Instance details Defined in Data.Singletons.Prelude.Ord data Sing (b :: Down a) where SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)
data Sing (b :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (b :: NonEmpty a) where (:%\|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :\| n2)
data Sing (b :: Endo a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: Endo a) where SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)
data Sing (b :: MaxInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MaxInternal a) where SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)
data Sing (b :: MinInternal a)
Instance details Defined in Data.Singletons.Prelude.Foldable data Sing (b :: MinInternal a) where SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)
data Sing (c :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: Either a b) where SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b) SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)
data Sing (c :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (c :: (a, b)) where STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)
data Sing (c :: Arg a b)
Instance details Defined in Data.Singletons.Prelude.Semigroup data Sing (c :: Arg a b) where SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)
newtype Sing (f :: k1 ~> k2)
Instance details Defined in Data.Singletons.Internal newtype Sing (f :: k1 ~> k2) = SLambda { applySing :: forall (t :: k1). Sing t -> Sing (f @@ t) }
data Sing (b :: StateL s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateL s a) where SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)
data Sing (b :: StateR s a)
Instance details Defined in Data.Singletons.Prelude.Traversable data Sing (b :: StateR s a) where SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)
data Sing (d :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (d :: (a, b, c)) where STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)
data Sing (c :: Const a b)
Instance details Defined in Data.Singletons.Prelude.Const data Sing (c :: Const a b) where SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)
data Sing (e :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (e :: (a, b, c, d)) where STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)
data Sing (f :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (f :: (a, b, c, d, e)) where STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)
data Sing (g :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (g :: (a, b, c, d, e, f)) where STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)
data Sing (h :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (h :: (a, b, c, d, e, f, g)) where STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

type SZ = (Sing :: Z -> Type) Source #

Defunctionalization symbols (these can be ignored)

type ZeroSym0 = Zero Source #

data SSym0 :: (~>) Z Z Source #

Instances

SuppressUnusedWarnings SSym0 Source #
Instance details Defined in Data.Metrology.Z Methods suppressUnusedWarnings :: () #
SingI SSym0 Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing SSym0 #
type Apply SSym0 (t6989586621679083877 :: Z) Source #
Instance details Defined in Data.Metrology.Z type Apply SSym0 (t6989586621679083877 :: Z) = S t6989586621679083877

type SSym1 (t6989586621679083877 :: Z) = S t6989586621679083877 Source #

data PSym0 :: (~>) Z Z Source #

Instances

SuppressUnusedWarnings PSym0 Source #
Instance details Defined in Data.Metrology.Z Methods suppressUnusedWarnings :: () #
SingI PSym0 Source #
Instance details Defined in Data.Metrology.Z Methods sing :: Sing PSym0 #
type Apply PSym0 (t6989586621679083879 :: Z) Source #
Instance details Defined in Data.Metrology.Z type Apply PSym0 (t6989586621679083879 :: Z) = P t6989586621679083879

type PSym1 (t6989586621679083879 :: Z) = P t6989586621679083879 Source #

Conversions

zToInt :: Z -> Int Source #

Convert a Z to an Int

szToInt :: Sing (z :: Z) -> Int Source #

Convert a singleton Z to an Int.

Type-level operations

Arithmetic

type family Succ (z :: Z) :: Z where ... Source #

Add one to an integer

Equations

Succ Zero = S Zero
Succ (P z) = z
Succ (S z) = S (S z)

type family Pred (z :: Z) :: Z where ... Source #

Subtract one from an integer

Equations

Pred Zero = P Zero
Pred (P z) = P (P z)
Pred (S z) = z

type family Negate (z :: Z) :: Z where ... Source #

Negate an integer

Equations

Negate Zero = Zero
Negate (S z) = P (Negate z)
Negate (P z) = S (Negate z)

type family (a :: Z) #+ (b :: Z) :: Z where ... infixl 6 Source #

Add two integers

Equations

Zero #+ z = z
(S z1) #+ (S z2) = S (S (z1 #+ z2))
(S z1) #+ Zero = S z1
(S z1) #+ (P z2) = z1 #+ z2
(P z1) #+ (S z2) = z1 #+ z2
(P z1) #+ Zero = P z1
(P z1) #+ (P z2) = P (P (z1 #+ z2))

type family (a :: Z) #- (b :: Z) :: Z where ... infixl 6 Source #

Subtract two integers

Equations

z #- Zero = z
(S z1) #- (S z2) = z1 #- z2
Zero #- (S z2) = P (Zero #- z2)
(P z1) #- (S z2) = P (P (z1 #- z2))
(S z1) #- (P z2) = S (S (z1 #- z2))
Zero #- (P z2) = S (Zero #- z2)
(P z1) #- (P z2) = z1 #- z2

type family (a :: Z) #* (b :: Z) :: Z where ... infixl 7 Source #

Multiply two integers

Equations

Zero #* z = Zero
(S z1) #* z2 = (z1 #* z2) #+ z2
(P z1) #* z2 = (z1 #* z2) #- z2

type family (a :: Z) #/ (b :: Z) :: Z where ... Source #

Divide two integers

Equations

Zero #/ b = Zero
a #/ (P b') = Negate (a #/ Negate (P b'))
a #/ b = ZDiv b b a

sSucc :: Sing z -> Sing (Succ z) Source #

Add one to a singleton Z.

sPred :: Sing z -> Sing (Pred z) Source #

Subtract one from a singleton Z.

sNegate :: Sing z -> Sing (Negate z) Source #

Negate a singleton Z.

Comparisons

type family (a :: Z) < (b :: Z) :: Bool where ... Source #

Less-than comparison

Equations

Zero < Zero = False
Zero < (S n) = True
Zero < (P n) = False
(S n) < Zero = False
(S n) < (S n') = n < n'
(S n) < (P n') = False
(P n) < Zero = True
(P n) < (S n') = True
(P n) < (P n') = n < n'

type family NonNegative z :: Constraint where ... Source #

Check if a type-level integer is in fact a natural number

Equations

NonNegative Zero = ()
NonNegative (S z) = ()

Synonyms for certain numbers

type One = S Zero Source #

type Two = S One Source #

type Three = S Two Source #

type Four = S Three Source #

type Five = S Four Source #

type MOne = P Zero Source #

type MTwo = P MOne Source #

type MThree = P MTwo Source #

type MFour = P MThree Source #

type MFive = P MFour Source #

sZero :: Sing Zero Source #

This is the singleton value representing Zero at the term level and at the type level, simultaneously. Used for raising units to powers.

sOne :: Sing (S Zero) Source #

sTwo :: Sing (S (S Zero)) Source #

sThree :: Sing (S (S (S Zero))) Source #

sFour :: Sing (S (S (S (S Zero)))) Source #

sFive :: Sing (S (S (S (S (S Zero))))) Source #

sMOne :: Sing (P Zero) Source #

sMTwo :: Sing (P (P Zero)) Source #

sMThree :: Sing (P (P (P Zero))) Source #

sMFour :: Sing (P (P (P (P Zero)))) Source #

sMFive :: Sing (P (P (P (P (P Zero))))) Source #

Deprecated synonyms

pZero :: Sing Zero Source #