Polymorphism and effects

Aaron and I were having a conversation over lunch yesterday about the 
interaction of polymorphism and effects, and the history of how Wright and 
Felleisen's A Syntactic Approach to Type Soundness turned out to be incorrect 
in the polymorphic ML with callcc case.

In July of 91, Harper and Lillibridge posted to the sml-list and TYPES forum, 
the message "ML with callcc is unsound" demonstrating a counter example that 
would bring SML of NJ to it's knees.

    http://www.cis.upenn.edu/~bcpierce/types/archives/1991/msg00034.html

In 2002, Matthias recalled the experience of receiving this example in an 
email from Bob Harper:

    the point of (any) semantics, was Re: semantics for F_{sub,rec} ??
    http://www.cis.upenn.edu/~bcpierce/types/archives/current/msg01178.html

He also put forth a call for:

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

To which Dan Grossman, of Cyclone fame, put forth the following 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.


I'm still a bit confused over the time line though, since the Harper note 
appeared in 91, but A Syntactic Approach to Type Soundness didn't appear in 
Information and Computation until 1994, but references to it exist in the lit 
as early as 90.

David