Morley.Util.PeanoNatural

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.

Documentation

data PeanoNatural (n :: Peano) where

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.

Bundled Patterns

pattern Zero :: () => n ~ 'Z => PeanoNatural n

Patterns Zero and Succ We introduce pattern synonyms Zero and Succ assuming that Zero and Succ cover all possible cases that satisfy the invariant. Using these patterns, we also avoid cases when `k /= peanoValSing @n s`

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 Succ (Succ Zero) in several places.

pattern Two :: () => n ~ 'S ('S 'Z) => PeanoNatural n

Instances

Show (PeanoNatural n)

Defined in Morley.Util.PeanoNatural

Methods

showsPrec :: Int -> PeanoNatural n -> ShowS

show :: PeanoNatural n -> String

showList :: [PeanoNatural n] -> ShowS

NFData (PeanoNatural n)

Defined in Morley.Util.PeanoNatural

Methods

rnf :: PeanoNatural n -> ()

Eq (PeanoNatural n)

Defined in Morley.Util.PeanoNatural

Methods

(==) :: PeanoNatural n -> PeanoNatural n -> Bool

(/=) :: PeanoNatural n -> PeanoNatural n -> Bool

RenderDoc (PeanoNatural n)

Defined in Morley.Util.PeanoNatural

Methods

renderDoc :: RenderContext -> PeanoNatural n -> Doc

isRenderable :: PeanoNatural n -> Bool

toPeanoNatural :: forall n. SingI n => PeanoNatural n

toPeanoNatural' :: forall (n :: Nat). SingIPeano n => PeanoNatural (ToPeano n)

fromPeanoNatural :: forall n. PeanoNatural n -> Natural

singPeanoVal :: forall (n :: Peano). SingNat n -> Natural

toPeanoNatural and toPeanoNatural' connect PeanoNatural with natural numbers known at run-time.

eqPeanoNat :: PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)

Check if two PeanoNaturals are equal, and return evidence of type equality between the corresponding Nats.

singPeanoNat :: PeanoNatural a -> SingNat a

Get a corresponding SingNat from a PeanoNatural.