Version 33 (modified by diatchki, 14 months ago)

--

## 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 -> *
```

For example, Sing 0, Sing 127, Sing "hello", Sing "this also}, are all singleton types. The intuition 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
```

The function fromSing has an interesting type: it maps singletons to ordinary values, but the type of the result depends on the kind of the singleton parameter. So, if we apply it to a value of type Sing 3 we get the number 3, but, if we apply it to a value of type Sing "hello" we would get the string "hello".

So, how do we make values of type Sing n in the first place? This is done with the special overloaded constant sing:

```class SingI a where
sing :: Sing a

-- Built-in instances for all type-literals.
instance SingI 0        where sing = ... the singleton value representing 0 ...
instance SingI 1        where sing = ... the singleton value representing 1 ...
instance SingI "hello"  where sing = ... the singleton value representing "hello" ...
// ... etc.
```

Here are some examples on the GHCi prompt to get a feel of how sing works:

```> :set -XDataKinds
> sing :: Sing 1
> 1
> sing :: Sing "hello"
> "hello"
```

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

• It is the introduction construct for 'Sing' values,
• It is an implicit singleton parameter (this is discussed in more detail bellow)

Notice that GHCi could display values of type Sing, so they have a Show instance. As another example, here is the definition of the Show instance:

```instance Show (SingRep a) => Show (Sing a) where
showsPrec p = showsPrec p . fromSing
```

Easy! We just convert the singleton into an ordinary value (integer or string), and use its Show instance to display it.

Next, we show two functions which make it easier to work with singleton types:

```withSing :: SingI a => (Sing a -> b) -> b
withSing f = f sing

singThat :: SingI a => (SingRep a -> Bool) -> Maybe (Sing a)
singThat p = withSing \$ \x -> if p (fromSing x) then Just x else Nothing
```

The first function, withSing, is useful when we want to work with the same singleton value multiple times. The constant sing is polymorphic, so every time we use it in a program, it may refer to a potentially different singleton, so to ensure that two singleton values are the same we have to resort to explicit type signatures, which just adds noise to a definition. By using, withSing we avoid this problem because we get an explicit (monomorphic) name for a given singleton, and so we can use the name many times without any type signatures. This technique is shown in the definition of the second function, singThat.

The function singThat is similar to the constant sing in that it defines new singleton values. However, it allows us to specify a predicate on (the representation of) the value and it only succeeds if this predicate holds. Here are some examples of how that works:

```> singThat (== 1) :: Maybe (Sing 1)
> Just 1
> singThat (== 1) :: Maybe (Sing 2)
> Nothing
> singThat ("he" `isPrefixOf`) :: Maybe (Sing "hello")
> Just "hello"
```

Now, using singThat we can show the definition of the Read instance for singletons:

```instance (SingI a, Read (SingRep a), Eq (SingRep a)) => Read (Sing a) where
case singThat (== x) of
Just y  -> [(y,ys)]
Nothing -> []
```

We use the Read instance of the representation for the singletons to parse a value, and then, we use singThat to make sure that this was the value corresponding to the singleton.

## 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.