haskell - Haskell for Dummies 中的简单依赖类型示例。它们在 Haskell 的实践中如何有用？我为什么要关心依赖类型？

Question

我现在听到很多关于依赖类型的信息，我听说 DataKinds 在某种程度上与依赖类型有关(但我不确定这一点……只是在 Haskell 聚会上听说过)。

有人可以用一个 super 简单的 Haskell 示例来说明依赖类型是什么以及它有什么用处吗？

在维基百科上写到依赖类型可以帮助防止错误。你能举一个简单的例子来说明 Haskell 中的依赖类型如何防止错误吗？

我现在可以在五分钟内开始使用以防止 Haskell 代码中的错误的东西吗？

依赖类型基本上是从值到类型的函数，这在实践中如何使用？为什么这么好？

Answer 1

迟到了，这个答案基本上是一个无耻的插件。

Sam Lindley 和我写了一篇关于 Hasochism 的论文，Haskell 中依赖类型编程的乐趣和痛苦。它提供了很多现在在 Haskell 中可能实现的示例，并与 Agda/Idris 生成的依赖类型语言进行了比较(有利与否)。

虽然是学术论文，但是是关于实际程序的，你可以从Sam's repo获取代码.我们有很多小例子(例如合并排序输出的有序性)，但我们最终得到了一个文本编辑器示例，在其中我们使用宽度和高度索引来管理屏幕几何形状:我们确保组件是常规矩形(向量的向量，而不是参差不齐的列表)并且它们完全吻合。

依赖类型的关键功能是保持单独数据组件之间的一致性(例如，矩阵中的头向量和其尾中的每个向量都必须具有相同的长度)。这从来没有比编写条件代码更重要。情况(总有一天会被视为天真得可笑)是以下都是类型保留的重写

if b then t else e => if b then e else t

if b then t else e => t

if b then t else e => e

虽然我们大概正在测试 b因为它为我们提供了一些有用的洞察力，让我们了解下一步什么是合适的(甚至是安全的)，所以这些洞察力都不是通过类型系统介导的: b 的想法的真相证明 t它的错误证明 e失踪，尽管很重要。

普通的老 Hindley-Milner 确实为我们提供了一种确保某种一致性的方法。每当我们有一个多态函数

f :: forall a. r[a] -> s[a] -> t[a]

我们必须实例化 a始终如一:但是第一个参数修复了 a ，第二个参数必须配合，我们在处理结果时会学到一些有用的东西。在类型级别允许数据很有用，因为某些形式的一致性(例如事物的长度)更容易用数据(数字)表示。

但真正的突破是 GADT 模式匹配，其中模式的类型可以细化它匹配的参数的类型。你有一个长度为 n 的向量;你看看它是 nil 还是 cons；现在你知道 n是否为零。这是一种测试形式，其中每种情况下的代码类型比整体的类型更具体，因为在每种情况下，所学到的东西都会反射(reflect)在类型级别上。是 通过测试学习这使得语言至少在某种程度上依赖于类型。

这是一个愚蠢的游戏，无论你使用什么类型的语言。将类型表达式中的每个类型变量和每个原始类型都替换为 1 并以数字方式评估类型(求和，乘积， s -> t 表示 t -to-the- s )，看看你得到了什么: if你得到 0，你是一个逻辑学家；如果你得到 1，你就是一名软件工程师；如果你得到 2 的幂，你就是电子工程师；如果你得到无穷大，你就是一个程序员。这个游戏中发生的事情是一种粗略的尝试来衡量我们正在管理的信息以及我们的代码必须做出的选择。我们通常的类型系统擅长管理编码的“软件工程”方面:解包和将组件组合在一起。但是一旦做出选择，类型就没有办法观察它，一旦做出选择，类型就没有办法指导我们:非依赖类型系统近似于一个给定类型相同。这对它们在错误预防中的使用是一个非常严重的限制。