Modeling Abstract Types in Modules with Open Existential Types, by BenoÃ®t Montagu Didier RÃ©my:
We propose F^{¥}, a calculus of open existential types that is an extension of System F obtained by decomposing the introduction and elimination of existential types into more atomic constructs. Open existential types model modular type abstraction as done in module systems. The static semantics of F^{¥} adapts standard techniques to deal with linearity of typing contexts, its dynamic semantics is a small-step reduction semantics that performs extrusion of type abstraction as needed during reduction, and the two are related by subject reduction and progress lemmas. Applying the Curry-Howard isomorphism, F^{¥} can be also read back as a logic with the same expressive power as second-order logic but with more modular ways of assembling partial proofs. We also extend the core calculus to handle the double vision problem as well as type-level and term-level recursion. The resulting language turns out to be a new formalization of (a minor variant of) Dreyerâ€™s internal language for recursive and mixin modules.
This approach to existentials seems to considerably improve their power and simplify their use. It also brings us one step closer to first-class modules!
Recent comments
2 hours 22 min ago
9 hours 29 min ago
1 day 4 hours ago
2 days 11 hours ago
2 days 21 hours ago
3 days 7 hours ago
3 days 10 hours ago
3 days 11 hours ago
3 days 14 hours ago
3 days 19 hours ago