> 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).

The Caml FAQ explains the problem, its solution in Caml, and why it is
considered a good solution. See
http://pauillac.inria.fr/caml/FAQ/FAQ_EXPERT-eng.html

This mailing list archives contain an article about the history of the
problem, http://pauillac.inria.fr/caml/caml-list/0485.html. It states
that the Caml implementors impulsed a new interest on the subject by
writing papers as soon as 1990.

This article also recalls that the Caml compiler incorporates the
restriction of polymorphism to non expansive expressions since 1995
(Caml-Light 0.7), even before Andrew Wright's article was published.

Best regards,

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/