Reflections on existential types
Jonathan Sterling

TL;DR
This paper reconstructs existential types using reflective subuniverses and dependent sums, providing a semantic foundation for first-class modules and models of ML-style languages with effects.
Contribution
It offers a novel semantic account of first-class modules via reflective subuniverses, connecting traditional modules with modal operators and extending models to include recursive modules and effects.
Findings
Semantic models for ML-style languages with first-class modules and effects
Justification of first-class module rules in OCaml and MoscowML
Models accommodating higher-order recursive modules and store
Abstract
Existential types are reconstructed in terms of small reflective subuniverses and dependent sums. The folklore decomposition detailed here gives rise to a particularly simple account of first-class modules as a mode of use of traditional second-class modules in connection with the modal operator induced by a reflective subuniverse, leading to a semantic justification for the rules of first-class modules in languages like OCaml and MoscowML. Additionally, we expose several constructions that give rise to semantic models of ML-style programming languages with both first-class modules and realistic computational effects, culminating in a model that accommodates higher-order first-class recursive modules and higher-order store.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Software Engineering Research · Model-Driven Software Engineering Techniques
