annotations and type-checking

annotations and type-checking

[Aaron Bohannon]

Why do the first two programs type-check but the thrid one does not?

let f x = x in (f true, f 3);;

let f (x : 'a) : 'a = x in (f true);;

let f (x : 'a) : 'a = x in (f true, f 3);;

 - Aaron

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

[Jon Harrop]

On Tuesday 28 July 2009 22:47:25 Aaron Bohannon wrote:
> let f (x : 'a) : 'a = x in (f true, f 3);;

Err, good question. :-)

# let f : _ = fun x -> x in f true, f 3;;
- : bool * int = (true, 3)
# let f : 'a = fun x -> x in f true, f 3;;
Error: This expression has type int but is here used with type bool

I'm guessing the scope of the 'a is not what you'd expect but I have no idea 
why. I'd have thought the latter would be a harmless type annotation...

Any takers?

-- 
Dr Jon Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?e

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

[Philippe]

Le 29 juil. 09 à 01:28, Jon Harrop <jon@ffconsultancy.com> a écrit :

> On Tuesday 28 July 2009 22:47:25 Aaron Bohannon wrote:
>> let f (x : 'a) : 'a = x in (f true, f 3);;
>
> Err, good question. :-)
>
> # let f : _ = fun x -> x in f true, f 3;;
> - : bool * int = (true, 3)
The type of f here is something like 'a. 'a -> 'a. So you can use it  
on bool or int. I understand it like [], like in the expression (3 ::  
[], true :: []) where it has type 'a. 'a list (unfortunately it is not  
synctacally correct to say
let f : 'a. 'a -> 'a = fun x -> x, I don't know why.)

>
> # let f : 'a = fun x -> x in f true, f 3;;
> Error: This expression has type int but is here used with type bool
Here you specify that there exists a type named 'a, which is the  
return type of f and which should unify with both bool and int. Hence  
the typing error.


>
>
> I'm guessing the scope of the 'a is not what you'd expect but I have  
> no idea
> why. I'd have thought the latter would be a harmless type  
> annotation...

My guess is that the problem here is not about scope but about  
quantifiers : the type of f is quantified universally by default but  
the annotation constrains the type of f to a fixed (yet unknown) type  
in the subsequent expression (in that sense, yes, the scope of f plays  
a crucial role).

HTH,

Ph.

>
>
> Any takers?
>
> -- 
> Dr Jon Harrop, Flying Frog Consultancy Ltd.
> http://www.ffconsultancy.com/?e
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs

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

[Johannes Kanig]

Philippe wrote:
> Le 29 juil. 09 à 01:28, Jon Harrop <jon@ffconsultancy.com> a écrit :
>> I'm guessing the scope of the 'a is not what you'd expect but I have 
>> no idea
>> why. I'd have thought the latter would be a harmless type annotation...
> 
> My guess is that the problem here is not about scope but about 
> quantifiers : the type of f is quantified universally by default but the 
> annotation constrains the type of f to a fixed (yet unknown) type in the 
> subsequent expression (in that sense, yes, the scope of f plays a 
> crucial role).

I think John Harrop is right and the scope of 'a is really the issue 
here. First of all, transforming "let ... in" into a top-level let makes 
the code work again:

# let f (x : 'a) : 'a = x;;
val f : 'a -> 'a = <fun>
# f true;;
- : bool = true
# f 3;;
- : int = 3

which suggests that the scope of type variables in annotations is a 
top-level let-binding. I think I have read about this somewhere, but I 
can't find the right page of the manual ...

Also, the following code fails:

# let f (x : 'a) : 'a = x in (f true, (3 : 'a));;
Error: This expression has type int but an expression was expected of 
type bool


Here it is clear that all annotations are talking about the same 
variable 'a. If 'a was existentially bound twice (once for the function 
definition, once for the constant 3), a type error would not occur.

Johannes

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

[Mark Shinwell]

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

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

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

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?

 - Aaron

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
>

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

[Jacques Garrigue]

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

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

[Aaron Bohannon]

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
>

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

[Jon Harrop]

On Wednesday 29 July 2009 15:39:28 Jacques Garrigue wrote:
> 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).

That's very interesting. I had taken this for granted and never noticed this 
subtlety before...

-- 
Dr Jon Harrop, Flying Frog Consultancy Ltd.
http://www.ffconsultancy.com/?e