Re: [Caml-list] '_a

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Dave,

Thanks for your comments.

> 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 personally believe that the main advantage is

0. Keep the typing abstract from implementation details.

This limits one very strongly when seeking alternatives.

> 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 agree with your first remark on point 2: while it avoids introducing
a new kind of variables, the value restriction is really confusing for
beginners. The theoretical rule may be simple, but it is not
intuitive, so one only understands it through a series of
approximations.
So my argument goes as: avoid introducing a new kind of variables (for
the sake of abstraction), but get as much polymorphism as possible, as
the non-generalizable case should be the exception.
Even if the rule for what to generalize is more complex, in some ways
it is closer to intuition. In "most" cases, it is just okay to
generalize the result of function applications.
Basically, non-generalizable cases with the relaxed restriction end up
belonging to two categories:
  * partial applications
  * mutable data structures
I believe this is easy to understand why they have to be restricted.

For the semantics, this should not be too hard. You just need to
introduce subtyping. And ocaml already has subtyping for evident
reasons.

Typed compilation shall also be ok. Note that we only allow
generalization of covariant variables (meaning "bottom"), not
contravariant ones (meaning "top"). By definition the covariant
variables correspond to no value, so you shouldn't need them to
determine the data representation. If we were also to generalize
purely contravariant variables, then we need a top object, meaning
that the representation would have to be uniform.

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

This is also an idea that crosses my mind once in a while, but I never
tried to formalize it further.
Looks like the main problem would be to decide where to use this
annotation. You can quickly get back into the above abstraction
problem, if purity is not considered as an essential part of the
semantics.
So this looks like an idea hard to apply in practice.

   Jacques Garrigue