Data.Metrology.Z

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.

The Z datatype

data Z

The datatype for type-level integers.

Constructors

Zero

S Z

P Z

Instances

Eq Z

Defined in Data.Metrology.Z

Methods

(==) :: Z -> Z -> Bool

(/=) :: Z -> Z -> Bool

SEq Z => SEq Z

Defined in Data.Metrology.Z

Methods

(%==) :: Sing a -> Sing b -> Sing (a == b)

(%/=) :: Sing a -> Sing b -> Sing (a /= b)

PEq Z

Defined in Data.Metrology.Z

Associated Types

type x == y :: Bool

type x /= y :: Bool

SDecide Z => SDecide Z

Defined in Data.Metrology.Z

Methods

(%~) :: Sing a -> Sing b -> Decision (a :~: b)

SingKind Z

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

Defined in Data.Metrology.Z

Methods

sing :: Sing Zero

SingI n => SingI (S n :: Z)

Defined in Data.Metrology.Z

Methods

sing :: Sing (S n)

SingI n => SingI (P n :: Z)

Defined in Data.Metrology.Z

Methods

sing :: Sing (P n)

SuppressUnusedWarnings PSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SuppressUnusedWarnings SSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SingI PSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing PSym0

SingI SSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing SSym0

SingI (TyCon1 S)

Defined in Data.Metrology.Z

Methods

sing :: Sing (TyCon1 S)

SingI (TyCon1 P)

Defined in Data.Metrology.Z

Methods

sing :: Sing (TyCon1 P)

data Sing (a :: Z)

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

Defined in Data.Metrology.Z

type Demote Z = Z

type (x :: Z) /= (y :: Z)

Defined in Data.Metrology.Z

type (x :: Z) /= (y :: Z) = Not (x == y)

type (a :: Z) == (b :: Z)

Defined in Data.Metrology.Z

type (a :: Z) == (b :: Z)

type Apply PSym0 (t6989586621679083713 :: Z)

Defined in Data.Metrology.Z

type Apply PSym0 (t6989586621679083713 :: Z) = P t6989586621679083713

type Apply SSym0 (t6989586621679083711 :: Z)

Defined in Data.Metrology.Z

type Apply SSym0 (t6989586621679083711 :: Z) = S t6989586621679083711

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

The singleton kind-indexed data family.

Instances

data Sing (a :: Bool)

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)

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)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Z)

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)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

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)

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])

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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)

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))

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)

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)

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)

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)

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))

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)

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))

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))

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))

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))

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)

Defunctionalization symbols (these can be ignored)

type ZeroSym0 = Zero

data SSym0 :: (~>) Z Z

Instances

SuppressUnusedWarnings SSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SingI SSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing SSym0

type Apply SSym0 (t6989586621679083711 :: Z)

Defined in Data.Metrology.Z

type Apply SSym0 (t6989586621679083711 :: Z) = S t6989586621679083711

type SSym1 (t6989586621679083711 :: Z) = S t6989586621679083711

data PSym0 :: (~>) Z Z

Instances

SuppressUnusedWarnings PSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SingI PSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing PSym0

type Apply PSym0 (t6989586621679083713 :: Z)

Defined in Data.Metrology.Z

type Apply PSym0 (t6989586621679083713 :: Z) = P t6989586621679083713

type PSym1 (t6989586621679083713 :: Z) = P t6989586621679083713

Conversions

zToInt :: Z -> Int

Convert a Z to an Int

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

Convert a singleton Z to an Int.

Type-level operations

Arithmetic

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

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 ...

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 ...

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

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

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

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 ...

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)

Add one to a singleton Z.

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

Subtract one from a singleton Z.

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

Negate a singleton Z.

Comparisons

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

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 ...

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

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

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)

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)))))

Deprecated synonyms

pZero :: Sing Zero

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pOne :: Sing (S Zero)

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pTwo :: Sing (S (S Zero))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pThree :: Sing (S (S (S Zero)))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFour :: Sing (S (S (S (S Zero))))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pFive :: Sing (S (S (S (S (S Zero)))))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMOne :: Sing (P Zero)

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMTwo :: Sing (P (P Zero))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMThree :: Sing (P (P (P Zero)))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFour :: Sing (P (P (P (P Zero))))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pMFive :: Sing (P (P (P (P (P Zero)))))

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pSucc :: Sing z -> Sing (Succ z)

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.

pPred :: Sing z -> Sing (Pred z)

Deprecated: The singleton prefix is changing from p to s. The p versions will be removed in a future release.