RE: optimization and purity
 Andrew Kennedy
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  19990723 (17:00) 
From:  Andrew Kennedy <akenn@m...> 
Subject:  RE: optimization and purity 
> Original Message > From: Markus Mottl [mailto:mottl@miss.wuwien.ac.at] > Sent: Sunday, July 18, 1999 7:58 PM > To: camllist@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 loophoisting 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 illtyped 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 typebased 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 effectfree) and computations (which might have sideeffects). 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): (deadcode) 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 wellknown 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.