|Version 13 (modified by diatchki, 4 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. The value of a singleton type may be named using nat, which is a bit like a "smart" constructor for Nat n. Note that because nat is polymorphic, we may have to use a type signature to specify which singleton we mean. For example:
> natToInteger (nat :: Nat 3) 3
One may think of the smart constructor nat as being a method of a special built-in class, NatI:
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.
The name NatI is a mnemonic for the different uses of the class:
- It is the introduction construct for 'Nat' values,
- It is an implicit parameter of kind 'Nat' (this is discussed in more detail in a separate section)
Here is how we can use this API to define a Show instance for singleton types:
instance Show (Nat n) where showsPrec p n = showsPrec p (natToInteger n)
A more interesting example is to define a function which maps integers into singleton types:
integerToMaybeNat :: TypeNat n => Integer -> Maybe (Nat n) integerToMaybeNat x = check nat where check y = if x == natToInteger y then Just y else Nothing
The implementation of integerToMaybeNat is a little subtle: by using the helper function check, we ensure that the two occurrences of nat (aka y) both have the same type, namely Nat n. There are other ways to achieve the same, for example, by using scoped type variables, and providing explicit type signatures.
Now, we can use integerToNat to provide a Read instance for singleton types:
instance TypeNat n => Read (Nat n) where readsPrec p x = do (x,xs) <- readsPrec p x case integerToMaybeNat x of Just n -> [(n,xs)] Nothing -> 
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