Re: [Caml-list] Evaluation Order

[Frederick Smith <fms@cs.cornell.edu>]

Someone asked earlier on this thread if anyone had ever suggested adding effects to
types.  I believe this idea was introduced by Lucassen and Gifford in POPL '88.
Since then there have been numerous papers, including some extending ML's type
inference to support effects (for example Andrew Wright's paper of 1992). Check out
http://citeseer.nj.nec.com/contextsummary/83989/0 for a list of over 50 papers
citing that first POPL paper.

I do not believe a simple effect annotation on function types, as suggested, would
suffice.  Although we may like to think of OCaml programs as effect free, they are
replete with effects: 1) I/O, 2) exceptions, and 3) non-termination.  It is
theoretically and practically infeasible to check that programs terminate.  Since
non-termination is usually not the source of programmer error, except perhaps when
writing multi-threaded applications, we may choose not to consider non-termination
a side-effect.  This pragmatic choice means that there will be programs whose
behavior depends on the order of evaluation.  If that is unacceptable, than it
would be best to fix the order of evaluation and let the compiler use the effect
analysis of its choice without burdening the user with additional annotations.
Have there been any studies showing the practical effect of fixing evaluation
order?  How bad is the performance penalty? How much can compiler analyses do to
minimize the impact?

If we choose to ignore non-termination but keep exceptions as effects then we face
the same problem as Java's throw clauses.  These throw annotations indicate which
exceptions a function may throw.  For large applications, it soon becomes the case
that nearly every function throws some kind of exception directly or indirectly.
Often the programmers know that those exceptions (NullPointer for example) will
never occur, but the type system cannot verify this fact.  Consequently, every
function contains a throws annotation making the annotations useless.  Similarly,
many OCaml functions especially in a deeply nested large application are likely to
raise exceptions.  Note that almost every one of the 2-list functions in the list
library raise exceptions.  Are you willing to wrap every call to List.for_all2 with
a handler?  How will you deal with the error?  Most likely by raising an
"impossible" exception and aborting the program :-).  Therefore it seems to me that
exceptions cannot be counted as side-effects either, increasing yet again the set
of programs whose behavior depends on order of evaluation.

If the real goal of the effect annotation is to prevent I/O from happening in an
unexpected order than a simple solution would be to implement the I/O libraries as
a monad. No extension of the type system or compiler would be necessary, although
we might want some syntactic sugar for convenience.  The connection between monads
and effects has been explored by Wadler.  Maybe someone with Haskell experience
could comment on how well monads work in practice?

In our project, order of evaluation surprised us in the pretty printer and later in
the assembler and disassembler.  It is dismaying to see these kinds of problems
arise in as friendly a language as OCaml.  I wish a solution were obvious.

-Fred


John Max Skaller wrote:

> Dave Mason wrote:
>
> > I think the answer is that the ``effect''ness isn't simply captured in
> > the type.  So the current type-inference engine would not be able to
> > do it.  It would require a bit of ad-hocery in the compiler.  That
> > doesn't mean that it's unsound, just that the existing compiler
> > mechanisms couldn't do it.
>
>         I think you probably _have_ to capture it in the type.
> Consider a new type
>
>         'a => 'b
>
> where '=>' means 'function with side effects'. Now consider
> the following two term constructors:
>
>         Apply(fn1,arg1)
>         Init(name,fn2,arg2)
>
> The type-checking rules are then clear:
>
>         fn1: 'a->'b, arg1:'a, Apply(fn1,arg1):'b
>         fn2: 'a=>'b, arg2:'a, name: 'b
>
> and
>
>         'a->'b is a subtype of 'a=>'b'
>
> In Felix it would be easy to verify correct usage,
> but I'm not sure it is possible to verify correct
> specification. In Ocaml, it may be harder, since
> one can use a function before declaration in a 'let rec',
> and it may be too late when spotting the type annotation
> to report a wrong usage.
>
> [OTOH, if the Ocaml compiler scanned 'let recs' for type
> annotations before examining bodies, it might improve
> error reporting in other circumstances??]
>
> --
> John (Max) Skaller, mailto:skaller@maxtal.com.au
> 10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
> checkout Vyper http://Vyper.sourceforge.net
> download Interscript http://Interscript.sourceforge.net
> -------------------
> Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
> To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr

-------------------
Bug reports: http://caml.inria.fr/bin/caml-bugs  FAQ: http://caml.inria.fr/FAQ/
To unsubscribe, mail caml-list-request@inria.fr  Archives: http://caml.inria.fr