Skip to Main content Skip to Navigation
Conference papers

Expansion for Universal Quantifiers

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 System F s , 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Sergueï Lenglet <>
Submitted on : Wednesday, November 30, 2016 - 2:37:44 PM
Last modification on : Tuesday, December 29, 2020 - 10:02:01 AM
Long-term archiving on: : Monday, March 27, 2017 - 9:07:13 AM


Files produced by the author(s)



Sergueï Lenglet, J Wells. Expansion for Universal Quantifiers. European Symposium On Programming (ESOP 2012), Mar 2012, Tallinn, Estonia. pp.456 - 475, ⟨10.1007/978-3-642-28869-2_23⟩. ⟨hal-01405792⟩



Record views


Files downloads