  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.
