Re: [Caml-list] Are record types generative?

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

On 2018/02/03 08:07, Toby Kelsey wrote:
> 
> On 24/01/18 08:43, Jacques Garrigue wrote:
>> I.e., types can be used to optimize a program, but they do not change its semantics.
>> It’s true of so-called “overloaded” record labels, it’s true of a labeled and default arguments
>> (which use type information for compilation, but not semantics), it’s true of objects,
>>  it’s true of GADT pattern-matching (again optimized), etc…
> 
> type foo = { x : int }
> type bar = { x : string }
> 
> let f r = r.x           (* OK: uses bar *)
> let f r = (r:foo).x  (* OK: uses foo *)
> let f r = (r.x : int) (* type error - wrong type inferred *)
> 
> 
> Aren't the semantics different? 'f' has different types in the first two definitions, And why does type inference fail for the last example?


By semantics, I mean runtime semantics (i.e. the evaluation of a program).
The first two functions both return the contents of the field x of their argument.
The problem with the 3rd function is not semantics but incompleteness of type inference in presence of label overloading.

Jacques