Safe Haskell | None |
---|---|

Language | Haskell2010 |

Provides singletons and general type-level utilities. singletons are value-level representations of types.

- data family The k :: k -> *
- class KnownSing x where
- (*.) :: The Nat n -> The Nat m -> The Nat (n * m)
- (+.) :: The Nat n -> The Nat m -> The Nat (n + m)
- (^.) :: The Nat n -> The Nat m -> The Nat (n ^ m)
- (-.) :: m <= n => The Nat n -> The Nat m -> The Nat (n - m)
- (<=.) :: The Nat n -> The Nat m -> The Bool (n <=? m)
- totalOrder :: p n -> q m -> ((n <=? m) :~: False) -> (m <=? n) :~: True
- type (<=) x y = (x <=? y) :~: True
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- data Nat :: *

# Documentation

data family The k :: k -> * Source #

A data family for singletons. The cute name allows code like this:

addZeroZero :: The Nat n -> n + 0 :~: n

data The Bool Source # | |

data The Nat Source # | This is just a newtype wrapper for The reason for this setup is to allow properties and invariants to be proven about the numbers involved, while actual computation can be carried out efficiently on the values at runtime. See the implementation of Data.Heap.Indexed.Leftist for an example of the uses of this type. |

data The Nat Source # | Singleton for type-level Peano numbers. |

data The [k] Source # | |

(*.) :: The Nat n -> The Nat m -> The Nat (n * m) infixl 7 Source #

Multiply two numbers, on both the value and type level.

(+.) :: The Nat n -> The Nat m -> The Nat (n + m) infixl 6 Source #

Add two numbers, on both the value and type level.

(^.) :: The Nat n -> The Nat m -> The Nat (n ^ m) infixr 8 Source #

Raise a number to a power, on the type-level and value-level.

(-.) :: m <= n => The Nat n -> The Nat m -> The Nat (n - m) infixl 6 Source #

Subtract two numbers, on the type-level and value-level, with a proof that overflow can't occur.

(<=.) :: The Nat n -> The Nat m -> The Bool (n <=? m) infix 4 Source #

Test order between two numbers, and provide a proof of that order with the result.

totalOrder :: p n -> q m -> ((n <=? m) :~: False) -> (m <=? n) :~: True Source #

A proof of a total order on the naturals.

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #

Multiplication of type-level naturals.

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #

Exponentiation of type-level naturals.

(Kind) This is the kind of type-level natural numbers.

KnownNat n => KnownSing Nat n Source # | |

data The Nat Source # | This is just a newtype wrapper for The reason for this setup is to allow properties and invariants to be proven about the numbers involved, while actual computation can be carried out efficiently on the values at runtime. See the implementation of Data.Heap.Indexed.Leftist for an example of the uses of this type. |

type (==) Nat a b | |