[Prev][Next][Index][Thread]
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:
* ML + call/cc (Wright/Felleisen/Lillibridge/Harper)
* Polymorphic fields in OCaml 3.05 (Leroy/Prevost, July 2002)
-- see OCaml mailing list
* Existential types in Cyclone (April 2002)
[Yes, I am 'guilty' too. I just was lucky enough to discover my
mistake before somebody else did.]
-- see ESOP2002
* Generic Java type inference (Jeffrey, December 2001)
-- see Types List
* Breaking parametricity in ML (Pierce/Sangiorgi, 1997)
[Not an unsoundness, but a surprising result nonetheless]
-- see JACM2000
This collection makes it possible to make provocative rants. For example:
(1) Language designers not familiar with this collection will continue
to make false claims about polymorphic languages.
(2) Alas, language designers familiar with this collection will continue
to make false claims about polymorphic languages.
--Dan
Matthias Felleisen wrote:
> So, I am calling on people to collect a bunch of examples with the
> following characteristics:
>
> - people make a claim about a language
> - people later find that this is not true
> - by adjusting the implementation to the language, we help programmers
> develop, debug, and maintain their programs more easily and indeed,
> prevent latent explosions.
>
> Example: I volunteer one of my own publications as an example. Some of
> you may be aware of my paper with Andrew Wright, which uses my 'evaluation
> context semantics' to prove type soundness/safety for a series of ML-ish
> languages.
>
> The last of the languages is the polymorphic ML core with call/cc.
References: