Version 14 (modified by diatchki, 7 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
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
```