Re: [Caml-list] annotations and type-checking

[Aaron Bohannon <bohannon@cis.upenn.edu>]

Yes, I was completely wrong.  Type variables do prevent me from writing

let f (x : 'a -> 'a) : 'a = x;;

and

let f (x : 'a) (y : 'a) : int = 3 in f true "true";;

So they are certainly not meaningless.  But I use annotations
primarily to get better, more accurately located error messages from
the type-checker, and apparently annotating functions that are
(intended to be) polymorphic is never useful for this purpose.  And it
boggles my mind that annotations with type variables *prevent*
generalization.

But at least by now, I guess anyone following this discussion should
know whether this program type-checks... ;)

let f (x : 'a -> unit) : unit = () in
f print_string;
let g (y : 'a -> unit) : unit = () in
g print_float ;;

 - Aaron

On Wed, Jul 29, 2009 at 10:39 AM, Jacques
Garrigue<garrigue@math.nagoya-u.ac.jp> wrote:
> From: Aaron Bohannon <bohannon@cis.upenn.edu>
>> Thank you for that link.  To boil it down, it seems (1) type variables
>> annotating top-level declarations are ignored, and (2) type variables
>> annotating local bindings are treated existentially (as if one had
>> written '_a, although that name itself is considered syntactically
>> ill-formed).
>
> Point (1) is wrong. They are not ignored, they act as constraints.
> Actually, their behaviour is uniform: they are always bound and
> generalized at toplevel. This is true both for normal functions an
> classes. The only exception is with modules, but it is not surprising
> as modules work on a different level.
>
> I can see only one really buggy behaviour in Alain's mail, the fact
> that local modules did flush type variables. Fortunately, this has
> been corrected.
>
>> So if OCaml cannot do anything better than this, then why are type
>> variables even syntactically legal in annotations?  If backwards
>> compatibility is the issue, could it not at the very very least give a
>> compiler warning when they are used?
>
> Because it is useful to be able to have type annotations sharing type
> variables in different places in a term (for instance for different
> arguments).
>
> Jacques Garrigue
>
>> On Wed, Jul 29, 2009 at 3:40 AM, Mark
>> Shinwell<mshinwell@janestcapital.com> wrote:
>>> On Tue, Jul 28, 2009 at 05:47:25PM -0400, Aaron Bohannon wrote:
>>>> Why do the first two programs type-check but the thrid one does not?
>>>
>>> Dark corners of the type system.
>>>
>>>> let f (x : 'a) : 'a = x in (f true, f 3);;
>>>
>>> Explicit type variables in this situation are considered "global".  They are
>>> not generalized until the type of the whole toplevel declaration has been
>>> determined.  Consequentially, during type-checking of the body of your
>>> let expression, 'a is not a generalized variable.
>>>
>>> There is more detail on similar situations here:
>>>
>>> http://caml.inria.fr/pub/ml-archives/caml-list/2002/06/a03da53be62c12671a891708c51e85f9.en.html
>>>
>>> Mark
>