by Nicolas Wu

Posted on 11 November 2010

Tags: Haskell

This article is an introduction to polymorphic mapping, with ideas taken from the second section of Polytypic Values Possess Polykinded Types by Ralf Hinze.

Although relatively simple, the `List`

is one of the most widely used datastructures in programs written in a functional style:

`> data List a = Nil | Cons a (List a)`

One of the first interesting operators which one encounters when learning about lists is the `map`

function, which applies a function to all the elements in a list. Here’s a slightly different rendition of this function:

```
> map_List :: (a -> a') -> List a -> List a'
> map_List map_a Nil = Nil
> map_List map_a (Cons a list) = Cons a' list'
> where
> a' = map_a a
> list' = map_List map_a list
```

This mapping function makes use of `map_a`

, which can be thought of as the mapping which is specific to values of type `a`

. Understanding the definition of a `map`

in this way will help with our generalisation to higher order types.

A different representation of lists is in terms of the function `Mu`

(which is normally written \(μ\), and forms the Initial F-Algebra):

`> data Mu f = In { out :: f (Mu f) }`

Here the types `Mu f`

and `f (Mu f)`

are isomorphic, with the two different directions of the isomorphism given by the functions `In`

and `out`

:

```
In :: f (Mu f) -> Mu f
out :: Mu f -> f (Mu f)
```

The recursive nature of the list type can be thought of as a fix point of `Mu`

using a base functor which explicitly marks the recursion:

`> data FList a list = FNil | FCons a list`

The type given by `Mu (FList a)`

is isomorphic to the familiar version of `List`

:

```
Mu (FList a)
= {- Using In and out -}
Flist (Mu (Flist a))
= {- Definition Flist -}
FNil | FCons a (Mu (Flist a))
= {- Induction hypothesis Mu (Flist a) = List a -}
Nil | Cons a (List a)
= {- Definition List -}
List a
```

This gives us the following alternative definition of `List`

using a type synonym:

`> type List' a = Mu (FList a)`

Our aim is to provide a definition of `map`

for this which follows the structure of the type itself.

How might we now define the `map_List`

function we saw earlier in terms of `List'`

?

To start with, let’s define the mapping function for the base functor `FList`

. The base functor takes two type arguments, `a`

, and `list`

, so it makes sense to provide a mapping function for each of these, and use them in a transformation from `FList a list`

to `FList a' list'`

:

```
> map_FList :: (a -> a') -> (list -> list')
> -> FList a list -> FList a' list'
> map_FList map_a map_list FNil = FNil
> map_FList map_a map_list (FCons a list) = FCons a' list'
> where
> a' = map_a a
> list' = map_list list
```

Here we can begin see why at the beginning of this article we phrased the definition of standard `map`

in such a strange way.

The really interesting part is the definition for mapping over `Mu f`

. The argument to `Mu`

is a type constructor `f :: * -> *`

and since this is a functor it must have a mapping function with the following signature:

`map_f :: (a -> a') -> f a -> f a'`

This provides us with enough information to generically map over `Mu`

, where the idea is to use `map_f`

to map over the contents of the `f`

in question. The value we wish to map over make use of `In`

as a data constructor and the really juicy part of this equation is `fa :: f (Mu f)`

:

```
> map_Mu :: forall f f'. (forall a a'. (a -> a') -> f a -> f' a')
> -> Mu f -> Mu f'
> map_Mu map_f (In fa) = In fa'
> where
> fa' = map_f (map_Mu map_f) fa
```

Admittedly, this definition is a little bit dense, so here’s some justification. The definition takes the function `map_f`

, which can transform values of type `f a`

to `f' a'`

so long as it is provided with a function of type `a -> a'`

. In this case, we have a value of type `f (Mu f)`

, and want to produce a value of type `f' (Mu f')`

and so must provide a function of type `Mu f -> Mu f'`

. This is precisely what `map_Mu map_f`

provides!

Finally, we can put these pieces together to provide a mapping function for `List'`

based on the structure of the type:

```
> map_List' :: (a -> a') -> List' a -> List' a'
> map_List' map_a = map_Mu (map_FList map_a)
```

Our hope is that this definition of `map`

in terms of the structure of `List'`

results in the same behaviour as the definition given for `List`

. To check this, we’ll start with a mapping on `In FNil`

, which is isomorphic to `Nil`

:

```
map_List' map_a (In FNil)
= {- definition map_List' -}
map_Mu (map_FList map_a) (In FNil)
= {- definition map_Mu -}
In (map_FList map_a (map_Mu (map_FList map_a)) FNil)
= {- definition map_FList -}
In FNil
```

So far, so good. Now let’s verify that `In (FCons a list)`

gives back what we expect:

```
map_List' map_a (In (FCons a list))
= {- definition map_List' -}
map_Mu (map_FList map_a) (In (FCons a list))
= {- definition map_Mu -}
In (map_FList map_a (map_Mu (map_FList map_a)) (FCons a list))
= {- definition map_FList -}
In (FCons (map_a a) ((map_Mu (map_FList map_a)) list))
= {- definition map_List' -}
In (FCons (map_a a) (map_List' map_a list))
```

Hurrah! Using the induction hypothesis, we can see that we’ve arrived back where we started, and our definition of `map_List'`

does indeed provide a result that’s isomorphic to a simple `map_List`

we wrote at the start of this article.

One question which you might rightly raise at this point is: why bother with all this machinery? Well, the definition of `Mu`

is really quite generic, which means that as long as we can provide a base functor of a type, including the mapping for that base functor, then we can automatically make use of the mapping for the type.

Of course, not all types fit this recursion scheme, but given the work found in Adjoint Folds and Unfolds, also by Ralf Hinze, (and an excellent read), this method can be generalised to encompass a much broader selection of types.