Type annotations.

Type annotations.

[Ohad Rodeh]

Jacques,
  I'd love to see this added to the distribution, even if only 
as an optional compile time flag. Allowing polymorphic recursion, and
mitigating the record naming problem are worthy goals, 

   Ohad.

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

Re: Type annotations

[Jacques Garrigue]

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

Type annotations

[Ohad Rodeh]

Dear List, 
  I've previously sent a message, for which I got no replies, so
I'm resending it. 

> ... stuff removed ...
> 
> > Also, I am a bit curious why it doesn't help to type explicitely,
> > i.e. to
> > write
> > let x:point_3d={x=10.;y=20.;z=30.} ???
> > 
> 
> Because this is not the way it works. Labels are defined as are values
> or constructors, this is only afterwards that the compiler checks that
> they all belong to the same type. That is, the type cannot influence the
> choice between x(point_3d) and x(point_2d), only the order of
> definition can.
> 
> 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? 

	Ohad.