Hostname: page-component-7479d7b7d-c9gpj Total loading time: 0 Render date: 2024-07-15T21:44:26.148Z Has data issue: false hasContentIssue false
  • English
  • Français

Universal properties for universal types in bifibrational parametricity

Published online by Cambridge University Press:  22 March 2019

Neil Ghani ,
Fredrik Nordvall Forsberg  and
Federico Orsanigo
Neil Ghani*
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
Fredrik Nordvall Forsberg
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
Federico Orsanigo
Affiliation:
Department of Computer and Information Sciences, University of Strathclyde, Glasgow, UK
*
*Corresponding author. Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In the 1980s, John Reynolds postulated that a parametrically polymorphic function is an ad-hoc polymorphic function satisfying a uniformity principle. This allowed him to prove that his set-theoretic semantics has a relational lifting which satisfies the Identity Extension Lemma and the Abstraction Theorem. However, his definition (and subsequent variants) has only been given for specific models. In contrast, we give a model-independent axiomatic treatment by characterising Reynolds’ definition via a universal property, and show that the above results follow from this universal property in the axiomatic setting.

Keywords

Relational parametricitycategorical semanticscomprehension categories
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 29 , Issue 6 , June 2019 , pp. 810 - 827
Copyright
© Cambridge University Press 2019 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Ahmed, A. and Blume, M. (2008). Typed closure conversion preserves observational equivalence. In: International Conference on Functional Programming, ICFP ‘08, ACM, 157–168.Google Scholar
Ahmed, A., Dreyer, D. and Rossberg, A. (2009). State-dependent representation independence. In: Principles of Programming Languages, POPL ‘09, ACM, 340–353.Google Scholar
Atkey, R. (2009). A deep embedding of parametric polymorphism in Coq. In: Workshop on Mechanising Metatheory. Edinburgh, UK.Google Scholar
Bezem, M.Coquand, T. and Huber, S. (2014). A model of type theory in cubical sets. In: Types for Proofs and Programs (TYPES 2013). Leibniz International Proceedings in Informatics, vol. 26, Schloss Dagstuhl–Leibniz–Zentrum für Informatik, 107–128.Google Scholar
Birkedal, L. and Møgelberg, R. E. (2005). Categorical models for Abadi and Plotkin’s logic for parametricity. Mathematical Structure in Computer Science 15 709–772.CrossRefGoogle Scholar
Coquand, T. and Huet, G. (1988). The calculus of constructions. Information and Computation 76 95–120.CrossRefGoogle Scholar
Dreyer, D., Neis, G. and Birkedal, L. (2012). The impact of higher-order state and control effects on local relational reasoning. Journal of Functional Programming 22(4&5):477–428.CrossRefGoogle Scholar
Dunphy, B. and Reddy, U. S. (2004). Parametric limits. In: Logic in Computer Science, LICS ‘04, IEEE Computer Society, 242–251.Google Scholar
Ehrhard, T. (1988). A categorical semantics of constructions. In: Logic in Computer Science, 264–273.Google Scholar
Ghani, N., Johann, P., Nordvall Forsberg, F., Orsanigo, F. and Revell, T. (2015a). Bifibrational functorial semantics of parametric polymorphism. In: Dan, R. Ghica (ed.), MFPS.CrossRefGoogle Scholar
Ghani, N., Nordvall Forsberg, F. and Orsanigo, F. (2015b). Parametric polymorphism– universally. In: de Paiva, Valeria, de Queiroz, Ruy, Moss, Lawrence S., Leivant, Daniel and de Oliveira, Anjolina G. (eds.) Logic, Language, Information, and Computation, LNCS, vol. 9160, Springer, 81–92.CrossRefGoogle Scholar
Ghani, N., Nordvall Forsberg, F. and Orsanigo, F. (2016a). Proof-relevant parametricity. In: Lindley, Sam, McBride, Conor, Trinder, Philip W. and Sannella, Donald (eds.) A List of Successes That Can Change theWorld– Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday, Lecture Notes in Computer Science, vol. 9600, Springer, 109–131.Google Scholar
Ghani, N., Nordvall Forsberg, F. and Simpson, A. (2016b). Comprehensive parametric polymorphism: categorical models and type theory. In: Jacobs, Bart and Löding, Christof (eds.) Foundations of Software Science and Computation Structures, vol. 9634, Lecture Notes in Computer Science, Springer, 3–19.CrossRefGoogle Scholar
Girard, J.-Y., Taylor, P. and Lafont, Y. (1989). Proofs and Types. Cambridge, Cambridge University Press.Google Scholar
Hermida, C. (1993). Fibrations, Logical Predicates and Indeterminates. PhD thesis, University of Edinburgh.CrossRefGoogle Scholar
Hermida, C. (2006). Fibrational relational polymorphism. Available at http://maggie.cs.queensu.ca/chermida/papers/FibRelPoly.pdf.Google Scholar
Hur, C.-K. andDreyer, D. (2011). A Kripke logical relation between ML and assembly. In: Principles of Programming Languages, POPL ‘11, ACM, 133–146.Google Scholar
Jacobs, B. (1993). Comprehension categories and the semantics of type dependency. Theoretical Computer Science 107 (2): 169–207.CrossRefGoogle Scholar
Jacobs, B. (1999). Categorical logic and type theory. In: Studies in Logic and the Foundations of Mathematics, vol. 141, North Holland, Amsterdam.Google Scholar
Lawvere, F. W. (1970). Equality in hyperdoctrines and comprehension schema as an adjoint functor. Applications of Categorical Algebra, 17:1–14.CrossRefGoogle Scholar
Ma, Q. M. and Reynolds, J. C. (1992). Types, abstractions, and parametric polymorphism, part 2. In: Mathematical Foundations of Programming Semantics, Springer, 1–40.Google Scholar
Orsanigo, F. (2017). Bifibrational Parametricity: From Zero to Two Dimensions. PhD thesis, University of Strathclyde.Google Scholar
Pitts, A.M. (1987). Polymorphism is set theoretic, constructively. In: Category Theory and Computer Science, Springer, 12–39.CrossRefGoogle Scholar
Plotkin, G. and Abadi, M. (1993). A logic for parametric polymorphism. In: TLCA, Springer, 361–375.Google Scholar
Reynolds, J. C. (1983). Types, abstraction and parametric polymorphism. Information Processing (33), 513–523.Google Scholar
Reynolds, J. C. (1984). Polymorphism is not set-theoretic. In: Semantics of Data Types, Lecture Notes in Computer Science, vol. 173, Springer, 145–156.CrossRefGoogle Scholar
Seely, R. A. G. (1987). Categorical semantics for higher order polymorphic lambda calculus. Journal of Symbolic Logic, 969–989.CrossRefGoogle Scholar
Strachey, C. (2000). Fundamental concepts in programming languages. In: International Summer School in Computer Programming, Copenhagen, Lecture Notes, 1967. Published in Higher Order Symbolic Computation, Kluwer Academic Publishers, 13 (1-2):11–49.Google Scholar
Tse, S. and Zdancewic, S. (2004). Translating dependency into parametricity. In: International Conference on Functional Programming, ICFP ‘04, ACM, 115–125.Google Scholar
Wadler, P. (1989). Theorems for free! In: Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA ‘89, 347–359.Google Scholar