Safe Haskell | None |
---|---|
Language | Haskell2010 |
Set-theoretic ordinal arithmetic
- data Ordinal n where
- sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n
- sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal n
- ordToInt :: Ordinal n -> Int
- ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *)
- ordToSNat' :: Ordinal n -> CastedOrdinal n
- data CastedOrdinal n where
- CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n
- unsafeFromInt :: forall n. SingI n => Int -> Ordinal n
- inclusion :: (n :<<= m) ~ True => Ordinal n -> Ordinal m
- inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m
- (@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)
- enumOrdinal :: SNat n -> [Ordinal n]
- absurdOrd :: Ordinal Z -> a
- vacuousOrd :: Functor f => f (Ordinal Z) -> f a
- vacuousOrdM :: Monad m => m (Ordinal Z) -> m a
- od :: QuasiQuoter
Data-types
Set-theoretic (finite) ordinals:
n = {0, 1, ..., n-1}
So, Ordinal n
has exactly n inhabitants. So especially Ordinal 'Z
is isomorphic to Void
.
SingI Nat n => Bounded (Ordinal (S n)) Source # | |
SingI Nat n => Enum (Ordinal n) Source # | |
Eq (Ordinal n) Source # | |
SingI Nat n => Num (Ordinal n) Source # | |
Ord (Ordinal n) Source # | |
Read (Ordinal Z) Source # | Parsing always fails, because there are no inhabitant. |
Read (Ordinal n) => Read (Ordinal (S n)) Source # | |
Show (Ordinal n) Source # | |
Conversion from cardinals to ordinals.
sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n Source #
sNatToOrd'
n m
injects m
as Ordinal n
.
sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal n Source #
sNatToOrd'
with n
inferred.
ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *) Source #
Convert Ordinal n
into monomorphic SNat
ordToSNat' :: Ordinal n -> CastedOrdinal n Source #
Convert Ordinal n
into SNat m
with the proof of 'S m :<<= n
.
data CastedOrdinal n where Source #
CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n |
inclusion :: (n :<<= m) ~ True => Ordinal n -> Ordinal m Source #
Inclusion function for ordinals with codomain inferred.
inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m Source #
Inclusion function for ordinals.
Ordinal arithmetics
(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) Source #
Ordinal addition.
enumOrdinal :: SNat n -> [Ordinal n] Source #
Elimination rules for Ordinal
Z
.
Ordinal
Z
absurdOrd :: Ordinal Z -> a Source #
Since Ordinal 'Z
is logically not inhabited, we can coerce it to any value.
Since 0.2.3.0
vacuousOrdM :: Monad m => m (Ordinal Z) -> m a Source #
absurdOrd
for the value in Monad
.
This function will become uneccesary once Applicative
(and hence Functor
)
become the superclass of Monad
.
Since 0.2.3.0
Quasi Quoter
od :: QuasiQuoter Source #
Quasiquoter for ordinals