RE: optimization and purity

[Andrew Kennedy <akenn@microsoft.com>]

> -----Original Message-----
> From: Markus Mottl [mailto:mottl@miss.wu-wien.ac.at]
> Sent: Sunday, July 18, 1999 7:58 PM
> To: caml-list@inria.fr
> Subject: optimization and purity
> 
> 
> I would like to know whether anyone has already thought about means of
> indicating or inferring purity of functions.
> 
> 

You are indeed correct that knowing the purity of functions would permit a
number of optimisations such as the loop-hoisting example you present. There
was quite a bit of work on "effect inference" a few years back, though much
of it had a different motivation, namely to permit more expressions to be
given polymorphic types in the let construct (e.g. in the current revision
of Standard ML -- sorry I don't know the situation for CAML -- the
expression let val x = rev [] in (1::x, true::x) end is ill-typed even
though it would be sound to assign it the obvious type). I believe that the
MLj compiler, of which I am a developer, is the only ML compiler that
currently performs type-based effect inference and uses the results to
optimise code (I'd be happy to be contradicted here!). At present we have a
fairly crude set of effects:

  reads, writes, allocates, throws, loops

and the effect inference is also crude even though the *system* is quite
sophisticated (involving true subtyping induced by inclusion on sets of
effects). Expressions are divided into values (which syntactically are
effect-free) and computations (which might have side-effects). Computations
are given types that are annotated with their possible effects. Then we can
perform optimisations that depend on effect information (sorry about the SML
syntax):


(dead-code)
let val x = e1 in e2 end   -->   e2    
      if x not free in e2 
      and e1 has effect E for E \subseteq {reads,allocs}

(hoisting out of a function)
fn x => let val y = e1 in e2 end  -->   let val y = e1 in fn x => e2 end
      if e1 has the empty effect


(commuting computations)
let val x = e1 val y = e2 in e3 end --> let val y = e2 val x = e1 in e3 end
       if x,y not free in e1,e2
       and e1,e2 have effects E1,E2 
       such that E1,E2 \subseteq {reads,allocs,loops}
         OR E1 \subseteq {allocs,loops} and E2 \subseteq
{allocs,loops,writes}


Nick Benton and I have a paper submitted to HOOTS'99 on the theory of this
effect system in which we prove (e.g.) the equivalences listed above. If it
gets accepted I'll post a pointer to the final version. The bones of the
system can be seen in our ICFP'98 paper on MLj. I'll soon post a pointer to
that too if you like. Also in ICFP'98 you'll find Phil Wadler's paper on the
"marriage of effects and monads".

Note that the problem with many effect analyses of the past is that they
didn't consider termination. This is unfortunate, for you need to know
whether or not something might loop to use (for example) the first two of
the rewrites above. However, it's very hard to do a good job of inferring
termination behaviour -- in MLj, we basically assume that any recursive
function might loop. Notice also that recursion (and hence looping) can get
in by the back door -- two well-known routes are via recursive types and via
ref cells. Here's an example of the former:

datatype T = C of T->T;
val f = fn (y as C x) => x y;
val ouch = f (C f);

Hope this (partly) answers your question.

- Andrew.