Dependent ML - An approach to practical programming with dependent types
Dependent ML - An approach to practical programming with dependent types
复制标题
DOI：
10.1017/s0956796806006216
复制
发表时间：
2007-03-01
影响因子：
1.1
通讯作者：
Xi, Hongwei
中科院分区：
文献类型：
--
作者：
Xi, Hongwei
我们提出了一种用受限形式的依赖类型来丰富ML类型系统的方法，其中类型索引项需要从给定的类型索引语言L中提取，该语言完全独立于运行时程序，从而导致DML(L)语言模式。这种丰富允许更精确的类型信息的规范和推断，从而促进程序错误检测和编译器优化。本文的主要贡献在于我们的语言设计，它可以有效地支持依赖类型在实际编程中的使用。特别是，这种设计使得在存在引用和异常等影响的情况下适应依赖类型既自然又简单。
We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language L that is completely separate from run-time programs, leading to the DML(L) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.