Jim's
Tutorials

Spring 2019
course
site

For values, the fix function looks something like fix f = f (fix f) and is a way of factoring the recursion out of a recursive definition. In general, given a recursive definition like

fac 0 = 1
fac n = n * fac (n - 1)

we can transform it into one that takes an argument through which it "recurses":

fac' self 0 = 1
fac' self n = n * self (n - 1)

We can then recover the recursive fac by fix fac'. We have essentially split out the logic of a single "layer" of the function and then used fix to recursively nest those layers.

It's natural to generalize this to types. By defining newtype Fix f = Roll (f (Fix f)), we can transform a recursive type like

data IntList = Nil | Cons Int IntList

into

data IntList' self = Nil' | Cons' Int self

and recover IntList as Fix IntList'; we can now write Cons 1 (Cons 2 (Cons 3 Nil))) as Roll (Cons' 1 (Roll (Cons' 2 (Roll (Cons' 3 (Roll Nil')))))). This would seem to do little other than increase the amount of indirection in the code, but it has the benefit of allowing the writing of highly generic functions!

To elaborate: Consider a structurally recursive function like this:

showElems Nil = ""
showElems (Cons n ns) = show n ++ ";" ++ showElems ns

A precise way of capturing the fact that the recursion is structural is to observe that the function can be decomposed into 1. recursing on the nested occurrences in its argument; 2. making use of the structure of the argument and the results of the recursions. In particular, we can represent the input to part 2, an IntList with any recursive occurrences replaced by their result after recursing, as a value of type IntList' String! We can then factor out part 2 as:

showElems' :: IntList' String -> String
showElems' Nil' = ""
showElems' (Cons' n r) = show n ++ ";" ++ r

This is one case of a general phenomenon: Given a type Foo which can be represented as Fix Foo' for an appropriate Foo', any structurally recursive function Foo -> X (for some result type X) can have its non-recursive portions factored out as something of type Foo' X -> X. And furthermore, if we represent Foo as Fix Foo' in the first place, and Foo' happens to have a Functor instance, then we can add back the recursion using this extremely generic function:

cata :: Functor f => (f a -> a) -> Fix f -> a
cata phi (Roll layer) = phi (fmap (cata phi) layer)

This adds verbosity and isn't particularly useful for simple cases like showElems, but this kind of genericity can sometimes be useful in more complicated situations. For example, here is a paper showing how to automatically derive a tail-recursive version of cata for a restricted class of fs.