Safe Haskell | None |
---|---|
Language | Haskell2010 |
Utility for PeanoNatural
At the moment, we have no other libriaries with that would
provide effective implementation of type-level natural
numbers. So we define our own data type called PeanoNatural
.
Using this type one may extract a term-level natural number
from a type-level one quite simply.
Synopsis
- data PeanoNatural (n :: Nat) where
- pattern Zero :: () => n ~ 'Z => PeanoNatural n
- pattern Succ :: () => n ~ 'S m => PeanoNatural m -> PeanoNatural n
- pattern One :: () => n ~ 'S 'Z => PeanoNatural n
- pattern Two :: () => n ~ 'S ('S 'Z) => PeanoNatural n
- toPeanoNatural :: forall n. SingI n => PeanoNatural n
- toPeanoNatural' :: forall (n :: Nat). SingI (ToPeano n) => PeanoNatural (ToPeano n)
- fromPeanoNatural :: forall n. PeanoNatural n -> Natural
- singPeanoVal :: forall (n :: Nat). SingNat n -> Natural
Documentation
data PeanoNatural (n :: Nat) where Source #
PeanoNatural data type
The PN
constructor stores s :: SingNat n
and k :: Natural
with the following invariant:
if PN s k :: PeanoNatural n
, then k == n
.
This definition allows extracting values of Natural
without O(n) conversion from SingNat n
.
pattern Zero :: () => n ~ 'Z => PeanoNatural n | Patterns |
pattern Succ :: () => n ~ 'S m => PeanoNatural m -> PeanoNatural n | |
pattern One :: () => n ~ 'S 'Z => PeanoNatural n | The following patterns are introduced for convenience.
This allow us to avoid writing |
pattern Two :: () => n ~ 'S ('S 'Z) => PeanoNatural n |
Instances
Eq (PeanoNatural n) Source # | |
Defined in Util.PeanoNatural (==) :: PeanoNatural n -> PeanoNatural n -> Bool # (/=) :: PeanoNatural n -> PeanoNatural n -> Bool # | |
Show (PeanoNatural n) Source # | |
Defined in Util.PeanoNatural showsPrec :: Int -> PeanoNatural n -> ShowS # show :: PeanoNatural n -> String # showList :: [PeanoNatural n] -> ShowS # | |
NFData (PeanoNatural n) Source # | |
Defined in Util.PeanoNatural rnf :: PeanoNatural n -> () # |
toPeanoNatural :: forall n. SingI n => PeanoNatural n Source #
toPeanoNatural' :: forall (n :: Nat). SingI (ToPeano n) => PeanoNatural (ToPeano n) Source #
fromPeanoNatural :: forall n. PeanoNatural n -> Natural Source #