Date: Tue, 12 Oct 1999 16:59:10 +0200
From: Francois Pottier <Francois.Pottier@inria.fr>
To: David Gurr <gurr@pop.mrs.med.ge.com>
Subject: Re: the null pointer and subtyping
In-Reply-To: <199910120147.SAA01669@swag.med.ge.com>; from David Gurr on Mon, Oct 11, 1999 at 06:47:25PM -0700
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/
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:27 MET