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

(%==) :: forall (a :: Z) (b :: Z). Sing a -> Sing b -> Sing (a == b)

(%/=) :: forall (a :: Z) (b :: Z). 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

(%~) :: forall (a :: Z) (b :: Z). Sing a -> Sing b -> Decision (a :~: b)

SingKind Z

Defined in Data.Metrology.Z

Associated Types

type Demote Z = (r :: Type)

Methods

fromSing :: forall (a :: Z). Sing a -> Demote Z

toSing :: Demote Z -> SomeSing Z

SDecide Z => TestCoercion SZ

Defined in Data.Metrology.Z

Methods

testCoercion :: forall (a :: k) (b :: k). SZ a -> SZ b -> Maybe (Coercion a b)

SDecide Z => TestEquality SZ

Defined in Data.Metrology.Z

Methods

testEquality :: forall (a :: k) (b :: k). SZ a -> SZ b -> Maybe (a :~: b)

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

type Sing

Defined in Data.Metrology.Z

type Sing = SZ

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 (a6989586621679063794 :: Z)

Defined in Data.Metrology.Z

type Apply PSym0 (a6989586621679063794 :: Z) = PSym1 a6989586621679063794

type Apply SSym0 (a6989586621679063792 :: Z)

Defined in Data.Metrology.Z

type Apply SSym0 (a6989586621679063792 :: Z) = SSym1 a6989586621679063792

type family Sing :: k -> Type

The singleton kind-indexed type family.

Instances

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SBool

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SOrdering

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SNat

type Sing

Defined in Data.Singletons.TypeLits.Internal

type Sing = SSymbol

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple0

type Sing

Defined in Data.Metrology.Z

type Sing = SZ

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SVoid

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAll

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SAny

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SList :: [a] -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SMaybe :: Maybe a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMin :: Min a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SMax :: Max a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SWrappedMonoid :: WrappedMonoid m -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SOption :: Option a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SIdentity :: Identity a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SFirst :: First a -> Type

type Sing

Defined in Data.Singletons.Prelude.Monoid

type Sing = SLast :: Last a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SDual :: Dual a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SSum :: Sum a -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup.Internal

type Sing = SProduct :: Product a -> Type

type Sing

Defined in Data.Singletons.Prelude.Ord

type Sing = SDown :: Down a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SNonEmpty :: NonEmpty a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SEndo :: Endo a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SMaxInternal :: MaxInternal a -> Type

type Sing

Defined in Data.Singletons.Prelude.Foldable

type Sing = SMinInternal :: MinInternal a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = SEither :: Either a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple2 :: (a, b) -> Type

type Sing

Defined in Data.Singletons.Prelude.Semigroup

type Sing = SArg :: Arg a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Proxy

type Sing = SProxy :: Proxy t -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons.Internal

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons.Prelude.Traversable

type Sing = SStateL :: StateL s a -> Type

type Sing

Defined in Data.Singletons.Prelude.Traversable

type Sing = SStateR :: StateR s a -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple3 :: (a, b, c) -> Type

type Sing

Defined in Data.Singletons.Prelude.Const

type Sing = SConst :: Const a b -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple4 :: (a, b, c, d) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple5 :: (a, b, c, d, e) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple6 :: (a, b, c, d, e, f) -> Type

type Sing

Defined in Data.Singletons.Prelude.Instances

type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SZ :: Z -> Type where

Constructors

SZero :: SZ (Zero :: Z)

SS :: forall (n :: Z). (Sing n) -> SZ (S n :: Z)

SP :: forall (n :: Z). (Sing n) -> SZ (P n :: Z)

Instances

SDecide Z => TestCoercion SZ

Defined in Data.Metrology.Z

Methods

testCoercion :: forall (a :: k) (b :: k). SZ a -> SZ b -> Maybe (Coercion a b)

SDecide Z => TestEquality SZ

Defined in Data.Metrology.Z

Methods

testEquality :: forall (a :: k) (b :: k). SZ a -> SZ b -> Maybe (a :~: b)

Defunctionalization symbols (these can be ignored)

type ZeroSym0 = Zero :: Z

data SSym0 a6989586621679063792

Instances

SuppressUnusedWarnings SSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SingI SSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing SSym0

type Apply SSym0 (a6989586621679063792 :: Z)

Defined in Data.Metrology.Z

type Apply SSym0 (a6989586621679063792 :: Z) = SSym1 a6989586621679063792

type SSym1 (a6989586621679063792 :: Z) = S a6989586621679063792 :: Z

data PSym0 a6989586621679063794

Instances

SuppressUnusedWarnings PSym0

Defined in Data.Metrology.Z

Methods

suppressUnusedWarnings :: ()

SingI PSym0

Defined in Data.Metrology.Z

Methods

sing :: Sing PSym0

type Apply PSym0 (a6989586621679063794 :: Z)

Defined in Data.Metrology.Z

type Apply PSym0 (a6989586621679063794 :: Z) = PSym1 a6989586621679063794

type PSym1 (a6989586621679063794 :: Z) = P a6989586621679063794 :: Z

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 :: SZ '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 :: SZ ('S 'Zero)

sTwo :: SZ ('S ('S 'Zero))

sThree :: SZ ('S ('S ('S 'Zero)))

sFour :: SZ ('S ('S ('S ('S 'Zero))))

sFive :: SZ ('S ('S ('S ('S ('S 'Zero)))))

sMOne :: SZ ('P 'Zero)

sMTwo :: SZ ('P ('P 'Zero))

sMThree :: SZ ('P ('P ('P 'Zero)))

sMFour :: SZ ('P ('P ('P ('P 'Zero))))

sMFive :: SZ ('P ('P ('P ('P ('P 'Zero)))))

Deprecated synonyms

pZero :: SZ 'Zero

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

pOne :: SZ ('S 'Zero)

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

pTwo :: SZ ('S ('S 'Zero))

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

pThree :: SZ ('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 :: SZ ('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 :: SZ ('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 :: SZ ('P 'Zero)

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

pMTwo :: SZ ('P ('P 'Zero))

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

pMThree :: SZ ('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 :: SZ ('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 :: SZ ('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 :: forall (z :: Z). SZ z -> SZ (Succ z)

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

pPred :: forall (z :: Z). SZ z -> SZ (Pred z)

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