Version 23 (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.TypeLits where

## Singleton Types

We relate type-level natural numbers to run-time values via a family of singleton types:

data TNat (n :: Nat) tNat :: NatI n => TNat n tNatInteger :: TNat n -> Integer

The only "interesting" value of type *TNat n* is the number *n*. Technically, there is also an undefined element.
The value of a singleton type may be named using *tNat*, which is a bit like a "smart" constructor for *TNat n*.
Note that because *tNat* is polymorphic, we may have to use a type signature to specify which singleton we mean. For example:

> :set -XDataKinds > tNatInteger (tNat :: TNat 3) 3

One may think of the smart constructor *tNat* as being a method of a special built-in class, *NatI*:

class NatI n where tNat :: TNat n instance NatI 0 where tNat = ...singleton 0 value... instance NatI 1 where tNat = ...singleton 1 value... instance NatI 2 where tNat = ...singleton 2 value... etc.

The name *NatI* is a mnemonic for the different uses of the class:

- It is the
*introduction*construct for 'TNat' values, - It is an
*implicit*parameter of kind 'TNat' (this is discussed in more detail bellow)

## Examples

Here is how we can use the basic primitives to define a `Show` instance for singleton types:

instance Show (TNat n) where showsPrec p n = showsPrec p (tNatInteger n)

A more interesting example is to define a function which maps integers into singleton types:

integerToMaybeNat :: NatI n => Integer -> Maybe (TNat n) integerToMaybeNat x = tNatThat (== x)

It checks that the value argument `x`, passed at runtime, matches the statically-expected value, returning `Nothing` if not, and a typed singleton if so.

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,
thus:

integerToMaybeNat :: forall n. NatI n => Integer -> Maybe (Nat n) integerToMaybeNat x | x == natToInteger (nat :: Nat n) = Just nat | otherwise = Nothing

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 -> []

## Implicit vs. Explicit Parameters

There are two different styles of writing functions which need the integer corresponding to a type level natural. To illustrate the two style consider a type for working with C-style arrays:

newtype ArrPtr (n :: Nat) a = ArrPtr (Ptr a)

One approach is to use an explicit parameter of type `TNat n`. For example:

memset :: Storable a => ArrPtr n a -> a -> TNat n -> IO () memset (ArrPtr p) a n = mapM_ (\i -> pokeElemOff p i a) [ 0 .. fromIntegral (tNatInteger n - 1) ]

This style is, basically, a more typed version of what is found in many standard C libraries.
Callers of this function have to pass the size of the array explicitly, and the type system checks that the
size matches that of the array. Note that in the implementation of `memset` we used `tNatInteger`
to get the concrete integer associated with the singleton type.

Another approach is to let the system infer the parameter by using the class `NatI`. For example:

memsetAuto :: (Storable a, NatI n) => ArrPtr n a -> a -> IO () memsetAuto ptr a = withTNat (memset arr a)

In this style, the caller of the function does not need to provide the size of the array explicitly.
Instead, it is computed automatically from the type of the array.
When defining `memsetAuto` we can use `{tNat`, the method of `NatI`, to get access to the value
corresponding to the type level natural.

When using the implicit style, it is important that the type of `tNat` is specified precisely. Failing to do so typically results in ambiguity errors
(i.e., GHC does not know which integer it should use). Another common mistake is to forget that 'tNat' is a polymorphic value and so every time it is used it may refer to a different value.

An easy way to avoid such problems is to implement the implicit style functions in terms of the explicit ones. The ba

memsetAuto arr val = memset arr val nat