#### Type-level functions using closed type families

- January 16, 2017
Kwang's Haskell Blog - Type-level functions using closed type families

# Type-level functions using closed type families

Posted on January 16, 2017 by Kwang Yul Seo

In this post, we will see how to write basic type-level functions using closed type families.

Before we start, let’s declare a bunch of GHC language extensions required to use type-level functions.

``````{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}``````

Also import required modules. `GHC.TypeLits` provides type-level natural numbers and symbols.

``````import GHC.TypeLits
import Data.Proxy``````

# Literals

Datatype promotion allows us to use `True` and `False` as type constructors whose kind is `Bool`. The quotes are used to emphasize the promotion, but can be omitted when syntactically unambiguous.

``````λ> :set -XDataKinds
λ> :kind 'True
'True :: Bool
λ> :kind 'False
'False :: Bool``````

We can also use numbers such as `1` and `2` as types. The kind of these numbers is `Nat`.

``````λ> :kind 1
1 :: Nat``````

# Type-level Function

`If` takes three arguments `c`, `t` and `e` and returns `t` if `c` is `True`, returns `e` otherwise. The kind of `If` is `Bool -> * -> * -> *`.

``````type family If c t e where
If 'True  t e = t
If 'False t e = e``````

We can use GHCi’s `kind!` command to evaluate type functions.

``````λ> :kind! If 'True Bool Char
If 'True Bool Char :: *
= Bool
λ> :kind! If 'False Int Double
If 'False Int Double :: *
= Double``````

# Type-level List

As we can promote types like `Bool`, we can also promote lists and treat `[]` as a kind constructor, and `[]` and `(:)` as types.

When `(:)` is seen as a type constructor, it has kind

``````λ> :kind (:)
(:) :: a -> [a] -> [a]``````

It means `(:)` is kind-polymorphic.

So we can create a type-level list of booleans as well as naturals.

``````λ> :kind [True, False]
[True, False] :: [Bool]
λ> :kind [1, 2]
[1,2] :: [Nat]``````

# Type-level List Function

The definition of type-level function `Length` is the same as the value level `length` function. If it an empty list returns 0. If it not empty, add 1 to the length of the tail.

``````type family Length xs where
Length '[]       = 0
Length (x ': xs) = 1 + Length xs``````

`0` and `1` are types of `Nat` kind and `(+)` is a type-level add function defined in `GHC.TypeLits`. We can even use `(:)` as a pattern here.

``````λ> :kind! Length [Char,Bool,Int]
Length [Char,Bool,Int] :: Nat
= 3``````

It seems `Length` is almost identical to the value level function `length`, but `Length` function is not kind-polymorphic by default. Thus passing `[1, 2, 3]` to `Length` causes an error.

``````λ> :kind! Length [1,2,3]

<interactive>:1:8: error:
• Expected kind ‘[*]’, but ‘'[1, 2, 3]’ has kind ‘[Nat]’
• In the first argument of ‘Length’, namely ‘'[1, 2, 3]’
In the type ‘Length '[1, 2, 3]’``````

To make it poly-kinded, we need to turn on `PolyKind` extension. The kind is inferred automatically, but we can also specify the kind with `k`.

``````type family Length (xs :: [k]) where
Length '[]       = 0
Length (x ': xs) = 1 + Length xs``````

`Head` and `Tail` are defined in a similar manner. Note that the kind of `xs` is explicitly annotated with `[*]` because they only work on type-level lists.

``````type family Head (xs :: [*]) where
Head (x ': xs) = x

type family Tail (xs :: [*]) where
Tail (x ': xs) = xs``````

We can see `Head` and `Tail` work as expected.

``````λ> :kind! Head [Char, Bool, Int]
Head [Char, Bool, Int] :: *
= Char
*Main
λ> :kind! Tail [Char, Bool, Int]
Tail [Char, Bool, Int] :: [*]
= '[Bool, Int]``````

One notable thing here is that both `Head` and `Tail` are partially defined. What if we pass `'[]` to `Head` or `Tail`?

``````λ> :kind! Head '[]

It seems GHC treats `Head '[]` as a valid type instead of emitting a type error. It is a bit mysterious, but at least we can see that type-level functions in Haskell can be partial and the behavior is not intuitive. Interested readers are referred to Richard Eisenberg’s What are type families? which discusses this issue in details.

# Higher-order Type-level List Function

It is even possible to define type-level map function. `Map` takes a type-level function `f` and a type-level list `xs`. It applies `f` to every element of `xs` and returns a new type-level list containing the results.

``````type family Map (f :: * -> *) (xs :: [*]) where
Map f '[]       = '[]
Map f (x ': xs) = f x ': Map f xs``````
``````λ> :kind! Map MakePair [Char,Bool,Int]
Map MakePair [Char,Bool,Int] :: [GHC.Types.*]
= '[(Char, Char), (Bool, Bool), (Int, Int)]``````

where the definition of `MakePair` is

``````type family MakePair (x :: *) where
MakePair x = (x, x)``````

# Wrap-up

So far we’ve covered only the basics of type-level datatypes and functions. Recent additions to GHC make it possible to explore the whole new world of dependent type programming in Haskell. Interested readers might want to take a look at the publications of Richard A. Eisenberg whose current work is to add dependent types to Haskell.

#### Learning Agda to be a better Haskell programmer

- February 21, 2014
Kwang's Haskell Blog - Learning Agda to be a better Haskell programmer

# Learning Agda to be a better Haskell programmer

Posted on February 21, 2014 by Kwang Yul Seo

In my previous post Learning Prolog to be a better Haskell programmer, I advocated learning Prolog is quite helpful to get more intuitions on Haskell type-level programming.

I think a good next step is to learn a dependent typed programming language such as Agda or Epigram. As learning Haskell is a good way to develop oneself as a better Java programmer, learning a dependent typed programming language is a good way to develop oneself as a better Haskell programmer.

Among many dependent typed programming languages, I recommend Agda simply because its surface syntax is quite similar to that of Haskell. Because dependent typed programming languages in general are not mature enough to perform day-to-day programming task and most of them are more or less equivalent in powers, choosing a syntactically familiar language helps you understand more advanced type system behind the syntax.

As the name “dependent type” implies, the biggest difference lies in the type system. While Haskell’s type system strictly splits values and types, Agda blurs the distinction between types and values. Type level programming in Haskell with type families or functional dependencies is esoteric at best, but type level programming in Agda is a norm.

For example, it is possible to define a type of lists of a certain length. In this setting, it is a type error to pass an empty list to head.

``````data Vec (A : Set) : Nat -> Set where
[] : Vec A zero
_::_ : {n : Nat} -> A -> Vec A n -> Vec A (suc n)

head : {A : Set}{n : Nat} -> Vec A (suc n) -> A
head (x :: xs) = x``````

Please refer to Dependently Typed Programming in Agda and Daniel Peebles’s introduction on Agda for more information on Agda.