[Prev][Next][Index][Thread]

Re: A simple categorical model of predicative polymorphism

Dear Olaf:
   One interesting reference characterizing lambda definability in
categorical models of core-ML is by Moez Alimohamed, TCS 146 (1995),
pp. 5-23. A general framework has been discussed by Mitchell and
Scedrov (in their paper "Notes on Sconing and Relators, SLNCS 702, 1993).
   I don't know how "simple" you consider the following model, but one
approach to modelling core-ML is in a short paper by Girard, Scedrov, and
me:  "Normal Forms and Cut-Free Proofs as Natural Transformations", in
Logic from Computer Science, ed. by Y. Moschovakis, Springer, 1992  (I
recommend you get the version from my account at Hypatia or my website,
since the original published one was badly printed by Springer (with
missing fonts)).  This is related to Phil Wadler's work entitled "Theorems
for free". The general framework is discussed in the paper "Functorial
Polymorphism" by Bainbridge, Freyd, Scedrov, and me in  TCS 70 (1990),
pp. 35-64.

   			Cheers,
			Phil Scott
			University of Ottawa
    


On Mon, 2 Aug 1999, Olaf Chitil wrote:

> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> I'm looking for a *simple* categorical model of a predicatively polymorphic
> lambda calculus, that is, a model which avoids the complications needed for
> impredicativity.
> I just need a model of an explicitly typed version of Core-ML (including
> recursion).
> 
> I found the following, promising reference:
> 
> W. Phoa: A simple categorical model of first-order polymorphism (submitted)
> 
> Unfortunately it seems that this paper has never been published and the author
> left academica.
> 
> Furthermore, it seems to be folk-lore that polymorphic functions are natural
> transformations. It would be nice, if the model expressed this formally.
> 
> Any pointers to literature are highly welcome.
> 
> Thank you,
> Olaf 
> 
> -- 
> OLAF CHITIL, Lehrstuhl fuer Informatik II, RWTH Aachen, 52056 Aachen, Germany
>              Tel: (+49/0)241/80-21212; Fax: (+49/0)241/8888-217
>              URL: http://www-i2.informatik.rwth-aachen.de/~chitil/
>