|Version 8 (modified by diatchki, 5 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 "interesting" value of type Nat n is the number n. Technically, there is also an undefined element.
One may think of the smart constructor nat as being a method of a special built-in class:
class NatI n where nat :: Nat n instance NatI 0 where nat = "singleton 0 value" instance NatI 1 where nat = "singleton 1 value" instance NatI 2 where nat = "singleton 2 value" 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