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 = 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 t. () => forall n1. (~) Bool ((:<) Nat n1 t) True => Sing Nat n1 -> Ordinal Nat 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. () => (~) Bool ((:<) Nat Z n) True => Ordinal Nat n

Pattern synonym representing the 0-th ordinal.

Since 0.7.0.0

pattern OS :: forall t. SingI Nat t => Ordinal Nat t -> Ordinal Nat (Succ Nat 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

ordToInt :: Ordinal n -> Integer

Convert ordinal into Int.

Since 0.7.0.0

unsafeFromInt :: SingI n => MonomorphicRep (Sing :: Nat -> Type) -> Ordinal n

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

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