Re: [Caml-list] Equality between abstract type definitions

[Roberto Di Cosmo <roberto@dicosmo.org>]

Hi Jonathan,
   I beg to disagree

On Fri, Oct 25, 2013 at 02:45:52PM +0200, Jonathan Protzenko wrote:
> You should also remember that the top-level, which is what most
> beginners use, also favors the confusion.
> 
> # let f x = x;;
> val f : 'a -> 'a = <fun>

OCaml is telling you: hey, your code is so generic that I can give it
the type 'a -> 'a, you got a polymorphic function!

> # let f : 'a -> 'a = fun x -> x + 1;;
> val f : int -> int = <fun>
> 

Here you are telling OCaml: 
 look, I'd like to see f as having type 'a -> 'a, what do you think?

And OCaml tells you: sorry sir, the best I can give you is int -> int

> What OCaml is actually telling you is: "this function has type 'a -> 'a,
> but if you write 'a -> 'a yourself, I'm going to give it a totally
> different meaning".
> 
> ~ jonathan

The point on which I agree is that if we leave these annotations in
the code, they may end up being read as specifications by whomever
looks at the sources alone, and this may lead to confusion.

But to spot such issues we do not need to change the syntax and semantics of 
type annotations, it would be enough to have yet another warning
that informs us that the type annotations have been instanciated...
something like

# let f : 'a -> 'a = fun x -> x + 1;;
           _______
Warning 66: the user provided type constraint is too general:
variable 'a has been instanciated to type int
val f : int -> int = <fun>

--
Roberto

P.S.: I will not feed the troll any longer though, time to
get back to work :-)