Hasochism: the pleasure and pain of dependently typed haskell programming
Hasochism: the pleasure and pain of dependently typed haskell programming
复制标题
Hasochism：依赖类型 Haskell 编程的快乐和痛苦
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Conor McBride
中科院分区：
文献类型：
--
作者：
S. Lindley;Conor McBride
Haskell的类型系统已经超过了Hindley-Milner的根源，以至于它现在延伸到了依赖类型的编程的基础知识。在本文中，我们对Haskell中的依赖类型进行了整理和分类，以编程，并贡献一些新的技术。特别是，通过扩展的示例---合并 - 选项和矩形瓷砖---我们展示了如何利用Haskell的约束求解器作为定理宣传员，并提供代码，作为AGDA程序员，我们羡慕。我们探讨了模拟因函数空间主题的变化所涉及的妥协，以帮助程序员提出依赖类型的工作，并更广泛地为Haskell和依赖性类型的语言提供了不断发展的语言设计。
Haskell's type system has outgrown its Hindley-Milner roots to the extent that it now stretches to the basics of dependently typed programming. In this paper, we collate and classify techniques for programming with dependent types in Haskell, and contribute some new ones. In particular, through extended examples---merge-sort and rectangular tilings---we show how to exploit Haskell's constraint solver as a theorem prover, delivering code which, as Agda programmers, we envy. We explore the compromises involved in simulating variations on the theme of the dependent function space in an attempt to help programmers put dependent types to work, and to inform the evolving language design both of Haskell and of dependently typed languages more broadly.