[Haskell-cafe] Scrap your rolls/unrolls

[Max Bolingbroke]

Hi Cafe,

In generic programming, e.g. as in "Data Types a la Carte" and Compos,
you often wish to work with data types in their fix-point of a functor
form. For example:

"""
data ListF a rec = Nil | Cons a rec
newtype List a = Roll { unroll :: ListF a (List a) }
"""

In some presentations, this is done by factoring the fix point like so:

"""
newtype FixF f = Roll { unroll :: f (FixF f) }
type List a = FixF (ListF a)
"""

This is all well and good, but it means when working with data types
defined in this manner you have to write Roll and unroll everywhere.
This is tedious :-(

Something I have long wished for is equirecursion, which would let you
write this instead:

"""
type List a = ListF a (List a)
"""

Note that we now have a type instead of a newtype, so we won't need to
write any injection/extraction operators. However, currently GHC
rightly rejects this with a complaint about a cycle in type synonym
declarations.

However, you can use type families to hide the cycle from GHC:

"""
type List a = ListF a (Force (ListThunk a))
data ListThunk a
type family Force a
type instance Force (ListThunk a) = List a
"""

Unfortunately, this requires UndecidableInstances (the type instance
RHS is not smaller than the instance head). And indeed when we turn
that extension on, GHC goes into a loop, so this may not seem very
useful.

However, we can make this slight modification to the data type to make
things work again:

"""
data ListF a rec = Nil | Cons a (Force rec)
type List a = ListF a (ListThunk a)
"""

Note that the application of Force has moved into the *use site* of
rec rather than the *application site*. This now requires no
extensions other than TypeFamilies, and the client code of the library
is beautiful (i.e. has no rolls/unrolls):

"""
example, ones :: List Int
example = Cons 1 (Cons 2 Nil)
ones = Cons 1 ones
"""

We can factor this trick into a fix point combinator that does not
require roll/unroll:

"""
type Fix f = f (FixThunk f)
type List a = Fix (ListF a)
data FixThunk f
type family Force a
type instance Force (FixThunk f) = Fix f
"""

The annoying part of this exercise is the the presence of a "Force" in
the functor definition (e.g ListF) means that you can't make them into
actual Functor instances! The fmap definition gives you a function of
type (a -> b) and you need one of type (Force a -> Force b). However,
you can make them into a category-extras:Control.Functor.QFunctor
instance (http://hackage.haskell.org/packages/archive/category-extras/0.53.5/doc/html/Control-Functor.html)
by choosing the "s" Category to be:

"""
newtype ForceCat a b = ForceCat { unForceCat :: Force a -> Force b }

instance Category ForceCat where
  id = ForceCat id
  ForceCat f . ForceCat g = ForceCat (f . g)
"""

Rather than the usual "Hask" Category which is used in the standard
Functor. This is somewhat unsatisfying, but I'm not sure there is a
better way.

I haven't seen this trick to "emulate equirecursion" before. Has it
showed up anywhere else?

Cheers,
Max