Infinite Intersection and Union Types for the Lazy Lambda Calculus
A type theory with infinitary intersection and union types for the lazy λ-calculus is introduced. Types are viewed as upper closed subsets of a Scott domain. Intersection and union type constructors are interpreted as the set-theoretic intersection and union, respectively, even when they are not finite. The assignment of types to λ-terms extends naturally the basic type assignment system. We prove soundness and completeness using a generalization of Abramsky’s finitary domain logic for applicative transition systems.
KeywordsDistributive Lattice Intersection Type Type Theory Union Type Type Constructor
Unable to display preview. Download preview PDF.
- 1.S. Abramsky. The lazy lambda calculus. In Research Topics in Functional Programming, pp. 65–117, Addison Wesley, 1990.Google Scholar
- 3.F. Barbanera and M. Dezani-Ciancaglini. Intersection and union types. In Proceedings of TACS’91, vol. 526 of Lecture Notes in Computer Science, pp. 651–674. Springer-Verlag, 1991.Google Scholar
- 5.H. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North Holland, 1984.Google Scholar
- 8.M.M. Bonsangue. Topological Dualities in Semantics. Vol. 8 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1997.Google Scholar
- 11.M. Dezani-Ciancaglini, F. Honsell and Y. Motohama. Compositional characterizations of λ-terms using intersection types. In Proceedings of MFCS 2000, vol. 1893 of Lecture Notes in Computer Science, pp. 304–313. Springer-Verlag, 2000.Google Scholar
- 13.P.T. Johnstone. Stone Spaces. Cambridge University Press, 1982.Google Scholar
- 14.D. Leivant. Discrete polymorphism. In Proceedings of 1990 ACM Conference of LISP and Functional Programming, pp. 288–297.Google Scholar
- 15.B.C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.Google Scholar
- 16.G. Pottinger. A type assignment for the strongly normalizable λ-term. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 561–577. Academic Press, 1980.Google Scholar