一句话：报告在 GHC 中编码依赖类型编程的工业经验：可行且有价值，但成本高昂。
本文是一篇工业经验报告，探讨如何利用 GHC 的高级特性在 Haskell 中编码依赖类型编程风格。作者团队用这种“依赖类型 Haskell”构建了一个性能关键的库，该库是多个验证工具的核心组件。报告描述了在 Haskell 类型系统表达力边缘编程带来的价值，包括更强的静态保证和抽象能力，也总结了由此产生的困难，如类型错误复杂、开发与维护成本高，以及他们为应对这些困难所采用的一些方法。核心结论是：这种做法可行且有显著价值，但成本高昂。
Recent versions of the Haskell compiler GHC have a number of advanced features that allow many idioms from dependently typed programming to be encoded. We describe our experiences using this "dependently typed Haskell" to construct a performance-critical library that is a key component in a number of verification tools. We have discovered that it can be done, and it brings significant value, but also at a high cost. In this experience report, we describe the ways in which programming at the edge of what is expressible in Haskell's type system has brought us value, the difficulties that it has imposed, and some of the ways we coped with the difficulties.
@article{paperbot613,
title = {Dependently typed Haskell in industry (experience report)},
author = {David Thrane Christiansen and Iavor S. Diatchki and Robert Dockins and Joe Hendrix and Tristan Ravitch},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {ICFP},
year = {2019},
doi = {10.1145/3341704}
}