The Duality of Classical Intersection and Union Types

• Autorzy: Downen Paul , Ariola Zena M. , Ghilezan Silvia

Identyfikatory

DOI

10.3233/FI-2019-1855

• Języki publikacji: EN

Abstrakty

EN

For a long time, intersection types have been admired for their surprising ability to complete the simply typed lambda calculus. Intersection types are an example of an implicit typing feature which can describe program behavior without manifesting itself within the syntax of a program. Dual to intersections, union types are another implicit typing feature which extends the completeness property of intersection types in the lambda calculus to full-fledged programming languages. However, the formalization of union types can easily break other desirable meta-theoretical properties of the type system. But why should unions be troublesome when their dual, intersections, are not? We look at the issues surrounding the design of type systems for both intersection and union types through the lens of duality by formalizing them within the symmetric language of the classical sequent calculus. In order to formulate type systems which have all of our properties of interest—soundness, completeness, and type safety—we also look at the impact of evaluation strategy on typing. As a result, we present two dual type systems—one for call-by-value and one for call-by-name evaluation—which have all three properties. We also consider the possibility of classical non-deterministic evaluation, for which there is a choice between two different systems depending on which properties are desired: a full type system which is complete, and a simplified type system which is sound and type safe.

Słowa kluczowe

EN

intersection types; union types; duality; sequent calculus; discipline; type safety; strong normalization; soundness; completeness; reducibility candidates; symmetric candidates

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2019
• Tom: Vol. 170, nr 1-3
• Strony: 39--92
• Opis fizyczny: Bibliogr. 56 poz., rys., tab.

Twórcy

autor

Downen Paul

• University of Oregon, USA

autor

Ariola Zena M.

• University of Oregon, USA

autor

Ghilezan Silvia

• University of Novi Sad, Mathematical Institute SASA, Republic of Serbia

Bibliografia

