type-natural-0.8.2.0: Type-level natural and proofs of their properties.

Data.Type.Ordinal.Builtin

Description

Module providing the same API as Ordinal but specialised to GHC's builtin Nat.

Since 0.7.1.0

Synopsis

# Data-types and pattern synonyms

type Ordinal (n :: Nat) = Ordinal n Source #

Set-theoretic (finite) ordinals:

n = {0, 1, ..., n-1}

So, Ordinal n has exactly n inhabitants. So especially Ordinal 0 is isomorphic to Void. This module exports a variant of polymorphic Ordinal specialised to GHC's builtin numeral Nat.

Since 0.7.0.0

pattern OLt :: () => forall (n1 :: Nat). (n1 < t) ~ True => Sing n1 -> Ordinal t Source #

We provide specialised version of constructor OLt as type synonym OLt. In some case, GHC warns about incomplete pattern using pattern OLt, but it is due to the limitation of GHC's current exhaustiveness checker.

Since 0.7.0.0

pattern OZ :: forall (n :: Nat). () => (0 < n) ~ True => Ordinal n Source #

Pattern synonym representing the 0-th ordinal.

Since 0.7.0.0

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

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

Since 0.7.0.0

# Quasi Quoter

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

Quasiquoter for ordinal indexed by GHC's built-n Nat.

Since 0.7.0.0

# Conversion from cardinals to ordinals.

sNatToOrd' :: (m < n) ~ True => Sing n -> Sing m -> Ordinal n Source #

sNatToOrd' n m injects m as Ordinal n.

Since 0.7.0.0

sNatToOrd :: (KnownNat n, (m < n) ~ True) => Sing m -> Ordinal n Source #

sNatToOrd' with n inferred.

Since 0.7.0.0

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

Inclusion function for ordinals.

Since 0.7.0.0

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

Inclusion function for ordinals with codomain inferred.

Since 0.7.0.0

# Ordinal arithmetics

(@+) :: (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m) Source #

Since 0.7.0.0

enumOrdinal :: Sing n -> [Ordinal n] Source #

Enumerate all Ordinals less than n.

Since 0.7.0.0

# Elimination rules for Ordinal 0'.

absurdOrd :: Ordinal 0 -> a Source #

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

Since 0.7.0.0

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

absurdOrd for values in Functor.

Since 0.7.0.0

# Deprecated combinators

Convert ordinal into Int.