Categorical models of polymorphism

DOI10.1016/0890-5401(92)90024-AMaRDI QIDQ1193592zbMATH OpenFDO

Publication date 27 September 1992

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0890-5401(92)90024-A

Category theory has already been in the past one of the deepest instruments for the study of semantics of functional programming; and it seems to become more and more so in the future. It all started with the well-known correspondence between Cartesian-closed categories and lambda- calculus but it has gone much beyond that. This is particularly true of the second-order polymorphic lambda-calculus \(\lambda_ 2\), first defined in \textit{Y. Girard's} Thèse d'Etat (1976). This language has been modeled via two distinct categorical notions: that (external models) given by Seely (1987) based on CCC's indexed over another CCC on the one hand and that (internal models) given by Moggi (1987) based on topos theory. The present paper is devoted to an ``equational approach along Moggi's ideas. The paper presents and discusses the relations between two classes of categorical models of the second-order (or polymorphic) lambda-calculus, namely those based on internal categories (internal models) and those based on indexed categories (external models). Part I gives a detailed introduction to internal categories and their relations to indexed categories, via equations between arrows in an ambient category with finite limits. Part II introduces the above- mentioned two notions of a model and presents the ``externalization process that, given an internal model, yields an external one. It then shows how to go the other way round --- obtaining thus equivalent models. Part III discusses three major examples of models: provable retractions inside a PER model (Berardi, 1991), PER inside \(\omega\)-Set following Longo and Moggi (1991), and PL-categories inside their Grothendieck completion (Pitts, 1987). The appendix is an involved study of the notions of internal adjunction and internal CCC.

Recommendations

Cites work

Cited in

(8)

This page was built for publication: Categorical models of polymorphism

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1193592)