Categorical models of polymorphism (Q1193592): Difference between revisions

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.