# [Haskell-cafe] encoding for least fixpoint

Dan Doel dan.doel at gmail.com
Wed Mar 18 13:52:49 EDT 2009

On Wednesday 18 March 2009 5:28:35 am Duncan Coutts wrote:
> You can explain it to yourself (not a proof) by writing out the example
> for lists and co-lists along with fold for the list and unfold function
> for the co-list. Then write conversion functions between them. You can
> go from lists to co-lists using fold or unfold, but going from co-list
> to list requires general recursion. And that's the key of course. In
> Agda or something that distinguishes inductive and co-inductive types
> you could do the first two conversions but not the conversion in the
> other direction.

Yeah, I know how to show it can be done in Haskell. I meant more along the
lines of a proof (sketch) starting from a definition of a CPO category and
ending with the fact that initial algebras and terminal coalgebras are the
same.

Because, of course, in addition to going from, "we have general recursion,"
to, "least and greatest fixed points are the same," we can do the opposite:

fix :: (a -> a) -> a
fix = cata (\(f,fixf) -> f fixf) . ana (\f -> (f,f))

I suppose it's obvious that the least fixed point of 'F x = a*x' isn't empty
in a category like the one people use to model Haskell, because every type is
inhabited by at least one element, _|_. Once you have that as a base, you can
construct plenty of elements in ways that would be acceptable even in a total
language:

(1, _|_), (2, (1, _|_)), etc.

What remains is to show that you can get the infinite elements somehow (and
that the greatest fixed point has the above values, but seems less radical).

Anyhow, lastly I wanted to mention to ben that it's probably less hand-wavey
to explain where you get:

Mu F = forall x. (F x -> x) -> x

from by mentioning the paper Build, Augment and Destroy. Universally. That
develops a slightly tweaked semantics that takes as its basis, for some
functor F, essentially pairs (Mu' F, fold') where Mu' F is an F-algebra, and
fold' is obviously similar in function to the cata you get from an initial
algebra. You define a data type as a limit for such things, which gets you a
unique morphism that, when you finesse it back into haskell types, gives you:

build :: (forall x. (F x -> x) -> x) -> Mu F

And the paper of course goes on to show that initial algebras also fit with
this construction, and vice versa, so the two formulations are equivalent.
But, the above type looks a lot like the one we had for terminal coalgebras in
my last mail, so the definition:

newtype Mu f = Build (forall x. (f x -> x) -> x)

seems in order. I realize that was still pretty vague, but the paper gives a
rigorous treatment which should hopefully clear up the details.

(There's an analogous construction for greatest fixed points in the paper, but
it gets you

destroy :: (forall x. (x -> F x) -> x -> c) -> Nu f -> c

which gives you interesting ways to take apart coinductive objects, not build
them. Of course, I suppose you could recognize that this can be tweaked into:

destroy :: ((exists x. (x -> F x) * x) -> c) -> Nu f -> c

and further suppose that the above is just an identity function, modulo some
wrapping to make the type nice, which would get you to a similar place.)

Cheers,
-- Dan