Abstract
We propose \({\lambda_{\text{c}}2_{\eta}}\) -calculus, which is a second-order polymorphic call-by-value calculus with extensional universal types. Unlike product types or function types in call-by-value, extensional universal types are genuinely right adjoint to the weakening, i.e., β-equality and η-equality hold for not only values but all terms. We give monadic style categorical semantics, so that the results can be applied also to languages like Haskell. To demonstrate validity of the calculus, we construct concrete models for the calculus in a generic manner, exploiting “relevant” parametricity. On such models, we can obtain a reasonable class of monads consistent with extensional universal types. This class admits polynomial-like constructions, and includes non-termination, exception, global state, input/output, and list-non-determinism.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Cardelli, L., Curien, P.-L.: Formal parametric polymorphism. TCS: Theoretical Computer Science 121 (1993)
Benton, N., Hughes, J., Moggi, E.: Monads and effects. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) APPSEM 2000. LNCS, vol. 2395, pp. 42–122. Springer, Heidelberg (2002)
Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models (extended abstract). In: CSL, pp. 121–135 (1994)
Bierman, G.M., Pitts, A.M., Russo, C.V.: Operational properties of Lily, a polymorphic linear lambda calculus with recursion. Electr. Notes Theor. Comput. Sci. 41(3) (2000)
Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Linear Abadi & Plotkin logic. Logical Methods in Computer Science 2(5) (November 2006)
Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Category-theoretic models of linear Abadi and Plotkin logic. Theory and Applications of Categories 20(7), 116–151 (2008)
Birkedal, L., Møgelberg, R.E.: Categorical models for Abadi and Plotkin’s logic for parametricity. Mathematical Structures in Computer Science 15(4), 709–772 (2005)
Birkedal, L., Møgelberg, R.E., Petersen, R.L.: Domain-theoretical models of parametric polymorphism. Theor. Comput. Sci. 388(1-3), 152–172 (2007)
Freyd, P.: Recursive types reduced to inductive types. In: Mitchell, J. (ed.) Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, LICS 1990, pp. 498–507. IEEE Computer Society Press, Los Alamitos (1990)
Führmann, C.: Direct models of the computational lambda calculus. Electr. Notes Theor. Comput. Sci. 20 (1999)
Girard, J.-Y.: Interpretation fonctionelle et elimination des coupures de l’arithmetique d’ordre superieur. These D’Etat, Universite Paris VII (1972)
Harper, R., Lillibridge, M.: Operational interpretations of an extension of F ω with control operators. J. Funct. Program. 6(3), 393–417 (1996)
Hasegawa, M.: Linearly used effects: Monadic and CPS transformations into the linear lambda calculus. In: Hu, Z., Rodríguez-Artalejo, M. (eds.) FLOPS 2002. LNCS, vol. 2441, pp. 167–182. Springer, Heidelberg (2002)
Hasegawa, M.: Relational parametricity and control. Logical Methods in Computer Science 2(3) (2006)
Hasegawa, M., Kakutani, Y.: Axioms for recursion in call-by-value. Higher-Order and Symbolic Computation 15(2-3), 235–264 (2002)
Hasegawa, R.: Categorical data types in parametric polymorphism. Mathematical Structures in Computer Science 4(1), 71–109 (1994)
Hermida, C.A.: Fibrations, Logical Predicates and Indeterminates. Ph.D thesis, University of Edinburgh (1993)
Jacobs, B.: Semantics of weakening and contraction. Ann. Pure Appl. Logic 69(1), 73–106 (1994)
Jacobs, B.: Categorical Logic and Type Theory. In: Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, Amsterdam (1999)
Levy, P.B.: Call-By-Push-Value: A Functional/Imperative Synthesis. Semantics Structures in Computation, vol. 2. Springer, Heidelberg (2004)
Levy, P.B., Power, J., Thielecke, H.: Modelling environments in call-by-value programming languages. INFCTRL: Information and Computation (formerly Information and Control) 185 (2003)
Møgelberg, R.E.: Interpreting polymorphic FPC into domain theoretic models of parametric polymorphism. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 372–383. Springer, Heidelberg (2006)
Møgelberg, R.E., Simpson, A.: Relational parametricity for computational effects. In: LICS, pp. 346–355. IEEE Computer Society, Los Alamitos (2007)
Møgelberg, R.E., Simpson, A.: Relational parametricity for control considered as a computational effect. Electr. Notes Theor. Comput. Sci. 173, 295–312 (2007)
Moggi, E.: Computational lambda-calculus and monads. Technical Report ECS-LFCS-88-66, Laboratory for Foundations of Computer Science, University of Edinburgh (1988)
Moggi, E.: Computational lambda-calculus and monads. In: LICS, pp. 14–23. IEEE Computer Society, Los Alamitos (1989)
Moggi, E.: Notions of computation and monads. Information and Computation 93(1), 55–92 (1991)
Plotkin, G.D.: Type theory and recursion (extended abstract). In: LICS, p. 374. IEEE Computer Society, Los Alamitos (1993)
Plotkin, G.D., Abadi, M.: A logic for parametric polymorphism. In: Bezem, M., Groote, J.F. (eds.) TLCA 1993. LNCS, vol. 664, pp. 361–375. Springer, Heidelberg (1993)
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Symposium on Programming. LNCS, vol. 19, pp. 408–423. Springer, Heidelberg (1974)
Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: IFIP Congress, pp. 513–523 (1983)
Simpson, A.K., Plotkin, G.D.: Complete axioms for categorical fixed-point operators. In: LICS, pp. 30–41 (2000)
Street, R.: The formal theory of monads. Journal of Pure and Applied Algebra 2, 149–168 (1972)
Wadler, P.: Theorems for free! In: Functional Programming Languages and Computer Architecture. Springer, Heidelberg (1989)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Asada, K. (2008). Extensional Universal Types for Call-by-Value. In: Ramalingam, G. (eds) Programming Languages and Systems. APLAS 2008. Lecture Notes in Computer Science, vol 5356. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89330-1_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-89330-1_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89329-5
Online ISBN: 978-3-540-89330-1
eBook Packages: Computer ScienceComputer Science (R0)