Safe Haskell | None |
---|---|
Language | Haskell2010 |
Set-theoretic ordinals for built-in type-level naturals
Since 1.0.0.0
Synopsis
- data Ordinal (n :: Nat) where
- pattern OZ :: forall (n :: Nat). 0 < n => Ordinal n
- pattern OS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t)
- od :: QuasiQuoter
- sNatToOrd' :: m < n => SNat (n :: Nat) -> SNat m -> Ordinal n
- sNatToOrd :: (KnownNat n, m < n) => SNat m -> Ordinal n
- ordToNatural :: Ordinal (n :: Nat) -> Natural
- unsafeNaturalToOrd' :: forall proxy (n :: Nat). KnownNat n => proxy n -> Natural -> Ordinal n
- unsafeNaturalToOrd :: forall (n :: Nat). KnownNat n => Natural -> Ordinal n
- reallyUnsafeNaturalToOrd :: forall pxy (n :: Nat). KnownNat n => pxy -> Natural -> Ordinal n
- naturalToOrd :: forall n. KnownNat n => Natural -> Maybe (Ordinal (n :: Nat))
- naturalToOrd' :: SNat (n :: Nat) -> Natural -> Maybe (Ordinal n)
- ordToSNat :: Ordinal (n :: Nat) -> SomeSNat
- inclusion :: n <= m => Ordinal n -> Ordinal m
- inclusion' :: n <= m => SNat m -> Ordinal n -> Ordinal m
- (@+) :: forall (n :: Nat) m. (KnownNat n, KnownNat m) => Ordinal n -> Ordinal m -> Ordinal (n + m)
- enumOrdinal :: SNat (n :: Nat) -> [Ordinal n]
- absurdOrd :: Ordinal 0 -> a
- vacuousOrd :: Functor f => f (Ordinal 0) -> f a
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 1.0.0.0
Instances
(KnownNat n, 0 < n) => Bounded (Ordinal n) Source # | |
KnownNat n => Enum (Ordinal n) Source # | |
Defined in Data.Type.Ordinal succ :: Ordinal n -> Ordinal n # pred :: Ordinal n -> 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) Source # | |
KnownNat n => Num (Ordinal n) Source # | Class synonym for Peano numerals with ordinals. Since 1.0.0.0 |
Ord (Ordinal n) Source # | |
Defined in Data.Type.Ordinal | |
KnownNat n => Show (Ordinal n) Source # | |
pattern OZ :: forall (n :: Nat). 0 < n => Ordinal n Source #
Pattern synonym representing the 0-th ordinal.
Since 1.0.0.0
pattern OS :: forall (t :: Nat). KnownNat t => Ordinal t -> Ordinal (Succ t) Source #
Pattern synonym
represents (n+1)-th ordinal.OS
n
Since 1.0.0.0
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
od :: QuasiQuoter Source #
Quasiquoter for ordinal indexed by built-in numeral
.Nat
Conversion from cardinals to ordinals.
sNatToOrd' :: m < n => SNat (n :: Nat) -> SNat m -> Ordinal n Source #
sNatToOrd'
n m
injects m
as Ordinal n
.
Since 1.0.0.0
unsafeNaturalToOrd' :: forall proxy (n :: Nat). KnownNat n => proxy n -> Natural -> Ordinal n Source #
Since 1.0.0.0
unsafeNaturalToOrd :: forall (n :: Nat). KnownNat n => Natural -> Ordinal n Source #
Converts
s into Natural
'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 Source #
ordToSNat :: Ordinal (n :: Nat) -> SomeSNat Source #
Convert Ordinal n
into monomorphic SNat
Since 1.0.0.0
inclusion :: n <= m => Ordinal n -> Ordinal m Source #
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 Source #
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) Source #
Ordinal addition.
Since 1.0.0.0(type changed)
Elimination rules for Ordinal
Z
.
Ordinal
Z