A specification for dependent types in Haskell
A specification for dependent types in Haskell
复制标题
Haskell 中依赖类型的规范
DOI：
10.1145/3110275
复制
发表时间：
2017
影响因子：
--
通讯作者：
Eisenberg, Richard A.
中科院分区：
文献类型：
--
作者：
Weirich, Stephanie;Voizard, Antoine;de Amorim, Pedro Henrique;Eisenberg, Richard A.
我们提出了一个核心语义依赖Haskell，一个扩展的Haskell与全频谱依赖类型。我们的语义由两种相关的语言组成。第一种是Curry风格的依赖类型语言，具有非终止性、无关参数和相等抽象。第二个是受格拉斯哥Haskell的核心语言FC的启发，是它的显式类型的类似物，适合在GHC中实现。我们所有的结果-主要是类型安全，沿着与这两种语言相关的定理-已经使用Coq证明助手进行了形式化。因为我们的工作与Haskell向后兼容，所以我们的类型安全证明在存在非终止计算的情况下成立。然而，与其他全谱依赖类型语言（如Coq、Agda或Idris）不同，由于这种非终止性，Haskell的术语语言并不对应于一致逻辑。
We propose a core semantics for Dependent Haskell, an extension of Haskell with full-spectrum dependent types. Our semantics consists of two related languages. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compiler's core language FC, is its explicitly-typed analogue, suitable for implementation in GHC. All of our results---chiefly, type safety, along with theorems that relate these two languages---have been formalized using the Coq proof assistant. Because our work is backwards compatible with Haskell, our type safety proof holds in the presence of nonterminating computation. However, unlike other full-spectrum dependently-typed languages, such as Coq, Agda or Idris, because of this nontermination, Haskell's term language does not correspond to a consistent logic.
登录
查看更多内容
类型推断、Haskell 和依赖类型
DOI：
--
发表时间：
2013
期刊：
影响因子：
--
作者：
Adam Gundry
通讯作者：
Adam Gundry
可见型应用
DOI：
10.1007/978-3-662-49498-1_10
发表时间：
2016
期刊：
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
R. Eisenberg;Stephanie Weirich;Hamidhasan G. Ahmed
通讯作者：
Hamidhasan G. Ahmed
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