Data.Type.Ordinal.Peano

Module providing the same API as Ordinal but specialised to peano numeral Nat.

Since 0.7.0.0

Data-types and pattern synonyms

type Ordinal (n :: Nat) = Ordinal n

Set-theoretic (finite) ordinals:

n = {0, 1, ..., n-1}

So, Ordinal n has exactly n inhabitants. So especially Ordinal 'Z is isomorphic to Void. This module exports a variant of polymorphic Ordinal specialised to Peano numeral Nat.

Since 0.7.0.0

pattern OLt :: () => forall (n1 :: Nat). (n1 < t) ~ True => Sing n1 -> Ordinal t

We provide specialised version of constructor OLt as type synonym OLt. In some case, GHC warns about incomplete pattern using pattern OLt, but it is due to the limitation of GHC's current exhaustiveness checker.

Since 0.7.0.0

pattern OZ :: forall (n :: Nat). () => (Z < n) ~ True => Ordinal n

Pattern synonym representing the 0-th ordinal.

Since 0.7.0.0

pattern OS :: forall (t :: Nat). SingI t => Ordinal t -> Ordinal (Succ t)

Pattern synonym OS n represents (n+1)-th ordinal.

Since 0.7.0.0

Quasi Quoter

This section provides QuasiQuoter for ordinals. Note that, Num instance for Ordinals DOES NOT checks boundary; with od, we can use literal with boundary check. For example, with -XQuasiQuotes language extension enabled, [od| 12 |] :: Ordinal 1 doesn't typechecks and causes compile-time error, whilst 12 :: Ordinal 1 compiles but raises run-time error. So, to enforce correctness, we recommend to use these quoters instead of bare Num numerals.

od :: QuasiQuoter

Quasiquoter for ordinal indexed by Peano numeral Nat.

Since 0.7.0.0

Conversion from cardinals to ordinals.

sNatToOrd' :: (m < n) ~ True => Sing n -> Sing m -> Ordinal n

sNatToOrd' n m injects m as Ordinal n.

Since 0.7.0.0

sNatToOrd :: (SingI n, (m < n) ~ True) => Sing m -> Ordinal n

sNatToOrd' with n inferred.

Since 0.7.0.0

inclusion :: (n <= m) ~ True => Ordinal n -> Ordinal m

Inclusion function for ordinals.

Since 0.7.0.0

inclusion' :: (n <= m) ~ True => Sing m -> Ordinal n -> Ordinal m

Inclusion function for ordinals with codomain inferred.

Since 0.7.0.0

ordToNatural :: Ordinal (n :: Nat) -> Natural

unsafeNaturalToOrd :: SingI (n :: Nat) => Natural -> Ordinal n

naturalToOrd :: SingI (n :: Nat) => Natural -> Maybe (Ordinal n)

naturalToOrd' :: Sing (n :: Nat) -> Natural -> Maybe (Ordinal n)

Ordinal arithmetics

(@+) :: (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m)

Ordinal addition.

Since 0.7.0.0

enumOrdinal :: Sing n -> [Ordinal n]

Enumerate all Ordinals less than n.

Since 0.7.0.0

Elimination rules for Ordinal Z.

absurdOrd :: Ordinal Z -> a

Since Ordinal 'Z is logically not inhabited, we can coerce it to any value.

Since 0.7.0.0

vacuousOrd :: Functor f => f (Ordinal Z) -> f a

absurdOrd for values in Functor.

Since 0.7.0.0

Deprecated Combinators

ordToInt :: Ordinal n -> Int

Convert ordinal into Int.

Since 0.7.0.0

unsafeFromInt :: SingI n => Int -> Ordinal n