• [1] Downen P, Johnson-Freyd P, Ariola ZM. Uniform Strong Normalization for Multi-Discipline Calculi. In: Rewriting Logic and its Applications. 2018 pp. 205-225. doi:10.1007/978-3-319-99840-4_12.
• [2] Church A. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 1940. 5:56-68. doi:10.2307/2266170.
• [3] Barendregt H. Introduction to generalized type systems. Journal of Functional Programming, 1991. 1(2):125-154. doi:10.1017/S0956796800020025.
• [4] Coppo M, Dezani-Ciancaglini M. A new type assignment for λ-terms. Arch. Math. Log., 1978. 19(1):139-156. doi:10.1007/BF02011875.
• [5] Pottinger G. A type assignment for the strongly normalizable λ-terms. In: Seldin JP, Hindley JR (eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 561-577. Academic Press, London, 1980.
• [6] Sallé P. Une extension de la théorie des types en lambda-calcul. In: Ausiello G, Böhm C (eds.), Fifth International Conference on Automata, Languages and Programming, volume 62 of Lecture Notes in Computer Science. Springer-Verlag, 1978 pp. 398-410. ISBN-3-540-08860-1.
• [7] MacQueen DB, Plotkin GD, Sethi R. An Ideal Model for Recursive Polymorphic Types. Information and Control, 1986. 71(1/2):95-130. doi:10.1016/S0019-9958(86)80019-5.
• [8] Pierce BC. Programming with Intersection Types, Union Types, and Polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.
• [9] Barbanera F, Dezani-Ciancaglini M, de’Liguoro U. Intersection and Union Types: Syntax and Semantics. Inf. Comput., 1995. 119(2):202-230. doi:10.1006/inco.1995.1086.
• [10] Liquori L, Stolze C. Personal communication, 2019.
• [11] Honsell F, Liquori L, Stolze C, Scagnetto I. The Delta-Framework. In: 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2018, December 11-13, 2018, Ahmedabad, India. 2018 pp. 37:1-37:21. doi:10.4230/LIPIcs.FSTTCS.2018.37.
• [12] Tofte M. Type Inference for Polymorphic References. Inf. Comput., 1990. 89(1):1-34. doi:10.1016/0890-5401(90)90018-D.
• [13] Harper R, Lillibridge M. ML with callcc is unsound. Message to the TYPES mailing list, July 1991.
• [14] Curien PL, Herbelin H. The duality of computation. In: Odersky M, Wadler P (eds.), Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP ’00), Montreal, Canada, September 18-21, 2000. ACM. ISBN 1-58113-202-6, 2000 pp. 233-243. doi:10.1145/351240.351262.
• [15] Barbanera F, Berardi S. A Symmetric Lambda Calculus for “Classical” Program Extraction. In: Proceedings of the International Conference on Theoretical Aspects of Computer Software, TACS ’94. Springer-Verlag, London, UK, UK. ISBN 3-540-57887-0, 1994 pp. 495-515.
• [16] Wadler P. Call-by-value is dual to call-by-name. SIGPLAN Notices, 2003. 38(9):189-201. doi:10.1145/944746.944723.
• [17] Downen P, Ariola ZM. A tutorial on computational classical logic and the sequent calculus. J. Funct. Program., 2018. 28:e3. doi:10.1017/S0956796818000023.
• [18] Downen P. Sequent Calculus: A Logic and a Language for Computation and Duality. Ph.D. thesis, University of Oregon, 2017.
• [19] Herbelin H, Zimmermann S. An Operational Account of Call-By-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form. In: Curien PL (ed.), Typed Lambda Calculi and Applications: 9th International Conference, TLCA 2009. Springer Berlin Heidelberg, Berlin, Heidelberg. ISBN 978-3-642-02273-9, 2009 pp. 142-156. doi:10.1007/978-3-642-02273-9_12.
• [20] Carraro A, Guerrieri G. A Semantical and Operational Account of Call-by-Value Solvability. In: Foundations of Software Science and Computation Structures - 17th International Conference, FOSSACS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings. 2014 pp. 103-118. doi:10.1007/978-3-642-54830-7\_7.
• [21] Sabry A, Felleisen M. Reasoning About Programs in Continuation-Passing Style. Lisp and Symbolic Computation, 1993. 6(3-4):289-360. doi:10.1007/BF01019462.
• [22] Andreoli J. Logic Programming with Focusing Proofs in Linear Logic. J. Log. Comput., 1992. 2(3):297-347. doi:10.1093/logcom/2.3.297.
• [23] Laurent O. Étude de la polarisation en logique. Thèse de doctorat, Université de la Méditerranée - Aix-Marseille II, 2002.
• [24] Girard J. A New Constructive Logic: Classical Logic. Mathematical Structures in Computer Science, 1991. 1(3):255-296. doi:10.1017/S0960129500001328.
• [25] Downen P, Ariola ZM. The Duality of Construction. In: Shao Z (ed.), Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, volume 8410 of Lecture Notes in Computer Science. Springer. ISBN 978-3-642-54832-1, 2014 pp. 249-269. doi:10.1007/978-3-642-54833-8_14.
• [26] Giannini P, Ronchi Della Rocca S. Characterization of typings in polymorphic type discipline. In: Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS ’88), Edinburgh, Scotland, UK, July 5-8, 1988. IEEE Computer Society. ISBN 0-8186-0853-6, 1988 pp. 61-70. doi:10.1109/LICS.1988.5101.
• [27] Urzyczyn P. Type Reconstruction in Fω. Mathematical Structures in Computer Science, 1997. 7(4):329-358. doi:10.1017/S0960129597002302.
• [28] Milner R. A Theory of Type Polymorphism in Programming. J. Comput. Syst. Sci., 1978. 17(3):348-375. doi:10.1016/0022-0000(78)90014-4.
• [29] Wright AK, Felleisen M. A Syntactic Approach to Type Soundness. Inf. Comput., 1994. 115(1):38-94. doi:10.1006/inco.1994.1093.
• [30] Johnson-Freyd P. Properties of Sequent-Calculus-Based Languages. Ph.D. thesis, University of Oregon, 2018.
• [31] Urzyczyn P. The Emptiness Problem for Intersection Types. In: Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994. IEEE Computer Society. ISBN 0-8186-6310-3, 1994 pp. 300-309. doi:10.1109/LICS.1994.316059.
• [32] Bucciarelli A, Kesner D, Ronchi Della Rocca S. Inhabitation for Non-idempotent Intersection Types. Logical Methods in Computer Science, 2018. 14(3). doi:10.23638/LMCS-14(3:7)2018.
• [33] Barendregt HP, Coppo M, Dezani-Ciancaglini M. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 1983. 48(4):931-940 (1984).
• [34] Reynolds JC. Design of the Programming Language Forsythe. Report CMU-CS-96-146, Carnegie Mellon University, Pittsburgh, Pennsylvania, 1996.
• [35] Pierce BC. Intersection Types and Bounded Polymorphism. In: Bezem M, Groote JF (eds.), Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA ’93, Utrecht, The Netherlands, March 16-18, 1993, Proceedings, volume 664 of Lecture Notes in Computer Science. Springer. ISBN 3-540-56517-5, 1993 pp. 346-360. doi:10.1007/BFb0037117.
• [36] Dunfield J, Pfenning F. Type Assignment for Intersections and Unions in Call-by-Value Languages. In: Gordon AD (ed.), Foundations of Software Science and Computational Structures, 6th International Conference, FOSSACS 2003 Held as Part of the Joint European Conference on Theory and Practice of Software, ETAPS 2003, Warsaw, Poland, April 7-11, 2003, Proceedings, volume 2620 of Lecture Notes in Computer Science. Springer. ISBN 3-540-00897-7, 2003 pp. 250-266. doi:10.1007/3-540-36576-1\_16.
• [37] Dunfield J. Elaborating intersection and union types. In: Thiemann P, Findler RB (eds.), ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012. ACM. ISBN 978-1-4503-1054-3, 2012 pp. 17-28. doi:10.1145/2364527.2364534.
• [38] Hindley JR. Coppo-Dezani Types do not Correspond to Propositional Logic. Theor. Comput. Sci., 1984. 28:235-236. doi:10.1016/0304-3975(83)90074-9.
• [39] Lopez-Escobar EGK. Proof functional connectives. In: Di Prisco CA (ed.), Methods in Mathematical Logic, volume 1130 of Lecture Notes in Mathematics. Springer-Verlag, 1985 p. 208-221.
• [40] Mints G. The Completeness of Provable Realizability. Notre Dame Journal of Formal Logic, 1989. 30(3):420-441. doi:10.1305/ndjfl/1093635158.
• [41] Barendregt HP, Dekkers W, Statman R. Lambda Calculus with Types. Perspectives in logic. Cambridge University Press, 2013. ISBN 978-0-521-76614-2. URL http://www.cambridge.org/de/academic/subjects/mathematics/logic-categories-and-sets/lambda-calculus-types.
• [42] Dezani-Ciancaglini M, Ghilezan S, Venneri B. The ”Relevance” of Intersection and Union Types. Notre Dame Journal of Formal Logic, 1997. 38(2):246-269. doi:10.1305/ndjfl/1039724889.
• [43] Ronchi Della Rocca S, Roversi L. Intersection Logic. In: Fribourg L (ed.), Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference of the EACSL, volume 2142 of Lecture Notes in Computer Science. Springer, 2001 pp. 414-428. doi:10.1007/3-540-44802-0\_29.
• [44] Liquori L, Ronchi Della Rocca S. Intersection-types à la Church. Inf. Comput., 2007. 205(9):1371-1386. doi:10.1016/j.ic.2007.03.005.
• [45] Herbelin H. C’est maitenant q’on calcul, au coer de la dualité. Habilitation. Habilitation à diriger les reserches, Université Paris 11, 2005. URL http://pauillac.inria.fr/~herbelin/habilitation/memoire.ps.
• [46] Dougherty DJ, Ghilezan S, Lescanne P. Characterizing strong normalization in a language with control operators. In: Moggi E, Warren DS (eds.), Proceedings of the 6th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 24-26 August 2004, Verona, Italy. ACM. ISBN 1-58113-819-9, 2004 pp. 155-166. doi:10.1145/1013963.1013982.
• [47] Dougherty DJ, Ghilezan S, Lescanne P. Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: Extending the Coppo-Dezani heritage. Theor. Comput. Sci., 2008. 398(1-3):114-128. doi:10.1016/j.tcs.2008.01.022.
• [48] van Bakel S. Completeness and partial soundness results for intersection and union typing for λμμ. Ann. Pure Appl. Logic, 2010. 161(11):1400-1430. doi:10.1016/j.apal.2010.04.010.
• [49] Parigot M. Strong Normalization for Second Order Classical Natural Deduction. In: Proceedings of the Eighth Annual Symposium on Logic in Computer Science (LICS ’93), Montreal, Canada, June 19-23, 1993. IEEE Computer Society. ISBN 0-8186-3140-6, 1993 pp. 39-46. doi:10.1109/LICS.1993.287602.
• [50] van Bakel S, Barbanera F, de’Liguoro U. Intersection Types for the lambda-mu Calculus. Logical Methods in Computer Science, 2018. 14(1). doi: 10.23638/LMCS-14(1:2)2018.
• [51] de’Liguoro U. The approximation theorem for the Λμ-calculus. Mathematical Structures in Computer Science, 2017. 27(5):560–580. doi:10.1017/S0960129515000286.
• [52] Kikuchi K, Sakurai T. A Translation of Intersection and Union Types for the λμ-Calculus. In: Garrigue J (ed.), Programming Languages and Systems - 12th Asian Symposium, APLAS 2014, Singapore, November 17-19, 2014, Proceedings, volume 8858 of Lecture Notes in Computer Science. Springer. ISBN 978-3-319-12735-4, 2014 pp. 120-139. doi:10.1007/978-3-319-12736-1\_7.
• [53] Bernadet A, Lengrand S. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 2013. 9(4). doi:10.2168/LMCS-9(4:3)2013.
• [54] Kesner D, Vial P. Types as Resources for Classical Natural Deduction. Submitted, University Paris Diderot, 2018.
• [55] Bessai J, Chen T, Dudenhefner A, Düdder B, de’Liguoro U, Rehof J. Mixin Composition Synthesis based on Intersection Types. CoRR, 2017. abs/1712.06906. 1712.06906.
• [56] Tsukada T, Nakazawa K. Intersection and Union Type Assignment and Polarised λμμ. Draft, University of Tokyo, 2018.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2019).