Re: [Caml-list] '_a

[Dave Berry <daveberry@btconnect.com>]

Jacques,

That's a very interesting paper.  I note that you ask

"Our examples with constructor functions and abstract datatypes were 
expressible in
systems predating the value restriction, and are refused by the strict 
value restriction.
This makes one wonder why this didn't cause more problems during the 
transition."

At the time that SML'97 was being defined, I was working on Harlequin's SML 
compiler and programming environment (which has long since vanished into 
legal limbo).  The Harlequin team initially opposed the adoption of the 
value polymorphism rule for precisely the reasons you give.  Eventually we 
gave in because the other advantages outweighed the disadvantages.  (All 
these discussions took place in private e-mail).

Basically, the touted advantages of adopting the value polymorphism rule were:

1. The formal semantics became simpler.
2. Eliminating the different types of type variable made the language 
easier to explain, without affecting expressibility in practice.
3.  It enabled typeful compilation (as you note in your paper).

I have never believed either half of point 2.  The value polymorphism rule 
means that you have to explain about references and their effect on type 
inference even for some simple programs that don't use references at all, 
such as the example that Mike gave.  This "raises the bar" for explaining 
type inference to beginners.  Furthermore, expressiveness is affected for 
the examples that you give in your paper.  We had to change several parts 
of our code when we adopted the value polymorphism rule.  However, we felt 
(and I still think) that points 1 and 3, particularly point 3, outweigh 
these disadvantages.

 From a practical point of view, I like your approach.  However, it does 
negate point 1 above, because it makes the formal semantics more complex 
again - although this is less of a problem in O'Caml, because its semantics 
are already so complicated compared to SML97.  (I do not intend that remark 
as an insult). It will be interesting to see how your approach affects 
point 2 - novices may still encounter the value restriction in a simple 
program, and the new system will be more complicated to explain.

I sometimes wonder whether it would help to have a "pure" annotation for 
function types that would require the implementation to not use references 
nor to raise exceptions.  I don't mean a detailed closure analysis, just a 
simple flag.  Most practical functions would not be pure, but many simple 
ones could be, and these could be used to introduce people to the basics of 
functional programming without raising the complication of the value 
polymorphism rule.  (You wouldn't get a theory paper out of it 
though).  Unfortunately I'm no longer working on programming languages and 
so I don't have the capability to explore this.   It may be a half-baked 
idea that doesn't work in practice.

Best wishes,

Dave.



At 00:51 27/01/2005, Jacques Garrigue wrote:
>From: Mike Hamburg <hamburg@fas.harvard.edu>
>Subject: [Caml-list] '_a
>Date: Wed, 26 Jan 2005 19:19:16 -0500
>
> > The appearance of '_a in places where it shouldn't appear causes some
> > annoyance, and a good deal of confusion among beginners to O'Caml.  In
> > particular, List.map (fun x -> x) "ought to" have type 'a list -> 'a
> > list, whereas it instead has type '_a list -> '_a list.
> >
> > Some types are treated specially for creation of '_a, such as refs and
> > arrays.  For instance, if you have the following two declarations:
> >
> > # let a = let f x () = [x] in f [];;
> > val a : unit -> 'a list list = <fun>
> > # let b = let f x () = [|x|] in f [];;
> > val b : unit -> '_a list array = <fun>
> >
> > Although I haven't read the code for O'Caml, I deduce from this that
> > there is deep magic in place to determine when to turn 'a into '_a, and
> > in many cases, the heuristic is wrong (in the conservative direction:
> > in this case, 'a should not be turned into '_a until b is applied).
>
>There is no deep magic, no heuristics. There is just a type system
>which guarantees type soundness (i.e. "well typed programs cannot
>produce runtime type errors").
>
>If you want the type system and all the historical details, read my
>paper "Relaxing the value restriction" at
>   http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/
>
>In a nutshell, ocaml uses an improvement of the value restriction.
>With the value restriction, only definitions which are syntactical
>values (i.e. that do not call functions, etc when defined) are allowed
>to contain polymorphic type variables.
>This is improved by allowing covariant type variables to be
>generalized in all cases. Your first example is ok, because list is a
>covariant type, but your second fails, because array is not (you may
>assign to an array, and you would have to look at the code to see that
>each call to b creates a different array)
>
>Of course, one could think of many clever tricks by looking
>at what the code actually does. The above paper describes some of the
>"crazy" things Xavier Leroy and others tried in the past, which
>actually subsume your ideas, before they all decided this was too
>complicated. The main reason is that, if something is going to break
>at module boundaries, then it is not really useful.
>
>Good reading,
>
>Jacques Garrigue
>
>_______________________________________________
>Caml-list mailing list. Subscription management:
>http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
>Archives: http://caml.inria.fr
>Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
>Bug reports: http://caml.inria.fr/bin/caml-bugs