Safe Haskell | None |
---|---|
Language | Haskell2010 |
Set-theoretic ordinals for general peano arithmetic models
- data Ordinal (n :: nat) where
- pattern OZ :: forall nat (n :: nat). IsPeano nat => (Zero nat < n) ~ True => Ordinal n
- pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t) => IsPeano nat => Ordinal t -> Ordinal (Succ t)
- class (PeanoOrder nat, SingKind nat) => HasOrdinal nat
- mkOrdinalQQ :: TypeQ -> QuasiQuoter
- odPN :: QuasiQuoter
- odLit :: QuasiQuoter
- sNatToOrd' :: (PeanoOrder nat, (m < n) ~ True) => Sing (n :: nat) -> Sing m -> Ordinal n
- sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m < n) ~ True) => Sing m -> Ordinal n
- ordToNatural :: HasOrdinal nat => Ordinal (n :: nat) -> Natural
- unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Natural -> Ordinal n
- unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Natural -> Ordinal n
- reallyUnsafeNaturalToOrd :: forall pxy nat (n :: nat). (HasOrdinal nat, SingI n) => pxy nat -> Natural -> Ordinal n
- naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n) => Natural -> Maybe (Ordinal (n :: nat))
- naturalToOrd' :: HasOrdinal nat => Sing (n :: nat) -> Natural -> Maybe (Ordinal n)
- ordToSing :: PeanoOrder nat => Ordinal (n :: nat) -> SomeSing nat
- inclusion :: (n <= m) ~ True => Ordinal n -> Ordinal m
- inclusion' :: (n <= m) ~ True => Sing m -> Ordinal n -> Ordinal m
- (@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m) => Ordinal n -> Ordinal m -> Ordinal (n + m)
- enumOrdinal :: PeanoOrder nat => Sing (n :: nat) -> [Ordinal n]
- absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a
- vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a
- ordToInt :: HasOrdinal nat => Ordinal (n :: nat) -> Int
- unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Int -> Ordinal n
- unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Int -> Ordinal n
Data-types
data Ordinal (n :: nat) where Source #
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
(SingI Nat m, SingI Nat n, (~) Nat n ((+) Nat m 1)) => Bounded (Ordinal Nat n) Source # | |
SingI Nat n => Bounded (Ordinal Nat (S n)) Source # | |
(HasOrdinal nat2, SingI nat2 n) => Enum (Ordinal nat2 n) Source # | |
HasOrdinal nat2 => Eq (Ordinal nat2 n) Source # | |
(HasOrdinal nat2, SingI nat2 n) => Num (Ordinal nat2 n) Source # | |
HasOrdinal nat2 => Ord (Ordinal nat2 n) Source # | |
(SingI nat2 n, HasOrdinal nat2) => Show (Ordinal nat2 n) Source # | |
pattern OZ :: forall nat (n :: nat). IsPeano nat => (Zero nat < n) ~ True => Ordinal n Source #
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) Source #
Pattern synonym
represents (n+1)-th ordinal.OS
n
Since 0.6.0.0
class (PeanoOrder nat, SingKind nat) => HasOrdinal nat Source #
Class synonym for Peano numerals with ordinals.
Since 0.5.0.0
(PeanoOrder nat, SingKind nat) => HasOrdinal nat Source # | |
Quasi Quoter
This section provides QuasiQuoter and general generator for ordinals.
Note that,
instance for Num
s DOES NOT
checks boundary; with Ordinal
, we can use literal with
boundary check.
For example, with od
-XQuasiQuotes
language extension enabled,
[
doesn't typechecks and causes compile-time error,
whilst od
| 12 |] :: Ordinal 112 :: Ordinal 1
compiles but raises run-time error.
So, to enforce correctness, we recommend to use these quoters
instead of bare
numerals.Num
mkOrdinalQQ :: TypeQ -> QuasiQuoter Source #
Quasiquoter generator for ordinals
odPN :: QuasiQuoter Source #
Quasiquoter for ordinal indexed by Peano numeral
.Nat
odLit :: QuasiQuoter Source #
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 Source #
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 Source #
sNatToOrd'
with n
inferred.
ordToNatural :: HasOrdinal nat => Ordinal (n :: nat) -> Natural Source #
unsafeNaturalToOrd' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Natural -> Ordinal n Source #
Since 0.8.0.0
unsafeNaturalToOrd :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Natural -> Ordinal n Source #
Converts
s into Natural
'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 Source #
naturalToOrd :: forall nat n. (HasOrdinal nat, SingI n) => Natural -> Maybe (Ordinal (n :: nat)) Source #
Since 0.8.0.0
naturalToOrd' :: HasOrdinal nat => Sing (n :: nat) -> Natural -> Maybe (Ordinal n) Source #
ordToSing :: PeanoOrder nat => Ordinal (n :: nat) -> SomeSing nat Source #
Convert Ordinal n
into monomorphic Sing
Since 0.5.0.0
inclusion :: (n <= m) ~ True => Ordinal n -> Ordinal m Source #
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 Source #
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) Source #
Ordinal addition.
enumOrdinal :: PeanoOrder nat => Sing (n :: nat) -> [Ordinal n] Source #
Enumerate all
s less than Ordinal
n
.
Elimination rules for Ordinal
Z
.
Ordinal
Z
absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a Source #
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 Source #
Deprecated combinators
ordToInt :: HasOrdinal nat => Ordinal (n :: nat) -> Int Source #
Deprecated: Use ordToNatural instead.
Convert ordinal into
.Int
unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => Int -> Ordinal n Source #
Deprecated: Use unsafeNaturalToOrd instead
Since 0.8.0.0
unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n) => proxy nat -> Int -> Ordinal n Source #
Deprecated: Use unsafeNaturalToOrd' instead
Since 0.8.0.0