Version 1 (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

data Nat (n :: Nat)                                     -- Abstract "singleton" types.

natToInteger :: Nat n -> Integer                        -- Convert a singleton to an integer.
integerToNat :: Integer -> (forall n. Nat n -> a) -> a  -- Convert an integer into a singleton.

class TypeNat n where
  nat :: Nat n                                          -- A value in a "singleton" type.

 instance TypeNat 0
 instance TypeNat 1
 instance TypeNat 2

-- property:  natToInteger (nat :: Nat n) == n