Polymorphic Mapping

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.

Lists

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.

List Base Functor

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.

Mapping The Base

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.

Mapping Mu

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!

Functor Mapping

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.

Conclusion

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.

Comments