# fixed point

Josef Svenningsson josefs at cs.chalmers.se
Tue Oct 28 11:56:21 EST 2003

Sorry about replying to my own mail.

On Mon, 27 Oct 2003, Josef Svenningsson wrote:

> On Mon, 27 Oct 2003, Paul Hudak wrote:
>
> > Thomas L. Bevan wrote:
> >  > Is there a simple transformation that can be applied to all
> >  > recursive functions to render them non-recursive with fix.
> >
> > Suppose you have a LET expression with a set of (possibly mutually
> > recursive) equations such as:
> >
> > let f1 = e1
> >      f2 = e2
> >      ...
> >      fn = en
> > in e
> >
> > The following is then equivalent to the above, assuming that g is not
> > free in e or any of the ei:
> >
> > let (f1,...,fn) = fix g
> >      g ~(f1,...,fn) = (e1,...,en)
> > in e
> >
> > Note that all recursion introduced by the top-most LET has been removed
> > (or, if you will, concentrated into the one application of fix).  This
> > transformation will work even if there is no recursion, and even if some
> > of the fi are not functions (for example they could be recursively
> > defined lazy data structures).
> >
> 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.

All the best,

/Josef