Reflections on existential types

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.