Abstract
Types are often used to control and analyze computer programs. Intersection types give great flexibility, but have been difficult to implement. The ! operator, used to distinguish between linear and non-linear types, has good potential for better resource-usage tracking, but has not been as flexible as one might want and has been difficult to use in compositional analysis. We introduce System E, a type system with expansion variables, linear intersection types, and the ! type constructor for creating non-linear types. System E is designed for maximum flexibility in automatic type inference and for ease of automatic manipulation of type information. Expansion variables allow postponing the choice of which typing rules to use until later constraint solving gives enough information to allow making a good choice. System E removes many difficulties that expansion variables had in the earlier System I and extends expansion variables to work with ! in addition to the intersection type constructor. We present subject reduction for call-by-need evaluation and discuss program analysis in System E.
Supported by grants: EC FP5 IST-2001-33477, EPSRC GR/L 41545/01, NATO CRG 971607, NSF 0113193 (ITR), Sun Microsystems 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
Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. In: Conf. Rec. 22nd Ann. ACM Symp. Princ. of Prog. Langs. (1995)
Barendregt, H., Coppo, M., Dezani-Ciancaglini, M.: A filter lambda model and the completeness of type assignment. J. Symbolic Logic 48(4) (1983)
Carlier, S.: Polar type inference with intersection types and ω. In: Proceedings of the 2nd Workshop on Intersection Types and Related Systems, The ITRS 2002 proceedings. Elec. Notes in Theoret. Comp. Sci., vol. 70(1) (2002)
Coppo, M., Dezani-Ciancaglini, M., Venneri, B.: Principal type schemes and λ- calculus semantics. In: Hindley, J.R., Seldin, J.P. (eds.) To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. Academic Press, London (1980)
Damas, L., Milner, R.: Principal type schemes for functional programs. In: Conf. Rec. 9th Ann. ACM Symp. Princ. of Prog. Langs. (1982)
Girard, J.-Y.: Interprétation Fonctionnelle et Elimination des Coupures de l’Arithmétique d’Ordre Supérieur. Thèse d’Etat, Université de Paris VII (1972)
Jim, T.: What are principal typings and what are they good for? In: Conf. Rec. POPL 1996: 23rd ACM Symp. Princ. of Prog. Langs. (1996)
Kfoury, J., Wells, J.B.: Principality and decidable type inference for finite-rank intersection types. In: POPL 1999 [14]. Superseded by [10] (1999)
Kfoury, J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Supersedes [8] (2003)
Kfoury, J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theoret. Comput. Sci. 200X (to appear). Supersedes [8]. For omitted proofs, see the longer report [9]
Kobayashi, N.: Quasi-linear types. In: POPL 1999 [14] (1999)
Milner, R.: A theory of type polymorphism in programming. J. Comput. System Sci. 17 (1978)
Mitchell, J.C., Plotkin, G.D.: Abstract types have existential type. ACM Trans. on Prog. Langs. & Systs. 10(3) (1988)
Conf. Rec. POPL 1999: 26th ACM Symp. Princ. of Prog. Langs. (1999)
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium. LNCS, vol. 19. Springer, Heidelberg (1974)
Turner, D.N., Wadler, P.: Operational interpretations of linear logic. Theoret. Comput. Sci. 227(1-2) (1999)
Turner, D.N., Wadler, P., Mossin, C.: Once upon a type. In: 7th International Conference on Functional Programming and Computer Architecture, San Diego, California (1995)
van Bakel, S.J.: Intersection type assignment systems. Theoret. Comput. Sci. 151(2) (1995)
Wadler, P.: Linear types can change the world. In: Broy, M., Jones, C.B. (eds.) IFIP TC 2 Working Conference on Programming Concepts and Methods (1990)
Wadler, P.: Is there a use for linear logic? In: Partial Evaluation and Semantics- Based Program Manipulation (PEPM). ACM Press, New York (1991)
Wansbrough, K., Jones, S.P.: Once upon a polymorphic type. In: POPL 1999 [14] (1999)
Wells, J.B.: The essence of principal typings. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol. 2380, p. 913. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J. (2004). System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. In: Schmidt, D. (eds) Programming Languages and Systems. ESOP 2004. Lecture Notes in Computer Science, vol 2986. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24725-8_21
Download citation
DOI: https://doi.org/10.1007/978-3-540-24725-8_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21313-0
Online ISBN: 978-3-540-24725-8
eBook Packages: Springer Book Archive