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 |
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.
- data Z
- data family Sing k (a :: k) :: *
- type SZ = (Sing :: Z -> Type)
- type ZeroSym0 = Zero
- data SSym0 (l :: TyFun Z Z)
- type SSym1 (t :: Z) = S t
- data PSym0 (l :: TyFun Z Z)
- type PSym1 (t :: Z) = P t
- 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 Z Zero
- sOne :: Sing Z (S Zero)
- sTwo :: Sing Z (S (S Zero))
- sThree :: Sing Z (S (S (S Zero)))
- sFour :: Sing Z (S (S (S (S Zero))))
- sFive :: Sing Z (S (S (S (S (S Zero)))))
- sMOne :: Sing Z (P Zero)
- sMTwo :: Sing Z (P (P Zero))
- sMThree :: Sing Z (P (P (P Zero)))
- sMFour :: Sing Z (P (P (P (P Zero))))
- sMFive :: Sing Z (P (P (P (P (P Zero)))))
- pZero :: Sing Z Zero
- pOne :: Sing Z (S Zero)
- pTwo :: Sing Z (S (S Zero))
- pThree :: Sing Z (S (S (S Zero)))
- pFour :: Sing Z (S (S (S (S Zero))))
- pFive :: Sing Z (S (S (S (S (S Zero)))))
- pMOne :: Sing Z (P Zero)
- pMTwo :: Sing Z (P (P Zero))
- pMThree :: Sing Z (P (P (P Zero)))
- pMFour :: Sing Z (P (P (P (P Zero))))
- pMFive :: Sing Z (P (P (P (P (P Zero)))))
- pSucc :: Sing Z z -> Sing Z (Succ z)
- pPred :: Sing Z z -> Sing Z (Pred z)
The Z
datatype
The datatype for type-level integers.
Eq Z Source # | |
SEq Z Source # | |
PEq Z Source # | |
SDecide Z Source # | |
SingKind Z Source # | |
SingI Z Zero Source # | |
SingI Z n => SingI Z (S n) Source # | |
SingI Z n => SingI Z (P n) Source # | |
SuppressUnusedWarnings (TyFun Z Z -> *) PSym0 Source # | |
SuppressUnusedWarnings (TyFun Z Z -> *) SSym0 Source # | |
data Sing Z Source # | |
type Demote Z Source # | |
type (:/=) Z x y Source # | |
type (:==) Z a b Source # | |
type Apply Z Z PSym0 l Source # | |
type Apply Z Z SSym0 l Source # | |
data family Sing k (a :: k) :: * #
The singleton kind-indexed data family.
data Sing Bool | |
data Sing Ordering | |
data Sing Nat | |
data Sing Symbol | |
data Sing () | |
data Sing Z # | |
data Sing [a] | |
data Sing (Maybe a) | |
data Sing (NonEmpty a) | |
data Sing (Either a b) | |
data Sing (a, b) | |
data Sing ((~>) k1 k2) | |
data Sing (a, b, c) | |
data Sing (a, b, c, d) | |
data Sing (a, b, c, d, e) | |
data Sing (a, b, c, d, e, f) | |
data Sing (a, b, c, d, e, f, g) | |
Defunctionalization symbols (these can be ignored)
Conversions
Type-level operations
Arithmetic
Comparisons
type family NonNegative z :: Constraint where ... Source #
Check if a type-level integer is in fact a natural number
NonNegative Zero = () | |
NonNegative (S z) = () |
Synonyms for certain numbers
This is the singleton value representing Zero
at the term level and
at the type level, simultaneously. Used for raising units to powers.
Deprecated synonyms
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pOne :: Sing Z (S Zero) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pTwo :: Sing Z (S (S Zero)) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pThree :: Sing Z (S (S (S Zero))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pFour :: Sing Z (S (S (S (S Zero)))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pFive :: Sing Z (S (S (S (S (S Zero))))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pMOne :: Sing Z (P Zero) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pMTwo :: Sing Z (P (P Zero)) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pMThree :: Sing Z (P (P (P Zero))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pMFour :: Sing Z (P (P (P (P Zero)))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.
pMFive :: Sing Z (P (P (P (P (P Zero))))) Source #
Deprecated: The singleton prefix is changing from p
to s
. The p
versions will be removed in a future release.