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

To: Dan Grossman <danieljg@cs.cornell.edu>
Subject: Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??
From: Didier Remy <Didier.Remy@inria.fr>
Date: Mon, 18 Nov 2002 12:02:45 +0100
Cc: Matthias Felleisen <matthias@ccs.neu.edu>, types@cis.upenn.edu
In-Reply-To: <200211162009.gAGK9LB6013165@saul.cis.upenn.edu>; from danieljg@cs.cornell.edu on Sat, Nov 16, 2002 at 01:33:46PM -0500
Organization: INRIA, BP 105, F-78153 Le Chesnay Cedex
Phone: (33) 1 3963 5317 -- Sec: (33) 1 3963 5207 -- Fax: (33) 1 3963 5193
References: <200211151436.PAA26724@fb04209.mathematik.tu-darmstadt.de> <200211161641.gAGGfQdR006037@saul.cis.upenn.edu> <200211162009.gAGK9LB6013165@saul.cis.upenn.edu>
Reply-To: Didier.Remy@inria.fr
User-Agent: Mutt/1.2.5i
Web: http://cristal.inria.fr/~remy

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

----------------
[1] 
@Article{Garrigue-Remy!poly-ml,
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"
}

References:

Re: semantics for F_{sub,rec} ??

From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>

Prev: Re: "foundations built on sand"
Next: Re: the point of (any) semantics, was Re: semantics for F_{sub,rec} ??
Index(es):
- Main
- Thread