fixed point

[Ross Paterson]

On Tue, Oct 28, 2003 at 11:56:21AM +0100, Josef Svenningsson wrote:
> On Mon, 27 Oct 2003, Josef Svenningsson wrote:
> > This is a very nice technique. As an exercise to the reader I suggest the
> > following program:
> >
> > \being{code}
> > data Tree a = Branch a (Tree (a,a)) | Leaf
> >
> > cross f (a,b) = (f a,f b)
> >
> > main1 =
> >   let mapTree :: (a -> b) -> Tree a -> Tree b
> >       mapTree = \f tree -> case tree of
> >                             Branch a t -> Branch (f a) (mapTree (cross f) t)
> >                             Leaf -> Leaf
> >   in mapTree id (Branch 42 Leaf)
> > \end{code}
> >
> I realise I was perhaps a bit dense in my previous mail. It was not my
> intention to try to sound smart. Sorry for that.
> 
> Does anyone know how to apply the transformation suggested by Paul Hudak
> to my program and make it typecheck? Does there exist a type system where
> the transformed program typechecks? I suppose so but I don't quite know
> what it would look like.

Polymorphic recursion implies a fix with a rank 3 type.  GHC can handle
those, but each one needs its own declaration, as in

	type MapTree = forall a b. (a -> b) -> Tree a -> Tree b

	fixMT :: (MapTree -> MapTree) -> MapTree
	fixMT f = f (fixMT f)

	mapTree' = fixMT (\ (mapTree :: MapTree) -> \f tree -> case tree of
			    Branch a t -> Branch (f a) (mapTree (cross f) t)
			    Leaf -> Leaf)