On Wed, Mar 18, 2009 at 5:15 AM, Ryan Ingram <[email protected]> wrote: > newtype Lfix f = Lfix (forall x. (f x -> x) -> x) > > l_in :: Functor f => f (Lfix f) -> Lfix f > l_in fl = Lfix (\k -> k (fmap (\(Lfix j) -> j k) fl)) > -- derivation of l_in was complicated!
I found l_in easiest to write in terms of cata and build. cata :: (f a -> a) -> Lfix f -> a cata f (Lfix t) = f t build :: (forall x. (f x -> x) -> c -> x) -> c -> Lfix f build t c = Lfix (\f -> t f c) l_in :: Functor f => f (Lfix f) -> Lfix f l_in = build (\f -> f . fmap (cata f)) And, dually, ana :: (a -> f a) -> a -> Gfix f ana f a = Gfix f a destroy :: (forall x. (x -> f x) -> x -> c) -> Gfix f -> c destroy t (Gfix f x) = t f x g_out :: Functor f => Gfix f -> f (Gfix f) g_out = destroy (\f -> fmap (ana f) . f) > 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. l_out :: Functor f => Lfix f -> f (Lfix f) l_out = cata (fmap l_in) g_in :: Functor f => f (Gfix f) -> Gfix f g_in = ana (fmap g_out) -- Dave Menendez <[email protected]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
