Version 14 (modified by diatchki, 4 years ago) (diff) |
---|

## Type-Level Naturals

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

## Singleton Types

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)

## Examples

Here is how we can use the basic primitives 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 :: NatI 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 NatI n => Read (Nat n) where readsPrec p x = do (x,xs) <- readsPrec p x case integerToMaybeNat x of Just n -> [(n,xs)] Nothing -> []

## Type-Level Operations

type family m ^ n :: Nat type family m * n :: Nat type family m + n :: Nat class m <= n

## Natural Numbers

data Natural = forall n . Natural !(Nat n) data NaturalInteger = Negative Natural | NonNegative Natural toNaturalInteger :: Integer -> NaturalInteger subNatural :: Natural -> Natural -> NaturalInteger