Andrej Dudenhefner
Skip Abstract Section
Skip Supplemental Material SectionAbstract
We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides an algebraic and algorithmic theory of approximation of classical principal types in terms of computable bases of abstract vector spaces (more precisely, semimodules), and it shows a systematic connection of dimensional calculi to the theory of approximants. Finite, computable bases are shown to span standard principal typings of a given term for sufficiently high dimension, thereby providing an approximation to standard principality by type inference, and capturing it precisely for sufficiently large dimensional parameter. Subsidiary results include decidability of principal inhabitation for intersection types (given a type does there exist a normal form for which the type is principal?). Remarkably, combining bounded type inference with principal inhabitation allows us to compute approximate normal forms of arbitrary terms without using beta-reduction.
Supplemental Material
- João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In Programming Languages and Systems -26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 1–28.Google Scholar
- Michael Artin. 2011. Algebra (2nd edition). Pearson Education.Google Scholar
- Henk P. Barendregt. 1984. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, 2nd Edition. Elsevier Science Publishers.Google Scholar
- Henk P. Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A Filter Lambda Model and the Completeness of Type Assignment. Journal of Symbolic Logic 48, 4 (1983), 931–940.Google ScholarCross Ref
- Henk P. Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press. Google ScholarDigital Library
- Gérard Boudol. 2008. On strong normalization and type inference in the intersection type discipline. Theor. Comput. Sci. 398, 1-3 (2008), 63–81. Google ScholarDigital Library
- Sébastien Carlier and Joe B. Wells. 2005. Expansion: the Crucial Mechanism for Type Inference with Intersection Types: A Survey and Explanation. Electr. Notes Theor. Comput. Sci. 136 (2005), 173–202. Google ScholarDigital Library
- Sébastien Carlier and Joe B. Wells. 2012. The Algebra of Expansion. Fundam. Inform. 121, 1-4 (2012), 43–82. Google ScholarDigital Library
- Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An Extension of Basic Functionality Theory for Lambda-Calculus. Notre Dame Journal of Formal Logic 21 (1980), 685–693.Google ScholarCross Ref
- Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sallé. 1979. Functional characterization of some semantic equalities inside λ-calculus. In ICALP International Colloquium on Automata, Languages, and Programming. Springer LNCS 71. Google ScholarDigital Library
- Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1980. Principal Type Schemes and λ-Calculus Semantics. In R. Hindley and J. Seldin (Eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Accademic Press, London, 480–490.Google Scholar
- Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Zeitschrift für mathematische Logik und Grundlagen der Mathematik (1981), 45–58.Google Scholar
- Mario Coppo and Paola Giannini. 1995. Principal Types and Unification for a Simple Intersection Type System. Inf. Comput. 122, 1 (1995), 70–96. Google ScholarDigital Library
- Boris Düdder, Moritz Martens, and Jakob Rehof. 2013. Intersection Type Matching with Subtyping. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. 125–139.Google Scholar
- Andrej Dudenhefner and Jakob Rehof. 2017a. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 15:1–15:14.Google Scholar
- Andrej Dudenhefner and Jakob Rehof. 2017b. Intersection type calculi of bounded dimension. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. 653–665. Google ScholarDigital Library
- Andrej Dudenhefner and Jakob Rehof. 2017c. Typability in bounded dimension. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. 1–12.Google ScholarCross Ref
- Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In 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. 331–350. Google ScholarDigital Library
- Jonathan S. Golan. 1999. Semirings and their Applications. Springer.Google Scholar
- Hans Hüttel, Ivan Lanese, Vasco T. Vasconcelos, Luís Caires, Marco Carbone, Pierre-Malo Deniélou, Dimitris Mostrous, Luca Padovani, António Ravara, Emilio Tuosto, Hugo Torres Vieira, and Gianluigi Zavattaro. 2016. Foundations of Session Types and Behavioural Contracts. Comput. Surveys 49, 1, Article 3 (April 2016), 36 pages. Google ScholarDigital Library
- Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, and J. B. Wells. 1999. Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract). In Proceedings of the fourth ACM SIGPLAN International Conference on Functional Programming (ICFP ’99), Paris, France, September 27-29, 1999., Didier Rémi and Peter Lee (Eds.). ACM, 90–101. Google ScholarDigital Library
- Assaf J. Kfoury and Joe B. Wells. 1999. Principality and Decidable Type Inference for Finite-Rank Intersection Types. In POPL 1999, Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, TX, USA, January 20-22, 1999. 161–174. Google ScholarDigital Library
- Assaf J. Kfoury and Joe B. Wells. 2004. Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311, 1-3 (2004), 1–70. Google ScholarDigital Library
- Toshihiko Kurata and Masako Takahashi. 1995. Decidable properties of intersection type systems. In TLCA 1995, Proceedings of Typed Lambda Calculus and Applications (LNCS), Vol. 902. Springer, 297–311. Google ScholarDigital Library
- Daniel Leivant. 1983. Polymorphic Type Inference. In POPL 1983, Proceedings of the 10th ACM Symposium on Principles of Programming Languages. 88–98. Google ScholarDigital Library
- Luigi Liquori and Claude Stolze. 2018. The Delta-calculus: syntax and types. CoRR abs/1803.09660 (2018). arXiv: 1803.09660 http://arxiv.org/abs/1803.09660Google Scholar
- Conor McBride. 2016. I Got Plenty o’ Nuttin’. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207–233.Google Scholar
- Grigory E. Mints. 1981. Closed categories and the theory of proofs. Journal of Soviet Mathematics 15, 1 (1981), 45–62.Google ScholarCross Ref
- Peter Møller Neergaard and Harry G. Mairson. 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming, ICFP 2004, Snow Bird, UT, USA, September 19-21, 2004. 138–149. Google ScholarDigital Library
- Garrel Pottinger. 1980. A Type Assignment for the Strongly Normalizable Lambda-Terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Hindley and J. Seldin (Eds.). Academic Press, 561–577.Google Scholar
- Jakob Rehof and Paweł Urzyczyn. 2012. The Complexity of Inhabitation with Explicit Intersection. In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday (LNCS), Robert L. Constable and Alexandra Silva (Eds.), Vol. 7230. Springer, 256–270. Google ScholarDigital Library
- John C. Reynolds. 1996. Design of the Programming Language Forsythe. Technical Report CMU-CS-96-146. CMU.Google Scholar
- Simona Ronchi Della Rocca. 1988. Principal Type Scheme and Unification for Intersection Type Discipline. Theor. Comput. Sci. 59 (1988), 181–209. Google ScholarDigital Library
- Simona Ronchi Della Rocca and Betti Venneri. 1984. Principal Type Schemes for an Extended Type Theory. Theor. Comput. Sci. 28 (1984), 151–169.Google ScholarCross Ref
- Takeshi Tsukada and C.-H. Luke Ong. 2016. Plays as Resource Terms via Non-idempotent Intersection Types. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. 237–246. Google ScholarDigital Library
- Paweł Urzyczyn. 1999. The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64, 3 (1999), 1195–1215.Google ScholarCross Ref
- Steffen van Bakel. 1993. Principal Type Schemes for the Strict Type Assignment System. J. Log. Comput. 3, 6 (1993), 643–670.Google ScholarCross Ref
- Steffen van Bakel. 2011. Strict Intersection Types for the Lambda Calculus. Comput. Surveys 43, 3 (2011). Google ScholarDigital Library
Index Terms
- Principality and approximation under dimensional bound
Recommendations
The inhabitation problem for intersection types
CATS '08: Proceedings of the fourteenth symposium on Computing: the Australasian theory - Volume 77In the system λΛ of intersection types, without ω, the problem as to whether an arbitrary type has an inhabitant, has been shown to be undecidable by Urzyczyn in [10]. For one subsystem of λΛ, that lacks the Λ-introduction rule, the inhabitation problem ...
Intersection type calculi of bounded dimension
POPL '17A notion of dimension in intersection typed λ-calculi is presented. The dimension of a typed λ-term is given by the minimal norm of an elaboration (a proof theoretic decoration) necessary for typing the term at its type, and, intuitively, measures ...
A typed lambda calculus with intersection types
Intersection types are well known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type operator is a meta-level operator, that is, there is no direct logical ...
Comments