Re: Type annotations

[Jacques Garrigue <garrigue@kurims.kyoto-u.ac.jp>]

> > There has been already various proposals for allowing types to be taken
> > into account when typing record labels. The difficulty is that as soon
> > as you make it into something useful, you loose the principal type
> > property, and that some theoreticians working on ocaml wouldn't like
> > it.
> 
> The loss of the pricipal type theorem has also recently been discussed in
> comp.lang.ml and comp.lang.functional. Using type-annotation by the
> compiler prior (call this the PRIOR approach) to unification can help
> typing expression that cannot be typed otherwise. For example, cases of
> polymoriphic recursion. In fact, this is the way this is handled in
> Haskell (this topic has also appeared in this list previously). 
> Although I wouldn't go running to implement all my code in Haskell :-), I
> do think that using PRIOR could be an improvement. 
> 
> Is there a problem with PRIOR? 

There are a few things that work well with this approach, polymorphic
recursion being one. But it is not as general as it seems.
A simple scheme is to assume that you can give explicitely a type to
an identifier, use this type to resolve ambiguities, and check
afterwards that this type is correct.
With such a scheme,
     let w : t = {x=1;y=2} in w.x
will indeed be correctly handled.
However, this breaks as soon as an annotation is lacking:
     let w : t = {x=1;y=2} in
     let v = w in
     w.x
Similarly, pairs won't work
     let w : t * int = ({x=1;y=2}, 3) in (fst w).x
Indeed, while w was given a special "assumed" type, propagating such
assumed types through definitions and function calls is much more
subtle.
In a paper by Didier Remy and myself [1], we designed a system that
could do a fair amount of "assumed" type propagation. This was
intended for providing first class polymorphism and polymorphic
methods, and was implemented in Objective Label. This could also be
used for typing records, while some might see it as an overkill.
But this is much more complex than what you are calling PRIOR.
And this is not principal in the strict meaning (due to a mischevious
side-effect of the value only prolymorphism rule).

I am currently working on reintegrating this feature in ocaml. However
it is not yet clear whether it can be made cheap enough to make it
into the main stream version (type inference becomes slower).
And then some might discuss the fact it would require people to learn
yet another set of rules about how assumed types are propagated.

Cheers,

Jacques

[1] Extending ML with semi-explicit higher order polymorphism,
    Information and Computation 155, december 1999, pages 134-171.

---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>