Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??

> For some reason I've begun collecting interactions between type 
> variables and effects that have the characteristics listed below.  (Is 
> this really any stranger than a stamp collection? :-))  Granted, this is 
> a very narrow response to Matthias' call -- surely semantics is useful 
> for more than "assignment statements and alphas".
> A brief introduction to my collection:

> * Polymorphic fields in OCaml 3.05 (Leroy/Prevost, July 2002)
>     -- see OCaml mailing list

This is a bit out of the main stream of the discussion, but I don't think
this is a fair example on your list, since this was really a cut-and-paste
implementation bug, not a theoretical hole.

Type-soundness for polymorphic methods had been checked formally before
their implementation [1]. However, the implementation of typechecking for
polymorphic record fields had been a too-quick cut-and-paste from the
(older) implementation of typechecking for polymorphic methods, which had
the obviously erroneous effect of typechecking fields as if they would block
the evaluation.

author =       "Jacques Garrigue and Didier R{\'e}my",
title =        "Extending {ML} with Semi-Explicit Higher-Order Polymorphism",
journal =      "Information and Computation",
year =         1999,
volume =    "155",
number =    "1/2",
pages =     "134--169",
note       = "A preliminary version appeared in TACS'97"