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 m, SingI n, n ~ (m + 1)) => Bounded (Ordinal n)

Defined in Data.Type.Ordinal

Methods

minBound :: Ordinal n

maxBound :: Ordinal n

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

Defined in Data.Type.Ordinal

Methods

minBound :: Ordinal (S n)

maxBound :: Ordinal (S n)

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

Defined in Data.Type.Ordinal

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]

HasOrdinal nat => Eq (Ordinal n)

Defined in Data.Type.Ordinal

Methods

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

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

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

Defined in Data.Type.Ordinal

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

HasOrdinal nat => Ord (Ordinal n)

Defined in Data.Type.Ordinal

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

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

Defined in Data.Type.Ordinal

Methods

showsPrec :: Int -> Ordinal n -> ShowS

show :: Ordinal n -> String

showList :: [Ordinal 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

Defined in Data.Type.Ordinal

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