Polymorphic first class labels

(This post uses GHC 6.12.1)

The expression “first class labels” refers to the idea that, for record data types, one should be able to pass around the labels just as they would any other type. For instance, if I have a record like

data Foo a b = { biz :: a, baz :: b }


the value biz shouldn’t just denote the function biz :: Foo a b -> a, but should also be usable as a way of updating records, that is, a function like biz' :: Foo a b -> a' -> Foo a' b.

The Mythical Haskell’ includes some proposals for updating the records system with features aimed at supporting this idea, but for the time being, many people prefer to use fclabels, which achieves much of this magic using Template Haskell.

Recently, while working on an EDSL, I found myself wishing I had first class labels. I ran into a problem, though, which (along with solution) I’ll now describe.

Consider the following code:

module Label where

data Foo a b = Foo a b deriving Show

updatea :: a' -> Foo a b -> Foo a' b
updatea a (Foo _ b) = Foo a b

updateb :: b' -> Foo a b -> Foo a b'
updateb b (Foo a _) = Foo a b

worksFine foo0 = let foo1 = updatea 'a' foo0
                     foo2 = updatea "a" foo1
                 in foo2

Here I’ve defined a data structure Foo with two fields, along with a pair of functions for updating these fields. Then I defined a function worksFine which uses updatea to modify a Foo.

Obviously I could also write the following function:

worksFine' foo0 = let foo1 = updateb 'a' foo0
                      foo2 = updateb "a" foo1
                  in foo2


which is exactly the same, except that it uses updateb instead, thereby modifying the other field in Foo.

So now we have an obvious place to generalize: instead of having both worksFine and worksFine', why not have a single function which takes the updater as a parameter?

If we try it out, the first attempt looks like this:

trouble u foo0 = let foo1 = u 'a' foo0
                     foo2 = u "a" foo1
                 in foo2


Only trouble is that this fails to type check:

    Couldn't match expected type `[Char]' against inferred type `Char'
      Expected type: [Char] -> t1 -> t
      Inferred type: Char -> t2 -> t1
    In the expression: u "a" foo1
    In the definition of `foo2': foo2 = u "a" foo1

The problem is that trouble doesn’t believe that the argument u is polymorphic enough. This is a typical rank-2 issue: we don’t want trouble to bind the type variables in the signature for u.

Using rank-2 types, we can get very close to a solution. We can write the functions

alsoWorksFinea :: (forall a a' . a' -> Foo a b -> Foo a' b)
               -> Foo a b -> Foo [Char] b
alsoWorksFinea u foo0 = let foo1 = u 'a' foo0
                            foo2 = u "a" foo1
                        in foo2

alsoWorksFineb :: (forall b b' . b' -> Foo a b -> Foo a b')
               -> Foo a b -> Foo a [Char]
alsoWorksFineb u foo0 = let foo1 = u 'a' foo0
                            foo2 = u "a" foo1
                        in foo2

but neither is able to accept both of our update functions, even though each function has exactly the same body. Worse, I wasn’t able to find a sufficiently general type signature that would allow me to have one function which would be able to accept both update functions.

Luckily, where rank-2 types have failed me, type families have saved me. Any time you need more flexibility in your type signatures than the syntax will allow, you might be in a box where type families are the way to go. Here’s what it looked like in my case.

First I defined some typed to represent the two fields of my Foo structure:

data A = A
data B = B


Obviously I can pass around these values in a first-class manner, no trouble at all.

Then I defined a class for describing updating and getting:

class Field f x y where
  type Updated f x y
  update :: f -> x -> y -> Updated f x y
  type Gotten f y
  get :: f -> y -> Gotten f y

Now there are two instances to give, one for each field in Foo:

instance Field A a' (Foo a b) where
  type Updated A a' (Foo a b) = Foo a' b
  update A a' (Foo a b) = Foo a' b
  type Gotten A (Foo a b) = a
  get A (Foo a b) = a

instance Field B b' (Foo a b) where
  type Updated B b' (Foo a b) = Foo a b'
  update B b' (Foo a b) = Foo a b'
  type Gotten B (Foo a b) = b
  get B (Foo a b) = b 

And we’re basically done. We can now write the function that started this whole mess:

shouldWorkFine f foo0 = let foo1 = update f 'a' foo0
                            foo2 = update f "a" foo1
                        in foo2

GHCi is able to give us a very promising type signature for it:

> :t shouldWorkFine 
shouldWorkFine
  :: (Field f [Char] (Updated f Char y), Field f Char y) =>
     f -> y -> Updated f [Char] (Updated f Char y)

While this technique introduces type classes and type families into our program (something which can make typing troublesome in other areas), it delivers something I don’t know how to otherwise get: polymorphic first class labels.

Clearly the next step is to implement a library like fclabels which uses Template Haskell to define instances of the Field class.