RE: optimization and purity

[Simon Helsen <helsen@informatik.uni-freiburg.de>]

Hi,

>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

indeed, there used to be a semantic-based approach to figure out about
polymorphic references (using imperative variables), but they did not say
anything about the purity of a function. Moreover, the scheme was
difficult to use and hence abandoned (see earlier discussions on this list
and comp.lang.ml - subject value polymorphism) 

>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

It depends on how you view it. The ML Kit also performs a region/type
based effect analysis, but to implement compile-time garbage collection. 
I don't know if they use it to perform low-level optimisations

However, quite related to compilation is partial evaluation (or program
specialisation). There you can use an effect analysis to classify more
program parts as static, i.e. executable at partial evaluation time. 
Indeed, such a technique has been incorporated in the PGG system, a
partial evaluator for the full Scheme language
(http://www.informatik.uni-freiburg.de/proglang/software/pgg/). It is the
only PE system (of which I know of) which uses such a type-based effect
analysis to specialize impure code at partial evaluation time. In fact, we
are now exploring new opportunities in Region/Effect analysis to produce a
powerful partial evaluator for (Standard - sorry) ML. 

>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

The problem of termination is equally there in partial evaluation. In PE
this issue is treated separately from impurity though, as it may occur in
pure code as well. Moreover, as you indicate, it is substantially more
difficult. In general, a partial evaluator guarantees to preserve
the semantics (including termination behaviour). What it usually does not
guarantee is to terminate itself. This is something where PE departs from
standard compilation and that may have consequences to what level of
optimisations you can put through. In fact, a PE system can be considered 
an aggresive program optimizer which performs function unfolding and
aggressive constant propagation.

cheers,

	Simon