fixed point
Josef Svenningsson
josefs at cs.chalmers.se
Wed Oct 29 11:48:52 EST 2003
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
More information about the Haskell-Cafe
mailing list