A role for dependent types in Haskell
A role for dependent types in Haskell
复制标题
Haskell 中依赖类型的角色
DOI：
10.1145/3341705
复制
发表时间：
2019
影响因子：
--
通讯作者：
Eisenberg, Richard A.
中科院分区：
文献类型：
--
作者：
Weirich, Stephanie;Choudhury, Pritam;Voizard, Antoine;Eisenberg, Richard A.
现代Haskell支持零成本强制转换，在这种机制中，共享相同运行时表示的类型可以在不同类型之间自由转换。为了确保这种转换的安全性和可取性，该特性依赖于一种防止无效强制转换的机制。在这项工作中，我们展示了如何将角色合并到依赖类型系统中，并使用Coq证明助手证明结果系统是可靠的。我们将这项工作设计为为格拉斯哥Haskell编译器添加依赖类型的基础，但我们也希望它对其他依赖类型语言的设计者有用，他们可能希望采用Haskell的安全强制特性。
Modern Haskell supportszero-costcoercions, a mechanism where types that share the same run-time representation may be freely converted between. To make sure such conversions are safe and desirable, this feature relies on a mechanism ofrolesto prohibit invalid coercions. In this work, we show how to incorporate roles into dependent types systems and prove, using the Coq proof assistant, that the resulting system is sound. We have designed this work as a foundation for the addition of dependent types to the Glasgow Haskell Compiler, but we also expect that it will be of use to designers of other dependently-typed languages who might want to adopt Haskell’s safe coercions feature.
登录
查看更多内容
使用内涵类型分析编译多态性
DOI：
10.1145/199448.199475
发表时间：
1995
期刊：
Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applications
影响因子：
--
作者：
R. Harper;G. Morrisett
通讯作者：
G. Morrisett
类型推断、Haskell 和依赖类型
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Adam Gundry
通讯作者：
Adam Gundry
Type:Type 的多态 Lambda 演算
DOI：
--
发表时间：
1986
期刊：
影响因子：
--
作者：
L. Cardelli
通讯作者：
L. Cardelli
模态类型理论中的内涵性、外延性和证明无关性
DOI：
10.1109/lics.2001.932499
发表时间：
2001
期刊：
Proceedings 16th Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
F. Pfenning
通讯作者：
F. Pfenning
使用交叉类型绑定器和子类型扩展纯类型系统的构造的隐式演算
DOI：
--
发表时间：
2001
期刊：
影响因子：
--
作者：
Alexandre Miquel
通讯作者：
Alexandre Miquel