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

# The Problem

The type level numbers of kind `Nat` have no structure,
which limits their use in programs that need to overload
values based on a natural number, or use programmer-defined
type functions. Consider, for example, a class with a
parameter of kind `Nat`:

class C (n :: Nat) where someMethod :: ...

To define instances of this class, we need to either select a set of concrete numbers like this:

instance C 0 where ... instance C 1 where ...

Or, alternatively, we could provide a completely polymorphic instance:

instance C a where ...

Usually, neither of these is good enough: the first one is too restrictive as we have to enumerate all the instances that will ever be used explicitly, while the second one is too general and does not give us any static information about the type that we are using (i.e., we could define the method without using a class).

The same sort of thing happens if we try to use numbers of kind `Nat` as the parametr
to a type function---we often can't define the instances that we need.

# The Solution

We can solve this problem by providing an additional representation of type-level natural numbers,
one that has explicit structure. We define another kind, `Nat1`, which represents natural numbers
is the traditional unary representation (here we are using GHC's `DataKinds` extension):

data Nat1 = Zero | Succ Nat1

This kind makes it easy to define class instances or type-functions using natural numbers. For examples, here is a function that selects a type from a list of types:

type family Get (n :: Nat1) (xs :: [*]) :: * type instance Get Zero (x `: xs) = x type instance Get (Succ n) (x `: xs) = Get n xs

Such a function might be useful if we were defining some sort safe interface to a foreign struct:

getField :: Selector n -> Ptr (Struct fields) -> Ptr (Get n fields)

(This is just an example---to make this work for real we'd probably have to use a type class, so that we can determine the sizes of struct fields.)

Unfortunately, if `getField` was defined with this type signature, we
wouldn't be able to use it with the type-level natural number literals
because `Selector` expects a type of kind `Nat1` and not a `Nat`.

To work around this, we can provide a type-function that relates the two representations of natural numbers:

type family FromNat1 (n :: Nat1) :: Nat type instance FromNat1 Zero = 0 type instance FromNat1 (Succ n) = 1 + FromNat1 n

By using `FromNat1`, we can give `getField` a type that will allow
for the use of ordinary type-level literals:

getField :: Selector (FromNat1 n) -> Ptr (Struct fields) -> Ptr (Get n fields)

There is one final detail that needs to be explained: if we were to try the
definitions presented so far without any further modifications, we would get
ambiguity errors when trying to use `getField`. The reason for this is that
the type variable `n` appears only in arguments to type-functions so GHC
has no way to determine its value from the result of the type function.

The good news is that the function `FromNat1` is injective so, in fact,
it is possible to determine the input from the output. We modified GHC's
type checker to make it aware of this fact. These changes are captured
by the following two rules:

forall a b. (FromNat1 a ~ FromNat1 b) => (a ~ b) forall a. exists b. (1 <= FromNat1 a) => (a ~ Succ b)

Now the function `getField` type-checks as expected:

s :: Selector 2 p :: Ptr (Struct [Int,Char,Float]) f :: Ptr Float f = getField s p