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 _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
