Abstract
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the λ-calculus with intersection types in order to obtain principal (i.e., most informative, strongest) typings. In a type inference scenario, expansion allows postponing choices for whether and how to use non-syntax-driven typing rules (e.g., intersection introduction) until enough information has been gathered to make the right decision. Furthermore, these choices can be equivalent to inserting uses of such typing rules at deeply nested positions in a typing derivation, without needing to actually inspect or modify (or even have) the typing derivation. Expansion has in recent years become simpler due to the use of expansion variables (e.g., in System E).
This paper extends expansion and expansion variables to systems with ∀-quantifiers. We present Fs, an extension of System F with expansion, and prove its main properties. This system turns type inference into a constraint solving problem; this could be helpful to design a modular type inference algorithm for System F types in the future.
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
Carlier, S., Polakow, J., Wells, J.B., Kfoury, A.J.: System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 294–309. Springer, Heidelberg (2004)
Carlier, S., Wells, J.B.: Expansion: the crucial mechanism for type inference with intersection types: A survey and explanation. Electr. Notes Theor. Comput. Sci. 136, 173–202 (2005)
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, pp. 535–560. Academic Press (1980)
Damas, L., Milner, R.: Principal type-schemes for functional programs. In: POPL, pp. 207–212 (1982)
Garrigue, J., Rémy, D.: Semi-explicit first-class polymorphism for ML. Inf. Comput. 155(1-2), 134–169 (1999)
Giannini, P., Ronchi Della Rocca, S.: Type Inference in Polymorphic Type Discipline. In: Ito, T., Meyer, A.R. (eds.) TACS 1991. LNCS, vol. 526, pp. 18–37. Springer, Heidelberg (1991)
Girard, J.-Y.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII (1972)
Kfoury, A.J., Wells, J.B.: Principality and type inference for intersection types using expansion variables. Theor. Comput. Sci. 311(1-3), 1–70 (2004)
Läufer, K., Odersky, M.: Polymorphic type inference and abstract data types. ACM Trans. Program. Lang. Syst. 16(5), 1411–1430 (1994)
Le Botlan, D., Rémy, D.: MLF: raising ML to the power of System F. In: ICFP, pp. 27–38. ACM (2003)
Le Botlan, D., Rémy, D.: Recasting MLF. Inf. Comput. 207(6), 726–785 (2009)
Leijen, D.: Flexible types: robust type inference for first-class polymorphism. In: POPL, pp. 66–77. ACM (2009)
Leivant, D.: Polymorphic type inference. In: POPL, pp. 88–98 (1983)
Lenglet, S., Wells, J.B.: Expansion for universal quantifiers (2012), http://arxiv.org/abs/1201.1101
Margaria, I., Zacchi, M.: Principal typing in a forall-and-discipline. J. Log. Comput. 5(3), 367–381 (1995)
Milner, R.: A theory of type polymorphism in programming. J. Comput. Syst. Sci. 17(3), 348–375 (1978)
Mitchell, J.C.: Polymorphic type inference and containment. Inf. Comput. 76(2/3), 211–249 (1988)
Rémy, D.: Programming Objects with ML-ART, an Extension to ML with Abstract and Record Types. In: Hagiya, M., Mitchell, J.C. (eds.) TACS 1994. LNCS, vol. 789, pp. 321–346. Springer, Heidelberg (1994)
Reynolds, J.C.: Towards a Theory of Type Structure. In: Loeckx, J. (ed.) ICALP 1974. LNCS, vol. 14, pp. 408–423. Springer, Heidelberg (1974)
Ronchi Della Rocca, S., Venneri, B.: Principal type schemes for an extended type theory. Theoretical Computer Science 28, 151–169 (1984)
van Bakel, S., Barbanera, F., Fernández, M.: Polymorphic Intersection Type Assignment for Rewrite Systems with Abstraction and β-Rule. In: Coquand, T., Nordström, B., Dybjer, P., Smith, J. (eds.) TYPES 1999. LNCS, vol. 1956, pp. 41–60. Springer, Heidelberg (2000)
Vasconcellos, C., Figueiredo, L., Camarão, C.: Practical type inference for polymorphic recursion: an implementation in haskell. J. UCS 9(8), 873–890 (2003)
Vytiniotis, D., Weirich, S., Peyton-Jones, S.: FPH: first-class polymorphism for Haskell. In: ICFP, pp. 295–306. ACM (2008)
Vytiniotis, D., Weirich, S., Peyton-Jones, S.: Boxy types: inference for higher-rank types and impredicativity. In: ICFP, pp. 251–262. ACM (2006)
Wells, J.B.: Typability and type checking in System F are equivalent and undecidable. Ann. Pure Appl. Logic 98(1-3), 111–156 (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, pp. 913–925. Springer, Heidelberg (2002)
Wells, J.B., Haack, C.: Branching Types. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 115–132. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lenglet, S., Wells, J.B. (2012). Expansion for Universal Quantifiers. In: Seidl, H. (eds) Programming Languages and Systems. ESOP 2012. Lecture Notes in Computer Science, vol 7211. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28869-2_23
Download citation
DOI: https://doi.org/10.1007/978-3-642-28869-2_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-28868-5
Online ISBN: 978-3-642-28869-2
eBook Packages: Computer ScienceComputer Science (R0)