Version 28 (modified by diatchki, 5 years ago) (diff)

--

## Type-Level Literals

Currently, we support two forms of type-level literals: natural numbers, and symbol constants. Natural number literals are a family of types, all of which belong to the kind `Nat`. Similarly, symbol literals are types that belong to the kind `Symbol`:

```0, 1, 2, ... :: Nat
"hello", "world", "some string literal" :: Symbol
```

Both of numeric and symbol literal types are empty---they have no inhabitants. However, they may be used as parameters to other type constructors, which makes them useful.

## Singleton Types

We use this idea to link the type-level literals to specific run-time values via singleton types. The singleton types and some useful functions for working with them are defined in module `GHC.TypeLits`:

```module GHC.TypeLits where
```

A singleton type is simply a type that has only one interesting inhabitant. We define a whole family of singleton types, parameterized by type-level literals:

```newtype Sing :: a -> *
```

So, for example, `Sing 0`, `Sing 127`, `Sing "hello"`, `Sing "this also`}, are all singleton types. The idea is that the only inhabitant of `Sing n` is the value `n`. Notice that `Sing` has a polymorphic kind because sometimes we apply it to numbers (which are of kind `Nat`) and sometimes we apply it to symbols (which are of kind `Symbol`).

But, if we have a value of type `Sing a`, how do we get the actual integer or string? We can do this with the function `fromSing`:

```fromSing :: Sing a -> SingRep a

type family SingRep a
type instance SingRep (n :: Nat)    = Integer
type instance SingRep (n :: Symbol) = String
```

While the type of `fromSing` looks a bit complex at first it is actually quite simple: given a singleton type, it will return either an integer or a string, depending on the kind of its index. So, if we apply it to a value of type `Sing 3` we would get the number `3`, but, if we apply to a value of type `Sing "hello"` we would get the string "hello".

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

```data TNat :: Nat -> *

tNat         :: NatI n => TNat n
tNatInteger  :: TNat n -> Integer

-- Convenient derived functions
tNatThat     :: NatI n => (Integer -> Bool) -> Maybe (TNat n)
withTNat     :: NatI n => (TNat n -> a) -> a
```

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)
```

Here is how to define a `Read` instance:

```instance NatI n => Read (Nat n) where
case tNatThat (== x) of
Just n  -> [(n,xs)]
Nothing -> []
```

The derived function `tNatThat` is similar to `tNat` except that it succeeds only if the integer representation of the singleton type matches the given predicate. So, in the `Read` instance we parse an integer and then we check if it is the expected integer for the singleton that we are trying to parse.

## 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_c :: Storable a => ArrPtr n a -> a -> TNat n -> IO ()
memset_c (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_c` we used `tNatInteger` to get the concrete integer associated with the singleton type.

While the explicit `TNat` parameter is convenient when we define the function, it is a bit tedious to have to provide it all the time---it is easier to let the system infer the value, based on the type of the array:

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

The function `withTNat` is useful when converting from the "explicit" to the "implicit" style because it avoids ambiguity errors, scoped type-variables and other complications.