[Haskell-cafe] encoding for least fixpoint

[Ryan Ingram]

On Tue, Mar 17, 2009 at 4:36 PM, ben <benedikt.ahrens at gmx.net> wrote:
> Then I stumbled over a blog entry of Shin-Cheng Mu [2] and from there
> over an article of Wadler [3], where the least fixpoint is encoded as
>
> Lfix X. F X  =  All X. (F X -> X) -> X.
>
> and the greatest fixpoint as
>
> Gfix X. F X  =  Exists X. (X -> F X) * X.
>
> I would like to understand these definitions, or get an intuition about
> their meaning.

> Could somebody give some explanation or a pointer to a place where I can
> find one?

This is interesting.  So, there are two things going on.  First, we
only allow "x" to appear in positive form in f; for standard data
types in Haskell, this is equivalent to saying that you can write an
instance of Functor for f.  (I have an interesting proof of this which
I think I will write up for the Monad.Reader)

Once you have that, then you can get to defining fixed points on those
types.  Lfix encodes a fixed point by its fold.  For example, consider
this type:

> data Cell x xs = Nil | Cons x xs

Lfix (Cell a) is then equivalent to to (forall b. (Cell a b -> b) ->
b), which, if you expand the function argument by the case analysis on
Cell, you get (forall b. b -> (a -> b -> b) -> b); that is, foldr f z
xs = xs f z.

This is where the "for free" comes in to the description; it's like
the encoding of datatypes in System F without actual datatypes/case.
Let "Pair a b" be an abbreviation for "forall c. (a -> b -> c)", then
you have:

pair :: forall A B. a -> b -> Pair A B
pair = /\A B -> \a b -> /\C -> \k -> k a b

But in this case, instead of building simple datatypes, we are instead
building *recursive* datatypes, without actually requiring fixed
points in the language!

Gfix is similar, but instead of encoding a type by its fold, it
encodes it as a state machine.  So a Gfix ((,) Integer) stream of the
natural numbers could look something like this:  Gfix (\x -> (x, x+1))
0; the first element of the pair is the stream result, and the second
is the existential state which is used to generate the next pair.

For reference, here's some code implementing this concept.  Keep in
mind that we are working in a subset of Haskell without fixed points;
so no recursion is allowed.

{-# LANGUAGE ExistentialQuantification, RankNTypes #-}
module FixTypes where

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!

-- l_out :: Functor f => Lfix f -> f (Lfix f)

instance Functor (Either a) where
   fmap f (Left a) = Left a
   fmap f (Right x) = Right (f x)

test_l :: Lfix (Either Int)
test_l = Lfix (\k -> k $ Right $ k $ Right $ k $ Left 2)


data Gfix f = forall x. Gfix (x -> f x) x

g_out :: Functor f => Gfix f -> f (Gfix f)
g_out (Gfix f s) = fmap (\x -> Gfix f x) (f s)

-- g_in :: Functor f => f (Gfix f) -> Gfix f

instance Functor ((,) a) where
   fmap f ~(a,x) = (a, f x)

test_g :: Gfix ((,) Integer)
test_g = Gfix (\x -> (x, x+1)) 0

> [3]http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt

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.

  -- ryan