Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
annotations and type-checking
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Aaron Bohannon <bohannon@c...>
Subject: Re: [Caml-list] annotations and type-checking
Yes, I was completely wrong.  Type variables do prevent me from writing

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


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*

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<> wrote:
> From: Aaron Bohannon <>
>> 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<> 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:
>>> Mark