Data.Type.Ordinal

Set-theoretic ordinal arithmetic

Data-types

data Ordinal n where

Set-theoretic (finite) ordinals:

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

So, Ordinal n has exactly n inhabitants. So especially Ordinal Z is isomorphic to Void.

Constructors

OZ :: Ordinal (S n)

OS :: Ordinal n -> Ordinal (S n)

Instances

SingRep Nat n => Bounded (Ordinal (S n))

SingRep Nat n => Enum (Ordinal n)

Eq (Ordinal n)

SingRep Nat n => Num (Ordinal n)

Ord (Ordinal n)

Read (Ordinal n) => Read (Ordinal (S n))

Read (Ordinal Z)

Parsing always fails, because there are no inhabitant.

Show (Ordinal n)

Conversion from cardinals to ordinals.

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

sNatToOrd' n m injects m as Ordinal n.

sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n

sNatToOrd' with n inferred.

ordToInt :: Ordinal n -> Int

Convert ordinal into Int.

ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)

Convert Ordinal n into monomorphic SNat

ordToSNat' :: Ordinal n -> CastedOrdinal n

Convert Ordinal n into SNat m with the proof of S m :<<= n.

data CastedOrdinal n where

Constructors

CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n

unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n

Ordinal arithmetics

(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)

Ordinal addition.

enumOrdinal :: SNat n -> [Ordinal n]