Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.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, eir at cis.upenn.edu) know.

Synopsis

The `Z` datatype

data Z Source

The datatype for type-level integers.

Constructors

Zero
S Z
P Z

Instances

Eq Z
SingI Z Zero
SEq Z (KProxy Z)
PEq Z (KProxy Z)
SDecide Z (KProxy Z)
SingI Z n0 => SingI Z (P n)
SingI Z n0 => SingI Z (S n)
SingKind Z (KProxy Z)
SuppressUnusedWarnings (TyFun Z Z -> *) PSym0
SuppressUnusedWarnings (TyFun Z Z -> *) SSym0
data Sing Z where SZero :: (~) Z z Zero => Sing Z z SS :: (~) Z z (S n) => Sing Z n -> Sing Z z SP :: (~) Z z (P n) => Sing Z n -> Sing Z z
type (:==) Z a0 b0
type Apply Z Z PSym0 l0 = PSym1 l0
type Apply Z Z SSym0 l0 = SSym1 l0
type DemoteRep Z (KProxy Z) = Z

data family Sing a

The singleton kind-indexed data family.

Instances

SDecide k (KProxy k) => TestEquality k (Sing k)
data Sing Bool where SFalse :: (~) Bool z0 False => Sing Bool z0 STrue :: (~) Bool z0 True => Sing Bool z0
data Sing Ordering where SLT :: (~) Ordering z0 LT => Sing Ordering z0 SEQ :: (~) Ordering z0 EQ => Sing Ordering z0 SGT :: (~) Ordering z0 GT => Sing Ordering z0
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z0 () => Sing () z0
data Sing Z where SZero :: (~) Z z Zero => Sing Z z SS :: (~) Z z (S n) => Sing Z n -> Sing Z z SP :: (~) Z z (P n) => Sing Z n -> Sing Z z
data Sing [a0] where SNil :: (~) [a0] z0 ([] a0) => Sing [a0] z0 SCons :: (~) [a0] z0 ((:) a0 n0 n1) => Sing a0 n0 -> Sing [a0] n1 -> Sing [a0] z0
data Sing (Maybe a0) where SNothing :: (~) (Maybe a0) z0 (Nothing a0) => Sing (Maybe a0) z0 SJust :: (~) (Maybe a0) z0 (Just a0 n0) => Sing a0 n0 -> Sing (Maybe a0) z0
data Sing (TyFun k1 k2 -> *) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t) }
data Sing (Either a0 b0) where SLeft :: (~) (Either a0 b0) z0 (Left a0 b0 n0) => Sing a0 n0 -> Sing (Either a0 b0) z0 SRight :: (~) (Either a0 b0) z0 (Right a0 b0 n0) => Sing b0 n0 -> Sing (Either a0 b0) z0
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a0 b0) z0 ((,) a0 b0 n0 n1) => Sing a0 n0 -> Sing b0 n1 -> Sing ((,) a0 b0) z0
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) a0 b0 c0) z0 ((,,) a0 b0 c0 n0 n1 n2) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing ((,,) a0 b0 c0) z0
data Sing ((,,,) a0 b0 c0 d0) where STuple4 :: (~) ((,,,) a0 b0 c0 d0) z0 ((,,,) a0 b0 c0 d0 n0 n1 n2 n3) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing ((,,,) a0 b0 c0 d0) z0
data Sing ((,,,,) a0 b0 c0 d0 e0) where STuple5 :: (~) ((,,,,) a0 b0 c0 d0 e0) z0 ((,,,,) a0 b0 c0 d0 e0 n0 n1 n2 n3 n4) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing ((,,,,) a0 b0 c0 d0 e0) z0
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where STuple6 :: (~) ((,,,,,) a0 b0 c0 d0 e0 f0) z0 ((,,,,,) a0 b0 c0 d0 e0 f0 n0 n1 n2 n3 n4 n5) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing ((,,,,,) a0 b0 c0 d0 e0 f0) z0
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where STuple7 :: (~) ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0 ((,,,,,,) a0 b0 c0 d0 e0 f0 g0 n0 n1 n2 n3 n4 n5 n6) => Sing a0 n0 -> Sing b0 n1 -> Sing c0 n2 -> Sing d0 n3 -> Sing e0 n4 -> Sing f0 n5 -> Sing g0 n6 -> Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) z0

type SZ z = Sing z Source

Defunctionalization symbols (these can be ignored)

type ZeroSym0 = Zero Source

data SSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Z Z -> *) SSym0
type Apply Z Z SSym0 l0 = SSym1 l0

type SSym1 t = S t Source

data PSym0 l Source

Instances

SuppressUnusedWarnings (TyFun Z Z -> *) PSym0
type Apply Z Z PSym0 l0 = PSym1 l0

type PSym1 t = P t 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 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 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 Source

Negate an integer

Equations

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

type family a #+ b :: Z 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 #- b :: Z 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 #* b :: Z 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 #/ b :: Z 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 < b :: Bool 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 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 Z 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 Z (S Zero) Source

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

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

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

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

sMOne :: Sing Z (P Zero) Source

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

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

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

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

Deprecated synonyms

pZero :: Sing Z Zero Source