[Haskell-cafe] encoding for least fixpoint

[Dan Doel]

On Wednesday 18 March 2009 5:15:32 am Ryan Ingram wrote:
> There's something from Wadler's draft that doesn't make sense to me.  He
> says:
>
> > This introduces a new type, T = Lfix X. F X, satisfying the isomorphism
> > T ~ F T.  Note that it is an isomorphism, not an equality:  the type
> > comes equipped with functions in : T -> F T and out : F T -> T.
>
> While I was able to derive "in" for Lfix, and "out" for Gfix, I don't
> think it's possible to derive a generic "out" for Lfix or "in" for
> Gfix; maybe such a function *can* always be generated (specific to a
> particular type), but I don't think it's possible to do so while just
> relying on Functor.  Perhaps stronger generic programming methods are
> necessary.

The isomorphism comes from the fact that f (Nu/Mu f) is an f-(co)algebra.

  fmap l_in  :: Functor f => f (f (Mu f)) -> f (Mu f)
  fmap g_out :: Functor f => f (Nu f) -> f (f (Nu f))

Because of this and initiality/finality, there is a unique morphism from Mu f 
to f (Mu f), and from f (Nu f) to Nu f, namely:

  cata (fmap l_in) :: Functor f => Mu f -> f (Mu f)
  ana (fmap g_out) :: Functor f => f (Nu f) -> Nu f

where

  cata f (Lfix k) = k f
  ana g x = Gfix g x

Of course, this isomorphism is subject to caveats about bottom and seq in 
Haskell.

-- Dan