Another polymorphism puzzle

Another polymorphism puzzle

[Yaron Minsky]

The last example I posted about had to do with variant types.  Here's
another interseting little typing surprise having to do with record
types:

# type 'a t = { foo: 'a };;
type 'a t = { foo : 'a; }
# let f x = { x with foo = 3 };;
val f : 'a -> int t = <fun>

I can kind of see how this happened, since after all, the result of (f
x) does not depend in any way on x.  And yet, it seems like the
unification rules should force f to have time ('a t -> int t).

y

Re: [Caml-list] Another polymorphism puzzle

[Karl Zilles]

Yaron Minsky wrote:
> The last example I posted about had to do with variant types.  Here's
> another interseting little typing surprise having to do with record
> types:
> 
> # type 'a t = { foo: 'a };;
> type 'a t = { foo : 'a; }
> # let f x = { x with foo = 3 };;
> val f : 'a -> int t = <fun>
> 
> I can kind of see how this happened, since after all, the result of (f
> x) does not depend in any way on x.  And yet, it seems like the
> unification rules should force f to have time ('a t -> int t).

Wow.  This is pretty cool.  Also

# type 'a t = { foo: 'a; bar: int };;
type 'a t = { foo : 'a; bar : int; }

# let f x = { x with foo = 3 };;
val f : 'a t -> int t = <fun>
(now the domain is limited to 'a t)

# f { foo= "blah"; bar=100 };;
- : int t' = {foo = 3; bar = 100}

Re: [Caml-list] Another polymorphism puzzle

[Manos Renieris]

Worse:

# let f x = { () with foo = 3};;                    
val f : 'a -> int t = <fun>
# let f x = { 42 with foo = 3};; 
val f : 'a -> int t = <fun>

I think this qualifies as a bug. Especially since the documentation
says the expr on the left hand side of with has to be a record.

Thu, Mar 31, 2005 at 09:02:14PM -0500, Yaron Minsky wrote:
> The last example I posted about had to do with variant types.  Here's
> another interseting little typing surprise having to do with record
> types:
> 
> # type 'a t = { foo: 'a };;
> type 'a t = { foo : 'a; }
> # let f x = { x with foo = 3 };;
> val f : 'a -> int t = <fun>
> 
> I can kind of see how this happened, since after all, the result of (f
> x) does not depend in any way on x.  And yet, it seems like the
> unification rules should force f to have time ('a t -> int t).
> 
> y
> 
> _______________________________________________
> 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] Another polymorphism puzzle

[Jacques Garrigue]

From: Manos Renieris <er@cs.brown.edu>
> Worse:
> 
> # let f x = { () with foo = 3};;                    
> val f : 'a -> int t = <fun>
> # let f x = { 42 with foo = 3};; 
> val f : 'a -> int t = <fun>
> 
> I think this qualifies as a bug. Especially since the documentation
> says the expr on the left hand side of with has to be a record.

What do you mean by worse? You just exhibit an immediate consequence
of the typing of f below.

> Thu, Mar 31, 2005 at 09:02:14PM -0500, Yaron Minsky wrote:
> > # type 'a t = { foo: 'a };;
> > type 'a t = { foo : 'a; }
> > # let f x = { x with foo = 3 };;
> > val f : 'a -> int t = <fun>

Now, why does it happen?
The reason is simply that the typing of {x with fields} follows
closely its semantics:
  build a record from the given fields, extracting values from x
  when a field is missing.
Consequence: if you provide all the fields, then there is no missing
field, so x can be completely ignored.
Following the manual, the typing could be more restrictive, but the
current typing is perfectly sound.

Jacques Garrigue

Re: [Caml-list] Another polymorphism puzzle

[Alex Baretta]

Jacques Garrigue wrote:
> From: Manos Renieris <er@cs.brown.edu>
> 
>>Worse:
>>
>># let f x = { () with foo = 3};;                    
>>val f : 'a -> int t = <fun>
>># let f x = { 42 with foo = 3};; 
>>val f : 'a -> int t = <fun>
>>
>>I think this qualifies as a bug. Especially since the documentation
>>says the expr on the left hand side of with has to be a record.
> 
> 
> What do you mean by worse? You just exhibit an immediate consequence
> of the typing of f below.

I think that "worse" here stands for "completely counterintuitive".

> Following the manual, the typing could be more restrictive, but the
> current typing is perfectly sound.
> 
> Jacques Garrigue

I doubt that any one of us has every written buggy code like the 
examples in this thread, yet, it it ever happens out of pure thermal 
agitation in the PS2 cable, I would expect the type checker to track 
down such "unsound" code, even if it would not cause a segfault.

Alex

-- 
*********************************************************************
http://www.barettadeit.com/
Baretta DE&IT
A division of Baretta SRL

tel. +39 02 370 111 55
fax. +39 02 370 111 54

Our technology:

The Application System/Xcaml (AS/Xcaml)
<http://www.asxcaml.org/>

The FreerP Project
<http://www.freerp.org/>