[Prev][Next][Index][Thread]
A simple categorical model of predicative polymorphism
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/