the null pointer and subtyping

the null pointer and subtyping

[David Gurr]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 4410 bytes --]

(Sorry no French version.  OK to reply to me in French for revenge.)

I've been playing with François Pottier's Wallace
<http://pauillac.inria.fr/~fpottier/> and considering the virtues of
subtyping in practice.  I thought that the following might be of interest.

# type a = { data : float option };;
type a = { data: float option }
# exception Uninit;;
exception Uninit
# let deref = function Some v -> v | None -> Uninit;;
val deref : exn option -> exn = <fun>
 
But we want "val deref : 'a option -> 'a". So:

# let deref = function Some v -> v ;;
Warning: this pattern-matching is not exhaustive.
val deref : 'a option -> 'a = <fun>
# deref { data = Some 99.9 }.data;;
- : float = 99.9
# deref { data = None }.data;;
Uncaught exception: Match_failure("", 12, 29)

So:

# let deref = try (function Some v -> v) with Match_failure _ -> Uninit;;
Warning: this pattern-matching is not exhaustive.
This expression has type exn but is here used with type 'a option -> 'a

Back to where we started. OK, try Wallace.  Wallace infers type 
declarations so we skip them.

?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 }
Executing... deref = <prim>

?let x = { data = None };;

Variable x defined with type { data: Pre [ None: Pre unit; Abs ]; Abs }
Executing... x = { data = None () }

?deref (x.data);;

Variable _unnamed defined with type 0
Executing... Uncaught user exception: Uninit ()

?deref ((x.data <- (Some 99.9)).data);;

Variable _unnamed defined with type float
Executing... _unnamed = 99.9

But suppose that instead we define deref without testing for None:

let deref = function Some v -> v ;;

Variable deref defined with type [ Some: Pre %d; Abs ] -> 
%d raises 0 | { 0 < %d < 1 }
Executing... deref = <fun>

?let x = { data = None };;

Variable x defined with type { data: Pre [ None: Pre unit; Abs ]; Abs }
Executing... x = { data = None () }

?deref (x.data);;

Inconsistent constraint:
'd < 'c -> 'b raises 'a
'g -> 'f raises 'e < 'c -> 'b raises 'a
'c < 'g
[ Some: 'k; None: 'l; 'm ] < [ Some: 'h; None: 'i; 'j ]
'l < 'i
Pre 'n < Abs

Since Java does not distinguish between Objects and null pointers, if
one looks at Java code, one finds lots of testing for null pointers
(and null pointer bombs when one runs Java).  MLJ is a SML compiler
that compiles to Java bytecode.  For this reason MLJ's option type
constructor combined with its array constructor have the semantics
Skaller is asking for.  Since this conflicts with the usual SML
tastes,  MLJ has a mixed policy towards option types (methods lenient;
functions not) but the programmer has no choice in the matter.

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 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.

I've written a good number of "improvements" to various Caml releases,
and found them to be mistakes.  The above is not a criticism of Ocaml.
I do want to point out this alternative that was not covered in the 
discussion so far.  Best of all since Wallace is implemented and since
its syntax is close to Ocaml, you can test it in practice and come to
your own conclusions.

-D


PS As for variable length arrays and type systems, I think there are
bigger problems than $. I've tried hand transliteration from Fortran to
Ocaml and not been satisfied with the results astheticly.  In contrast
APL2, J, and Nial are often quite nice.  Ocaml is a better C than C,
but IMHO, Ocaml is not a better Fortran than Fortran.  Arrays are still an
"open research topic", for example DML, Fish, and NESL.  (Yes, Ocaml is
a better C than C, but Ocaml is not a better asm than C.  A better asm
than C is also a "open research topic" ergo Talc & C--)

PPS.

> Assignment to array element can be very ineffictive in O'Caml due to the
> following reasons:
> 
> 1)O'Caml uses generational GC. 

False, generational does not imply copy-collect.  Dont alloc long lived 
mutables in the minor heap.  In fact, dont alloc any long lived anything in 
the minor heap :).

    

Re: the null pointer and subtyping

[Francois Pottier]

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/