From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: weis Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id IAA14412 for caml-redistribution; Wed, 13 Oct 1999 08:51:02 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA12055 for ; Tue, 12 Oct 1999 16:59:16 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id QAA15859; Tue, 12 Oct 1999 16:59:10 +0200 (MET DST) Received: (from fpottier@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id QAA09998; Tue, 12 Oct 1999 16:59:10 +0200 (MET DST) Message-ID: <19991012165910.63590@pauillac.inria.fr> Date: Tue, 12 Oct 1999 16:59:10 +0200 From: Francois Pottier To: David Gurr Cc: caml-list@inria.fr, =?iso-8859-1?Q?Fran=E7ois_Pottier?= Subject: Re: the null pointer and subtyping References: <199910120147.SAA01669@swag.med.ge.com> Mime-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Transfer-Encoding: 8bit X-Mailer: Mutt 0.89.1 In-Reply-To: <199910120147.SAA01669@swag.med.ge.com>; from David Gurr on Mon, Oct 11, 1999 at 06:47:25PM -0700 Sender: weis Hi, Since you have mentioned Wallace, let me add a few comments. > ?let deref = function Some v -> v | None -> raise Uninit;; > > Variable deref defined with type [ None: Pre unit; Some: Pre %d; Abs ] -> > %d raises [ Uninit: Pre unit; Abs ] | { 0 < %d < 1 } The two main features of Wallace which are using here are open data types (data constructors can be freely mixed, hence we can have a type where Some is the only allowed data constructor, and another where both None and Some are allowed) and exception inference (which, by the way, is more powerful in the second release than shown above: ``deref (Some v)' is statically known to throw no exception). Also, notice that because exception information is part of types, it is possible to assert that such piece of code never raises such exception. (This feature may sound like Java, but is much more powerful, since polymorphism and full inference are available.) Open data types are also available in O'Labl, which is fully-fledged language, whereas Wallace is a mere prototype. O'Labl uses row polymorphism to implement them, whereas Wallace combines rows and subtyping, adding some expressive power. Exception inference of such precision is not currently part of any production language, as far as I know. However, Wallace isn't a production language, or even a proposal for language design; it is only a *type inference* testbench, something rather technical. More concretely, it contains a simple interactive loop, with a type inference engine. If some list readers want to play with it, go ahead, but don't expect to be programming in the large with it any time soon ;) > By moving to subtyping, Wallace can "allow null pointers". But Wallace > lets the programmer choose when and where to allow them and Wallace will > enforce the choice at compile time. Wallace *might* be a design sweet > spot. I'm afraid you may be a little over-optimistic. Indeed, having open data types allows you to *describe* some program invariants with more precision. However, it might still be very difficult (or impossible) for the type inference system to *automatically build a proof* of the invariants you have in mind. > I should add, a) in practice I find the addtional constraints > that Ocaml makes are usually what I want, so usually Wallace is harder > to use than Ocaml, b) making a good Wallace compiler is not simple. Definitely. In particular, regarding a), Wallace's usual policy is ``let the user know about everything'', which is usually not what you want, unless the user is itself an automatic tool, such as a compiler back-end. Best regards, -- François Pottier Francois.Pottier@inria.fr http://pauillac.inria.fr/~fpottier/