2012/01/05 by Sergueï Lenglet, Lenglet, Sergueï, J. B. Wells +1
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Logic, programming, and type systems #Programming Languages (cs.PL) #Software Engineering Research #cs.PL
paper · pdf · doi:10.48550/arxiv.1201.1101
Long version of the corresponding ESOP 2012 paper
arxiv created 2012/01/05 · openalex publication_date 2012/01/05 · arxiv updated 2012/01/06 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Expansion is an operation on typings (i.e., pairs of typing environments and result types) defined originally in type systems for the lambda-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 forall-quantifiers. We present System 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.