[TYPES] Fwd: polymorphic isomorphisms

[Philip Wadler]

On 28 Jan 2008, at 11:49, Thorsten Altenkirch wrote:

> Background can be found in Wadler's seminal paper "Theorem's for
> free" and his note "Recursive types for free!" available from http://
> homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt
> (was this ever published?).

Thanks for the kind words.  I hasten to point out that "Theorems for  
Free"
is strongly influenced by Reynolds' seminal paper, "Types, Abstraction,
and Parametric Polymorphism".  "Recursive types for free" is indeed  
unpublished.
Another related paper is "The Girard-Reynolds Isomorphism"; the  
second edition
is in the Reynolds festschrift:

   http://dx.doi.org/10.1016/j.tcs.2006.12.042

There I wrote:

   The basic structure of the proofs in Section 5 was suggested,  
independently, by
   Wadler [46] and Hasegawa [16].  Wadler’s proof was not published,  
but it circulated
   informally, and influenced the work of Abadi, Cardelli, and Curien  
[1] and the
   subsequent work of Plotkin and Abadi [33].

(Reference 46 is "Recursive types for free".)  Cheers,  -- P