Abstract
Although systems with intersection types have many unique capabilities, there has never been a fully satisfactory explicitly typed system with intersection types. We introduce λB with branching types and types which are quantified over type selectors to provide an explicitly typed system with the same expressiveness as a system with intersection types. Typing derivations in λB effiectively squash together what would be separate parallel derivations in earlier systems with intersection types.
This work was partly supported by NSF grants CCR 9113196, 9417382, 9988529, and EIA 9806745, EPSRC grants GR/L 36963 and GR/R 41545/01, and Sun Microsystems equipment grant EDUD-7826-990410-US.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
T. Amtoft, F. Turbak. Faithful translations between polyvariant flows and polymorphic types. In Programming Languages & Systems, 9th European Symp. Programming, vol. 1782 of LNCS, pp. 26–40. Springer-Verlag, 2000.
B. Capitani, M. Loreti, B. Venneri. Hyperformulae, parallel deductions and intersection types. Electronic Notes in Theoretical Computer Science, 50, 2001. Proceedings of ICALP 2001 workshop: Bohm’s Theorem: Applications to Computer Science Theory (BOTH 2001), Crete, Greece, 2001-07-13.
M. Coppo, M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame J. Formal Logic, 21(4):685–693, 1980.
M. Dezani-Ciancaglini, S. Ghilezan, B. Venneri. The “relevance” of intersection and union types. Notre Dame J. Formal Logic, 38(2):246–269, Spring 1997.
A. Dimock, R. Muller, F. Turbak, J. B. Wells. Strongly typed flow-directed representation transformations. In Proc. 1997 Int’l Conf. Functional Programming, pp. 11–24. ACM Press, 1997.
A. Dimock, I. Westmacott, R. Muller, F. Turbak, J. B. Wells. Functioning without closure: Type-safe customized function representations for Standard ML. In Proc. 2001 Int’l Conf. Functional Programming, pp. 14–25. ACM Press, 2001.
A. Dimock, I. Westmacott, R. Muller, F. Turbak, J. B. Wells, J. Considine. Program representation size in an intermediate language with intersection and union types. In Proceedings of the Third Workshop on Types in Compilation (TIC 2000), vol. 2071 of LNCS, pp. 27–52. Springer-Verlag, 2001.
J.-Y. Girard. Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur. Thèse d’Etat, Université de Paris VII, 1972.
A. J. Kfoury. A linearization of the lambda-calculus. J. Logic Comput., 10(3), 2000. Special issue on Type Theory and Term Rewriting. Kamareddine and Klop (editors).
A. J. Kfoury, H. G. Mairson, F. A. Turbak, J. B. Wells. Relating typability and expressibility in finite-rank intersection type systems. In Proc. 1999 Int’l Conf. Functional Programming, pp. 90–101. ACM Press, 1999.
A. J. Kfoury, J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order λ-calculus. In Proc. 1994 ACM Conf. LISP Funct. Program., pp. 196–207, 1994.
A. J. Kfoury, J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In Conf. Rec. POPL’ 99: 26th ACM Symp. Princ. of Prog. Langs., pp. 161–174, 1999.
J. Palsberg, C. Pavlopoulou. From polyvariant flow information to intersection and union types. J. Funct. Programming, 11(3):263–317, May 2001.
B. C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, Feb. 1991.
G. Pottinger. A type assignment for the strongly normalizable λ-terms. In J. R. Hindley, J. P. Seldin, eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, pp. 561–577. Academic Press, 1980.
J. C. Reynolds. Towards a theory of type structure. In Colloque sur la Programmation, vol. 19 of LNCS, pp. 408–425, Paris, France, 1974. Springer-Verlag.
J. C. Reynolds. Design of the programming language Forsythe. In P. O’Hearn, R. D. Tennent, eds., Algol-like Languages. Birkhauser, 1996.
S. Ronchi Della Rocca, L. Roversi. Intersection logic. In Computer Science Logic, CSL’ 01. Springer-Verlag, 2001.
F. Turbak, A. Dimock, R. Muller, J. B. Wells. Compiling with polymorphic and polyvariant flow types. In Proc. First Int’l Workshop on Types in Compilation, June 1997.
P. Urzyczyn. Type reconstruction in F ω. Math. Structures Comput. Sci., 7(4):329–358, 1997.
B. Venneri. Intersection types as logical formulae. J. Logic Comput., 4(2):109–124, Apr. 1994.
J. B. Wells. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Symp. Logic in Comp. Sci., pp. 176–185, 1994. Superseded by [24].
J. B. Wells. Typability is undecidable for F+eta. Tech. Rep. 96-022, Comp. Sci. Dept., Boston Univ., Mar. 1996.
J. B. Wells. Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic, 98(1–3):111–156, 1999. Supersedes [22].
J. B. Wells, A. Dimock, R. Muller, F. Turbak. A typed intermediate language for flow-directed compilation. In Proc. 7th Int’l Joint Conf. Theory & Practice of Software Development, pp. 757–771, 1997. Superseded by [26].
J. B. Wells, A. Dimock, R. Muller, F. Turbak. A calculus with polymorphic and polyvariant flow types. J. Funct. Programming, 200X. To appear. Supersedes [25].
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wells, J.B., Haack, C. (2002). Branching Types. In: Le Métayer, D. (eds) Programming Languages and Systems. ESOP 2002. Lecture Notes in Computer Science, vol 2305. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45927-8_9
Download citation
DOI: https://doi.org/10.1007/3-540-45927-8_9
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43363-7
Online ISBN: 978-3-540-45927-9
eBook Packages: Springer Book Archive