fixed point

[Josef Svenningsson]

On Tue, 28 Oct 2003, Ross Paterson wrote:

> 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)
>
I see. It's a little annoying that one would have to write a special fix
for every such function. I suppose an impredicative type system whould
help here.

	/Josef