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

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

Methods

minBound :: Ordinal (S n)

maxBound :: Ordinal (S n)

SingI Nat n => Enum (Ordinal n)

Methods

succ :: Ordinal n -> Ordinal n

pred :: Ordinal n -> Ordinal n

toEnum :: Int -> Ordinal n

fromEnum :: Ordinal n -> Int

enumFrom :: Ordinal n -> [Ordinal n]

enumFromThen :: Ordinal n -> Ordinal n -> [Ordinal n]

enumFromTo :: Ordinal n -> Ordinal n -> [Ordinal n]

enumFromThenTo :: Ordinal n -> Ordinal n -> Ordinal n -> [Ordinal n]

Eq (Ordinal n)

Methods

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

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

SingI Nat n => Num (Ordinal n)

Methods

(+) :: Ordinal n -> Ordinal n -> Ordinal n

(-) :: Ordinal n -> Ordinal n -> Ordinal n

(*) :: Ordinal n -> Ordinal n -> Ordinal n

negate :: Ordinal n -> Ordinal n

abs :: Ordinal n -> Ordinal n

signum :: Ordinal n -> Ordinal n

fromInteger :: Integer -> Ordinal n

Ord (Ordinal n)

Methods

compare :: Ordinal n -> Ordinal n -> Ordering

(<) :: Ordinal n -> Ordinal n -> Bool

(<=) :: Ordinal n -> Ordinal n -> Bool

(>) :: Ordinal n -> Ordinal n -> Bool

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

max :: Ordinal n -> Ordinal n -> Ordinal n

min :: Ordinal n -> Ordinal n -> Ordinal n

Read (Ordinal Z)

Parsing always fails, because there are no inhabitant.

Methods

readsPrec :: Int -> ReadS (Ordinal Z)

readList :: ReadS [Ordinal Z]

readPrec :: ReadPrec (Ordinal Z)

readListPrec :: ReadPrec [Ordinal Z]

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

Methods

readsPrec :: Int -> ReadS (Ordinal (S n))

readList :: ReadS [Ordinal (S n)]

readPrec :: ReadPrec (Ordinal (S n))

readListPrec :: ReadPrec [Ordinal (S n)]

Show (Ordinal n)

Methods

showsPrec :: Int -> Ordinal n -> ShowS

show :: Ordinal n -> String

showList :: [Ordinal n] -> ShowS

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 :: (SingI 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. SingI n => Int -> Ordinal n

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

Inclusion function for ordinals with codomain inferred.

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

Inclusion function for ordinals.

Ordinal arithmetics

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

Ordinal addition.

enumOrdinal :: SNat n -> [Ordinal n]

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.2.3.0

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

absurdOrd for the value in Functor.

Since 0.2.3.0

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

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

Quasiquoter for ordinals