From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from majordomo@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id SAA30297; Wed, 13 Jun 2001 18:55:44 +0200 (MET DST) X-Authentication-Warning: pauillac.inria.fr: majordomo set sender to owner-caml-list@pauillac.inria.fr using -f Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id SAA30463 for ; Wed, 13 Jun 2001 18:55:43 +0200 (MET DST) Received: from sundown.cs.cornell.edu (sundown.cs.cornell.edu [128.84.96.20]) by nez-perce.inria.fr (8.11.1/8.10.0) with ESMTP id f5DGtgf14637 for ; Wed, 13 Jun 2001 18:55:42 +0200 (MET DST) Received: from cs.cornell.edu (dhcp99-221.cs.cornell.edu [128.84.99.221]) by sundown.cs.cornell.edu (8.11.3/8.11.3/R-3.5) with ESMTP id f5DGteC16071 for ; Wed, 13 Jun 2001 12:55:40 -0400 (EDT) Message-ID: <3B279ADB.B966DDD0@cs.cornell.edu> Date: Wed, 13 Jun 2001 12:54:51 -0400 From: Frederick Smith Organization: Cornell University X-Mailer: Mozilla 4.73 [en] (Win98; U) X-Accept-Language: en MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Evaluation Order References: <200106111303.JAA14369@sarg.Ryerson.CA> <3B265783.C386F97@ozemail.com.au> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: owner-caml-list@pauillac.inria.fr Precedence: bulk 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