Data.Type.Ordinal

Set-theoretic ordinals for general peano arithmetic models

Data-types

data Ordinal (n :: nat) 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 ((+) Nat 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 nat2, SingI nat2 n) => Enum (Ordinal nat2 n)

Methods

succ :: Ordinal nat2 n -> Ordinal nat2 n

pred :: Ordinal nat2 n -> Ordinal nat2 n

toEnum :: Int -> Ordinal nat2 n

fromEnum :: Ordinal nat2 n -> Int

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

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

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

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

HasOrdinal nat2 => Eq (Ordinal nat2 n)

Methods

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

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

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

Methods

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

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

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

negate :: Ordinal nat2 n -> Ordinal nat2 n

abs :: Ordinal nat2 n -> Ordinal nat2 n

signum :: Ordinal nat2 n -> Ordinal nat2 n

fromInteger :: Integer -> Ordinal nat2 n

HasOrdinal nat2 => Ord (Ordinal nat2 n)

Methods

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

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

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

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

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

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

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

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

Methods

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

show :: Ordinal nat2 n -> String

showList :: [Ordinal nat2 n] -> ShowS

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

Pattern synonym representing the 0-th ordinal.

Since 0.6.0.0

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

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

Since 0.6.0.0

class (PeanoOrder nat, SingKind nat) => HasOrdinal nat

Class synonym for Peano numerals with ordinals.

Since 0.5.0.0

Instances

(PeanoOrder nat, SingKind nat) => HasOrdinal nat

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.

ordToNatural :: HasOrdinal nat => Ordinal (n :: nat) -> Natural

unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Natural -> Ordinal n

Since 0.8.0.0

unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Natural -> Ordinal n

Converts Naturals into 'Ordinal n'. If the given natural is greater or equal to n, raises exception.

Since 0.8.0.0

reallyUnsafeNaturalToOrd :: forall pxy nat (n :: nat). (HasOrdinal nat, SingI n) => pxy nat -> Natural -> Ordinal n

Warning: This function may violate type safety. Use with care!

Converts Naturals into Ordinal n, WITHOUT any boundary check. This function may easily violate type-safety. Use with care!

naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n) => Natural -> Maybe (Ordinal (n :: nat))

Since 0.8.0.0

naturalToOrd' :: HasOrdinal nat => Sing (n :: nat) -> Natural -> Maybe (Ordinal n)

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

Convert Ordinal n into monomorphic Sing

Since 0.5.0.0

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

Deprecated combinators

ordToInt :: HasOrdinal nat => Ordinal (n :: nat) -> Int

Deprecated: Use ordToNatural instead.

Convert ordinal into Int.

unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Int -> Ordinal n

Deprecated: Use unsafeNaturalToOrd instead

Since 0.8.0.0

unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Int -> Ordinal n

Deprecated: Use unsafeNaturalToOrd' instead

Since 0.8.0.0