[Haskell-cafe] encoding for least fixpoint
David Menendez
dave at zednenem.com
Wed Mar 18 11:10:23 EDT 2009
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/>
More information about the Haskell-Cafe
mailing list