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

Safe Haskell None Haskell2010

Data.Type.Ordinal

Description

Set-theoretic ordinal arithmetic

Synopsis

# Data-types

data Ordinal n 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.

Constructors

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

Instances

 SingI Nat n => Bounded (Ordinal (S n)) Source # MethodsminBound :: Ordinal (S n) #maxBound :: Ordinal (S n) # SingI Nat n => Enum (Ordinal n) Source # Methodssucc :: Ordinal n -> Ordinal n #pred :: Ordinal n -> Ordinal n #toEnum :: Int -> 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 # Methods(==) :: Ordinal n -> Ordinal n -> Bool #(/=) :: Ordinal n -> Ordinal n -> Bool # SingI Nat n => Num (Ordinal n) Source # Methods(+) :: Ordinal n -> Ordinal n -> Ordinal n #(-) :: Ordinal n -> Ordinal n -> Ordinal n #(*) :: Ordinal n -> Ordinal n -> Ordinal n #negate :: Ordinal n -> Ordinal n #abs :: Ordinal n -> Ordinal n #signum :: Ordinal n -> Ordinal n # Ord (Ordinal n) Source # Methodscompare :: Ordinal n -> Ordinal n -> Ordering #(<) :: Ordinal n -> Ordinal n -> Bool #(<=) :: Ordinal n -> Ordinal n -> Bool #(>) :: Ordinal n -> Ordinal n -> Bool #(>=) :: Ordinal n -> Ordinal n -> Bool #max :: Ordinal n -> Ordinal n -> Ordinal n #min :: Ordinal n -> Ordinal n -> Ordinal n # Source # Parsing always fails, because there are no inhabitant. Methods Read (Ordinal n) => Read (Ordinal (S n)) Source # MethodsreadsPrec :: Int -> ReadS (Ordinal (S n)) #readList :: ReadS [Ordinal (S n)] #readPrec :: ReadPrec (Ordinal (S n)) # Show (Ordinal n) Source # MethodsshowsPrec :: Int -> Ordinal n -> ShowS #show :: Ordinal n -> String #showList :: [Ordinal n] -> ShowS #

# 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.

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 where Source #

Constructors

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

unsafeFromInt :: forall n. SingI n => Int -> Ordinal n Source #

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.

# Elimination rules for 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

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

absurdOrd for the value in Functor.

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

Quasiquoter for ordinals