From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id PAA31966 for caml-redistribution@pauillac.inria.fr; Tue, 21 Mar 2000 15:33:12 +0100 (MET) Resent-Message-Id: <200003211433.PAA31966@pauillac.inria.fr> 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 EAA12638 for ; Mon, 20 Mar 2000 04:10:07 +0100 (MET) Received: from suburbia.net (suburbia.net [203.4.184.1]) by nez-perce.inria.fr (8.8.7/8.8.7) with ESMTP id EAA03596 for ; Mon, 20 Mar 2000 04:10:03 +0100 (MET) Received: by suburbia.net (Postfix, from userid 110) id D303B6C564; Mon, 20 Mar 2000 14:10:00 +1100 (EST) Sender: proff@suburbia.net To: caml-list@inria.fr Subject: types, determination, seperate compilation and side effects Cc: proff@iq.org From: Julian Assange Date: 20 Mar 2000 14:10:00 +1100 Message-ID: MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Resent-From: weis@pauillac.inria.fr Resent-Date: Tue, 21 Mar 2000 15:33:12 +0100 Resent-To: caml-redistribution@pauillac.inria.fr It would be nice if the hindley-milner type system of ocaml were extended to provide unioning of determination, world-state-changes, mutagenic behavior etc as types. That is, if a function is discovered to lack referential transparency, either because it has side effects or calls functions which have side effects then that fact is reflected in the type of the function. This would permit the optimiser to perform code-flow elimination accross modules (and might make flow analysis within the same module easier). It is quite interesting to consider multiple argument functions. In ocaml multiple argument functions are rearranged into multiple curried forms. Type analysis of each form, as above, could result in elimination of that form if it has been typed as referentially transparent and found not to contribute to the calculation it was called from. Code flow analysis could do this already (theoretically), but not accross seperately compiled modules. It would be very useful for ocaml hackers to see if a non referentially transparent type was inferred for a function (and whether the cause was io, potential non-termination, or operation on mutables) or have the compiler discover conflicts between functions hand annotated as referentially transparent but inferred otherwise. I'm not sure how functions which potentially raise exceptions should be typed. Mercury (souped up prolog with functional desires from Melbourne University) supports determinacy annotations and checking, but the methodes employed are verbose and visually unpleasant. However, the designers do say that this has allowed them to catch several hundred errors during the development of the Mercury compiler and given the opimiser enough contraints to dramatically improve the speed of generated code (and it does generate fast code in an absolute sense, so there must be some truth in this). Cheers, Julian.