Data.Type.Ordinal

Set-theoretic ordinals for built-in type-level naturals

Since 1.0.0.0

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 1.0.0.0

Constructors

OLt :: n < m => SNat (n :: Nat) -> Ordinal m

Instances

(KnownNat n, 0 < n) => Bounded (Ordinal n)

Defined in Data.Type.Ordinal

Methods

minBound :: Ordinal n

maxBound :: Ordinal n

KnownNat 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]

Eq (Ordinal n)

Defined in Data.Type.Ordinal

Methods

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

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

KnownNat n => Num (Ordinal n)

Class synonym for Peano numerals with ordinals.

Since 1.0.0.0

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

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

KnownNat n => 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 (n :: Nat). 0 < n => Ordinal n

Pattern synonym representing the 0-th ordinal.

Since 1.0.0.0

pattern OS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)

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

Since 1.0.0.0

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.

od :: QuasiQuoter

Quasiquoter for ordinal indexed by built-in numeral Nat.

Conversion from cardinals to ordinals.

sNatToOrd' :: m < n => SNat (n :: Nat) -> SNat m -> Ordinal n

sNatToOrd' n m injects m as Ordinal n.

Since 1.0.0.0

sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n

sNatToOrd' with n inferred.

ordToNatural :: Ordinal (n :: Nat) -> Natural

unsafeNaturalToOrd' :: forall proxy (n :: Nat). KnownNat n => proxy n -> Natural -> Ordinal n

Since 1.0.0.0

unsafeNaturalToOrd :: forall (n :: Nat). KnownNat n => Natural -> Ordinal n

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

Since 1.0.0.0

reallyUnsafeNaturalToOrd :: forall pxy (n :: Nat). KnownNat n => pxy -> 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 n. KnownNat n => Natural -> Maybe (Ordinal (n :: Nat))

Since 1.0.0.0

naturalToOrd' :: SNat (n :: Nat) -> Natural -> Maybe (Ordinal n)

ordToSNat :: Ordinal (n :: Nat) -> SomeSNat

Convert Ordinal n into monomorphic SNat

Since 1.0.0.0

inclusion :: n <= m => Ordinal n -> Ordinal m

Inclusion function for ordinals with codomain inferred.

Since 1.0.0.0(constraint was weakened since last released)

inclusion' :: n <= m => SNat m -> Ordinal n -> Ordinal m

Inclusion function for ordinals.

Since 1.0.0.0(constraint was weakened since last released)

Ordinal arithmetics

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

Ordinal addition.

Since 1.0.0.0(type changed)

enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]

Enumerate all Ordinals less than n.

Elimination rules for Ordinal Z.

absurdOrd :: Ordinal 0 -> a

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

Since 1.0.0.0

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

absurdOrd for value in Functor.

Since 1.0.0.0