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

Safe HaskellNone
LanguageHaskell2010

Data.Type.Ordinal

Contents

Description

Set-theoretic ordinals for general peano arithmetic models

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.

Since 0.6.0.0

Constructors

OLt :: (IsPeano nat, (n :< m) ~ True) => Sing (n :: nat) -> Ordinal m 

Instances

(SingI Nat m, SingI Nat n, (~) Nat n ((+) m 1)) => Bounded (Ordinal Nat n) Source # 
SingI Nat n => Bounded (Ordinal Nat (S n)) Source # 

Methods

minBound :: Ordinal Nat (S n) #

maxBound :: Ordinal Nat (S n) #

(HasOrdinal nat1, SingI nat1 n) => Enum (Ordinal nat1 n) Source # 

Methods

succ :: Ordinal nat1 n -> Ordinal nat1 n #

pred :: Ordinal nat1 n -> Ordinal nat1 n #

toEnum :: Int -> Ordinal nat1 n #

fromEnum :: Ordinal nat1 n -> Int #

enumFrom :: Ordinal nat1 n -> [Ordinal nat1 n] #

enumFromThen :: Ordinal nat1 n -> Ordinal nat1 n -> [Ordinal nat1 n] #

enumFromTo :: Ordinal nat1 n -> Ordinal nat1 n -> [Ordinal nat1 n] #

enumFromThenTo :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n -> [Ordinal nat1 n] #

HasOrdinal nat1 => Eq (Ordinal nat1 n) Source # 

Methods

(==) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

(/=) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

(HasOrdinal nat1, SingI nat1 n) => Num (Ordinal nat1 n) Source # 

Methods

(+) :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n #

(-) :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n #

(*) :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n #

negate :: Ordinal nat1 n -> Ordinal nat1 n #

abs :: Ordinal nat1 n -> Ordinal nat1 n #

signum :: Ordinal nat1 n -> Ordinal nat1 n #

fromInteger :: Integer -> Ordinal nat1 n #

HasOrdinal nat1 => Ord (Ordinal nat1 n) Source # 

Methods

compare :: Ordinal nat1 n -> Ordinal nat1 n -> Ordering #

(<) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

(<=) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

(>) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

(>=) :: Ordinal nat1 n -> Ordinal nat1 n -> Bool #

max :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n #

min :: Ordinal nat1 n -> Ordinal nat1 n -> Ordinal nat1 n #

(SingI nat1 n, HasOrdinal nat1) => Show (Ordinal nat1 n) Source # 

Methods

showsPrec :: Int -> Ordinal nat1 n -> ShowS #

show :: Ordinal nat1 n -> String #

showList :: [Ordinal nat1 n] -> ShowS #

pattern OZ :: forall nat n. IsPeano nat => (~) Bool ((:<) nat (Zero nat) n) True => Ordinal nat n Source #

Pattern synonym representing the 0-th ordinal.

Since 0.6.0.0

pattern OS :: forall nat t. (PeanoOrder nat, SingI nat t) => IsPeano nat => Ordinal nat t -> Ordinal nat (Succ nat t) Source #

Pattern synonym OS n represents (n+1)-th ordinal.

Since 0.6.0.0

class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *), Integral (MonomorphicRep (Sing :: nat -> *)), Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat Source #

Class synonym for Peano numerals with ordinals.

Since 0.5.0.0

Instances

(PeanoOrder nat1, Monomorphicable nat1 (Sing nat1), Integral (MonomorphicRep nat1 (Sing nat1)), Show (MonomorphicRep nat1 (Sing nat1))) => HasOrdinal nat1 Source # 

Quasi Quoter

This section provides QuasiQuoter and general generator for ordinals. Note that, Num instance for Ordinals DOES NOT checks boundary; with od, we can use literal with boundary check. For example, with -XQuasiQuotes language extension enabled, [od| 12 |] :: Ordinal 1 doesn't typechecks and causes compile-time error, whilst 12 :: Ordinal 1 compiles but raises run-time error. So, to enforce correctness, we recommend to use these quoters instead of bare Num numerals.

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.

ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *)) => Ordinal (n :: nat) -> int Source #

Convert ordinal into Int.

ordToSing :: PeanoOrder nat => Ordinal (n :: nat) -> SomeSing nat Source #

Convert Ordinal n into monomorphic Sing

Since 0.5.0.0

unsafeFromInt :: forall n. (HasOrdinal nat, SingI (n :: nat)) => MonomorphicRep (Sing :: nat -> *) -> Ordinal n Source #

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 Ordinals less than n.

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

absurdOrd for value in Functor.

Since 0.2.3.0