|Version 6 (modified by diatchki, 3 years ago) (diff)|
There is a new kind, Nat. It is completely separate from GHC's hierarchy of sub-kinds, so Nat is only a sub-kind of itself.
The inhabitants of Nat are an infinite family of (empty) types, corresponding to the natural numbers:
0, 1, 2, ... :: Nat
These types are linked to the value world by a small library with the following API:
module GHC.TypeNats where
We relate type-level natural numbers to run-time values via a family of singleton types:
data Nat (n :: Nat) nat :: NatI n => Nat n natToInteger :: Nat n -> Integer
The only value of type Nat n is the number n. (Technically, there is also an undefined element.)
class NatI n where nat :: Nat n instance NatI 0 where nat = "0" instance NatI 1 where nat = "1" instance NatI 2 where nat = "2" etc.
type family m ^ n :: Nat type family m * n :: Nat type family m + n :: Nat class m <= n
data Natural = forall n . Natural !(Nat n) data NaturalInteger = Negative Natural | NonNegative Natural toNaturalInteger :: Integer -> NaturalInteger subNatural :: Natural -> Natural -> NaturalInteger