[Haskell-cafe] encoding for least fixpoint
Dan Doel
dan.doel at gmail.com
Wed Mar 18 16:29:43 EDT 2009
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
More information about the Haskell-Cafe
mailing list