Data.Type.Ordinal

Set-theoretic ordinals for general peano arithmetic models

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.

Since 0.6.0.0

Constructors

OLt :: (IsPeano nat, (n :< m) ~ True) => Sing (n :: nat) -> Ordinal m

Instances

(SingI Nat m, SingI Nat n, (~) Nat n ((+) m 1)) => Bounded (Ordinal Nat n)

Methods

minBound :: Ordinal Nat n

maxBound :: Ordinal Nat n

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

Methods

minBound :: Ordinal Nat (S n)

maxBound :: Ordinal Nat (S n)

(HasOrdinal nat1, SingI nat1 n) => Enum (Ordinal nat1 n)

Methods

succ :: Ordinal nat1 n -> Ordinal nat1 n

pred :: Ordinal nat1 n -> Ordinal nat1 n

toEnum :: Int -> Ordinal nat1 n

fromEnum :: Ordinal nat1 n -> Int

enumFrom :: Ordinal nat1 n -> [Ordinal nat1 n]

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

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

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

HasOrdinal nat1 => Eq (Ordinal nat1 n)

Methods

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

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

(HasOrdinal nat1, SingI nat1 n) => Num (Ordinal nat1 n)

Methods

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

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

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

negate :: Ordinal nat1 n -> Ordinal nat1 n

abs :: Ordinal nat1 n -> Ordinal nat1 n

signum :: Ordinal nat1 n -> Ordinal nat1 n

fromInteger :: Integer -> Ordinal nat1 n

HasOrdinal nat1 => Ord (Ordinal nat1 n)

Methods

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

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

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

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

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

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

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

(SingI nat1 n, HasOrdinal nat1) => Show (Ordinal nat1 n)

Methods

showsPrec :: Int -> Ordinal nat1 n -> ShowS

show :: Ordinal nat1 n -> String

showList :: [Ordinal nat1 n] -> ShowS

pattern OZ :: forall nat n. IsPeano nat => (~) Bool ((:<) nat (Zero nat) n) True => Ordinal nat n

Pattern synonym representing the 0-th ordinal.

Since 0.6.0.0

pattern OS :: forall nat t. (PeanoOrder nat, SingI nat t) => IsPeano nat => Ordinal nat t -> Ordinal nat (Succ nat t)

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

Since 0.6.0.0

class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *), Integral (MonomorphicRep (Sing :: nat -> *)), Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat

Class synonym for Peano numerals with ordinals.

Since 0.5.0.0

Instances

(PeanoOrder nat1, Monomorphicable nat1 (Sing nat1), Integral (MonomorphicRep nat1 (Sing nat1)), Show (MonomorphicRep nat1 (Sing nat1))) => HasOrdinal nat1

Quasi Quoter

This section provides QuasiQuoter and general generator 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.

mkOrdinalQQ :: TypeQ -> QuasiQuoter

Quasiquoter generator for ordinals

odPN :: QuasiQuoter

Quasiquoter for ordinal indexed by Peano numeral Nat.

odLit :: QuasiQuoter

Quasiquoter for ordinal indexed by built-in numeral Nat.

Conversion from cardinals to ordinals.

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

sNatToOrd' n m injects m as Ordinal n.

Since 0.5.0.0

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

sNatToOrd' with n inferred.

ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *)) => Ordinal (n :: nat) -> int

Convert ordinal into Int.

ordToSing :: PeanoOrder nat => Ordinal (n :: nat) -> SomeSing nat

Convert Ordinal n into monomorphic Sing

Since 0.5.0.0

unsafeFromInt :: forall n. (HasOrdinal nat, SingI (n :: nat)) => MonomorphicRep (Sing :: nat -> *) -> Ordinal n

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

Inclusion function for ordinals with codomain inferred.

Since 0.7.0.0 (constraint was weakened since last released)

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

Inclusion function for ordinals.

Since 0.7.0.0 (constraint was weakened since last released)

Ordinal arithmetics

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

Ordinal addition.

enumOrdinal :: PeanoOrder nat => Sing (n :: nat) -> [Ordinal n]

Enumerate all Ordinals less than n.

Elimination rules for Ordinal Z.

absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a

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

Since 0.2.3.0

vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a

absurdOrd for value in Functor.

Since 0.2.3.0