Concoqtion: indexed types now!
Concoqtion: indexed types now!
复制标题
Concoqtion：现在索引类型！
DOI：
10.1145/1244381.1244400
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
Walid Taha
中科院分区：
文献类型：
--
作者：
Seth Fogarty;E. Pasalic;Jeremy G. Siek;Walid Taha
在Cardelli的开创性努力将近20年后，编程语言社区正在积极地寻求将ω风格索引类型合并到编程语言中的方法。本文提倡Concoqtion，这是一种实用的方法，可以向成熟的编程语言中添加这种高度表达的类型。将该方法应用于MetaOCaml，使用Coq证明检查器保守地扩展Hindley-Milner类型推理。实现MetaOCaml concontion需要对语法、类型检查器和编译器进行最小的修改；并产生了一种在符号上可与主要提案相媲美的语言。生成的语言在类型系统中提供了无限的表达性，同时保持了可判定性。此外，程序员不仅可以利用编程语言的各种库，还可以利用索引类型的各种库。通过一些小示例和一个实现静态类型领域特定语言的案例研究，说明了在MetaOCaml concontion中的编程。
Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate Fω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.