[Haskell-cafe] encoding for least fixpoint

[Dan Doel]

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