Modeling Abstract Types in Modules with Open Existential Types

摘要

We propose FY, a calculus of open existential types that is an ex-tension of System F obtained by decomposing the introduction andelimination of existential types into more atomic constructs. Openexistential types model modular type abstraction as done in mod-ule systems. The static semantics of FY adapts standard techniquesto deal with linearity of typing contexts, its dynamic semantics is asmall-step reduction semantics that performs extrusion of type ab-straction as needed during reduction, and the two are related by sub-ject reduction and progress lemmas. Applying the Curry-Howardisomorphism, FY can be also read back as a logic with the same ex-pressive power as second-order logic but with more modular waysof assembling partial proofs. We also extend the core calculus tohandle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new for-malization of (a minor variant of) Dreyer's internal language forrecursive and mixin modules.