Type-safe difference lists

Question

A common idiom in Haskell, difference lists, is to represent a list xs as the value (xs ++). Then (.) becomes "(++)" and id becomes "[]" (in fact this works for any monoid or category). Since we can compose functions in constant time, this gives us a nice way to efficiently build up lists by appending.

Unfortunately the type [a] -> [a] is way bigger than the type of functions of the form (xs ++) -- most functions on lists do something other than prepend to their argument.

One approach around this (as used in dlist) is to make a special DList type with a smart constructor. Another approach (as used in ShowS) is to not enforce the constraint anywhere and hope for the best. But is there a nice way of keeping all the desired properties of difference lists while using a type that's exactly the right size?

Answer 1

Yes!

We can view [a] as a free monad instance Free ((,) a) ().

Thus we can apply the scheme described by Edward Kmett in Free Monads for Less.

The type we'll get is

newtype F a = F { runF :: forall r. (() -> r) -> ((a, r) -> r) -> r } 

or simply

newtype F a = F { runF :: forall r. r -> (a -> r -> r) -> r } 

So runF is nothing else than the foldr function for our list!

This is called the Boehm-Berarducci encoding and it's isomorphic to the original data type (list) — so this is as small as you can possibly get.

---

Will Ness says:

So this type is still too "wide", it allows more than just prefixing - doesn't constrain the g function argument.

If I understood his argument correctly, he points out that you can apply the foldr (or runF) function to something different from [] and (:).

But I never claimed that you can use foldr-encoding only for concatenation. Indeed, as this name implies, you can use it to calculate any fold — and that's what Will Ness demonstrated.

It may become more clear if you forget for a moment that there's one true list type, [a]. There may be lots of list types — e.g. I can define one by

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

It's be different from, but isomorphic to [a].

The foldr-encoding above is just yet another encoding of lists, like List a or [a]. It is also isomorphic to [a], as evidenced by functions \l -> F (\a f -> foldr a f l) and \x -> runF [] (:) and the fact that their compositions (in either order) is identity. But you are not obliged to convert to [a] — you can convert to List directly, using \x -> runF x Nil Cons.

The important point is that F a doesn't contain an element that is not the foldr functions for some list — nor does it contain an element that is the foldr functions for more than one list (obviously).

Thus, it doesn't contain too few or too many elements — it contains precisely as many elements as needed to exactly represent all lists.

This is not true of the difference list encoding — for example, the reverse function is not an append operation for any list.