type-natural-0.3.0.0: Type-level natural and proofs of their properties.

Safe HaskellNone
LanguageHaskell98

Data.Type.Ordinal

Contents

Description

Set-theoretic ordinal arithmetic

Synopsis

Data-types

data Ordinal n where Source

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

SingI Nat n => Bounded (Ordinal (S n)) Source 
SingI Nat n => Enum (Ordinal n) Source 
Eq (Ordinal n) Source 
SingI Nat n => Num (Ordinal n) Source 
Ord (Ordinal n) Source 
Read (Ordinal Z) Source

Parsing always fails, because there are no inhabitant.

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

Conversion from cardinals to ordinals.

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

sNatToOrd' n m injects m as Ordinal n.

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

sNatToOrd' with n inferred.

ordToInt :: Ordinal n -> Int Source

Convert ordinal into Int.

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

Convert Ordinal n into monomorphic SNat

ordToSNat' :: Ordinal n -> CastedOrdinal n Source

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

data CastedOrdinal n where Source

Constructors

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

unsafeFromInt :: forall n. SingI n => Int -> Ordinal n Source

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

Inclusion function for ordinals with codomain inferred.

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

Inclusion function for ordinals.

Ordinal arithmetics

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

Ordinal addition.

enumOrdinal :: SNat n -> [Ordinal n] Source

Elimination rules for Ordinal Z.

absurdOrd :: Ordinal Z -> a Source

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

Since 0.2.3.0

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

absurdOrd for the value in Functor.

Since 0.2.3.0

vacuousOrdM :: Monad m => m (Ordinal Z) -> m a Source

absurdOrd for the value in Monad. This function will become uneccesary once Applicative (and hence Functor) become the superclass of Monad.

Since 0.2.3.0

Quasi Quoter

od :: QuasiQuoter Source

Quasiquoter for ordinals