[Haskell-cafe] encoding for least fixpoint

[David Menendez]

On Wed, Mar 18, 2009 at 5:15 AM, Ryan Ingram <ryani.spam at gmail.com> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>