On Wed, Mar 18, 2009 at 5:15 AM, Ryan Ingram
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