# type-prelude and GHC 7.6.1

The new release of GHC has many new features. Deferred type errors are very useful but the other features are a lot more fun. It is now a lot easier to encode invariants, information and computation at the type level. How much of the prelude can be ported, and how difficult is it to port?

All the code from this article is available in the type-prelude package on hackage.

## Integer

The prelude has an Integer type that can represent any positive or negative integer. GHC has a new feature, data kind promotion, which automatically promotes data types and constructors into data kinds and types when it is possible. It is not possible to promote this type because its implementation is hidden.

GHC has a Nat kind which allows any natural number to be used as a type, but they cannot be used to replace Integer.

The `Prelude.Type.Integer`

module provides the `Integer`

kind, implemented as an unbounded list of bits using twos-complement. The `I`

class converts small `Nat`

s into Integers.

```
data Integer = One Integer | Zero Integer | Ones | Zeros
type family I (a :: Nat) :: Integer
type instance I 0 = Zeros
type instance I 1 = One Zeros
type instance I 2 = Zero (One (Zeros))
type instance I 3 = One (One Zeros)
type instance I 4 = Zero (Zero (One Zeros))
```

Three extra type functions allow working with `Integer`

s as if they really were lists of `Bool`

s.

```
type family IntegerHead (i :: Integer) :: Bool
type family IntegerTail (i :: Integer) :: Integer
type family IntegerCons (b :: Bool) (i :: Integer) :: Integer
```

Most of the functions and operators from `Num`

and `Integral`

can be implemented very easily for this `Integer`

kind. For example:

```
type family Negate (a :: k) :: k
type instance Negate a = Complement a + I 1
type family (a :: k) * (b :: k) :: k
type instance Zeros * j = Zeros
type instance Ones * j = Negate j
type instance (Zero i) * j = IntegerCons False (i * j)
type instance (One i) * j = j + IntegerCons False (i * j)
```

## Proxy

Constructors, when promoted, become types. But these types do not have any values. The `Prelude.Type.Value`

provides the `T`

type (known elsewhere as `Proxy`

).

`data T a = T`

It also provides a method of converting a `T`

into the value of its associated type.

`class Value (a :: k) (t :: *) | k -> t where value :: T a -> t`

The `Value`

instances for Integers converts each constructor into its corresponding value.

```
instance Value Zeros Prelude.Integer where value _ = 0
instance Value Ones Prelude.Integer where value _ = -1
instance (Value i Prelude.Integer) => Value (One i) Prelude.Integer
where value _ = shift (value (T::T i)) 1 Prelude.+ 1
instance (Value i Prelude.Integer) => Value (Zero i) Prelude.Integer
where value _ = shift (value (T::T i)) 1
```

The `T::T`

idiom is very common in code that uses `Prelude.Type`

. It is made even more useful when using the `Show`

instance for `T`

.

```
instance (Value a t, Prelude.Show t) => Prelude.Show (T a) where
show _ = Prelude.show (value (T::T a))
```

It allows easy type-level programming in ghci.

```
Prelude.Type> T::T (One (Zero Ones))
-3
```

## Lists

The list type has two well known constructors which GHC promotes into types. To avoid confusion, the cons and nil types need to be prefixed with a single quote.

Converting list functions into type-level functions is often very straightforward. For example, the last function can be written like this.

```
type family Last (a :: [k]) :: k
type instance Last '[] = Error "Last_: empty list"
type instance Last (x ': y ': xs) = Last (y ': xs)
type instance Last (x ': '[]) = x
```

And it works:

```
Prelude.Type.Families> T::T (Last [1,2,3])
3
```

## Type Families vs Type Classes

The `Last`

function can also be implemented as a type class.

```
class Last (l :: [a]) (x :: a) | l -> x
instance Error "Last: empty list" => Last '[] a
instance a ~ b => Last '[a] b
instance Last (y ': xs) a => Last (x ': y ': xs) a
```

But classes need to be used differently.

```
Prelude.Type> T :: Last [1,2,3] a => T a
3
```

Thanks to Constraint kinds, we can add a Value instance for simple constraints.

```
instance (c a, Value a t) => Value (c :: k -> Constraint) t
where value _ = value (T::T a)
```

Now we can use the `Last`

class in the exact same way we used the `Last`

type family.

```
Prelude.Type> T::T (Last [1,2,3])
3
```

Code written using type families often looks nicer, so why use type classes and functional dependencies? Because we can not (yet?) partially apply type families. However type classes do not mind being partially applied. We can easily write higher order type classes such as `FoldR`

.

```
class FoldR (f :: a -> b -> b -> Constraint)
(nil :: b) (list :: [a]) (ret :: b) | f nil list -> ret
instance Id nil ret => FoldR f nil '[] ret
instance (FoldR f nil xs tail, f x tail ret)
=> FoldR f nil (x ': xs) ret
```

`FoldR`

can be used to implement `Or`

.

`type Or = FoldR (||) '[]`

`Or`

can be used to implement `Any`

.

`type Any = (Compose1 Or) `Compose2` Partial1 Map`

Partial application of type classes does not work exactly the same way as in regular Haskell, which is why the `Compose`

class (corresponding to (.)) has many variants. Each variant has a different arity. But it still works.

```
Prelude.Type> T::T (Any ((==) 1) '[3,2,1])
True
```

## If and Case

To make type-level programming easier, `Prelude.Type`

also provides `If`

and `Case`

classes. For example, `Case`

is used to implement `Ord`

.

```
class Compare (a :: k) (b :: k) (o :: Ordering) | a b -> o
class ((a :: k) < (b :: k)) (p :: Bool) | a b -> p
instance (Compare a b o,
Case o [LT --> True ~ p,
Otherwise (False ~ p)])
=> (a < b) p
```

And If is used to implement `Enum`

for `Integer`

s.

```
instance If (b < a) (l ~ '[])
(((I 1) + a) c, EnumFromTo c b k, l ~ (a ': k))
=> EnumFromTo (a :: Integer) b l
```

## Extras

`Prelude.Type`

contains a port of most of the functions from the Prelude that operate on `Bool`

, `Integer`

, lists and functions.

For fun, it also provides the `Main`

type alias for writing executables entirely on the type level.

```
{-# LANGUAGE DataKinds, FlexibleInstances, MultiParamTypeClasses,
FlexibleContexts, UndecidableInstances, KindSignatures #-}
module Main (main) where
import Prelude.Type
instance Gcd (I 12) (I 10) a
=> Main a
```

```
$ ghc Main.hs
$ ./Main.hs
2
```