论文标题
对存在类型的思考
Reflections on existential types
论文作者
论文摘要
存在类型是根据小反射子输入和相关总和重建的。此处详细介绍的民间传说分解引起了对一流模块的特别简单描述，作为与反光子Universe引起的模态操作员有关的传统二等模块的使用方式，从而为OCAML和MoscowMl等语言中的一流模块规则提供了语义上的理由。此外，我们揭示了几种结构，这些结构带来了具有一流模块和现实计算效应的ML式编程语言的语义模型，最终以适合高阶一级递归模块和高级存储的模型。
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.
