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