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

Safe Haskell None

Data.Type.Ordinal

Description

Set-theoretic ordinal arithmetic

Synopsis

# Data-types

data Ordinal n whereSource

Set-theoretic (finite) ordinals:

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

So, `Ordinal n` has exactly n inhabitants. So especially `Ordinal Z` is isomorphic to `Void`.

Constructors

 OZ :: Ordinal (S n) OS :: Ordinal n -> Ordinal (S n)

Instances

 SingI Nat n => Bounded (Ordinal (S n)) SingI Nat n => Enum (Ordinal n) Eq (Ordinal n) SingI Nat n => Num (Ordinal n) Ord (Ordinal n) Read (Ordinal n) => Read (Ordinal (S n)) Read (Ordinal Z) Parsing always fails, because there are no inhabitant. Show (Ordinal n)

# Conversion from cardinals to ordinals.

sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal nSource

`sNatToOrd'` `n m` injects `m` as `Ordinal n`.

sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal nSource

`sNatToOrd'` with `n` inferred.

ordToInt :: Ordinal n -> IntSource

Convert ordinal into `Int`.

ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)Source

Convert `Ordinal n` into monomorphic `SNat`

Convert `Ordinal n` into `SNat m` with the proof of `S m :<<= n`.

data CastedOrdinal n whereSource

Constructors

 CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n

unsafeFromInt :: forall n. SingI n => Int -> Ordinal nSource

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

Inclusion function for ordinals with codomain inferred.

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

Inclusion function for ordinals.

# Ordinal arithmetics

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

Ordinal addition.

# Quasi Quote

Quasiquoter for ordinals