为什么不依赖类型？

依赖类型实际上只是值和类型级别的统一，所以你可以参数化类型的值(在哈斯克尔类型类和参数多态已经可以实现) ，你可以参数化类型的值(严格来说，在哈斯克尔还不可能，尽管 DataKinds非常接近)。

编辑: 显然，从这一点开始，我错了(参见@Pigworker 的评论)。我会把剩下的部分保存下来，作为我被灌输的神话的记录。校对: P

据我所知，转向完全依赖类型的问题在于，它将打破类型和值级别之间的相位限制，这种限制允许 Haskell 被编译为具有擦除类型的高效机器代码。以我们目前的技术水平，依赖类型的语言 必须的在某个时候会通过解释器(或者立即通过，或者在编译成依赖类型的字节码或类似代码之后通过)。

这不一定是一个根本性的限制，但我个人认为，目前还没有任何研究在这方面看起来很有希望，但尚未进入 GHC。如果其他人知道更多，我很乐意被纠正。

依赖性输入 Haskell 现在？

Haskell 在很小程度上是一种依赖类型的语言。有一种类型级别数据的概念，由于 DataKinds的存在，现在类型化更加合理，并且有一些方法(GADTs)可以提供运行时 因此，运行时内容的值有效地显示在类型中就是依赖类型化的语言。

简单数据类型的类型级别为 升职了，因此 它们包含的内容可以用在类型中

data Nat = Z | S Nat


data Vec :: Nat -> * -> * where
VNil   :: Vec Z x
VCons  :: x -> Vec n x -> Vec (S n) x

成为可能，并与它，定义，如

vApply :: Vec n (s -> t) -> Vec n s -> Vec n t
vApply VNil         VNil         = VNil
vApply (VCons f fs) (VCons s ss) = VCons (f s) (vApply fs ss)

这是很好的。注意，长度 n是一个纯静态的东西 该函数，确保输入和输出向量具有 相同的长度，即使该长度在执行 相比之下，这要困难得多(也就是说，不可能) 实现一个函数，使 n拷贝给定的 x(它 是 pure到 vApply的 <*>)

vReplicate :: x -> Vec n x

因为知道在运行时要复制多少份是至关重要的 单身。

data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)

对于任何可升级的类型，我们可以构建单例家族，索引 类型的运行时副本所占用的提升类型 Natty n是类型级别 < code > n 的运行时副本的类型 : : : Nat . 我们现在可以写

vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy     x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)

因此，类型级别的值与运行时值绑定在一起: 检查运行时副本提炼了 即使术语和类型是分开的，我们也可以 以独立类型的方式工作，方法是使用 singleton 构造作为 一种环氧树脂，在相之间形成键，这是一种 允许在类型中使用任意的运行时表达式还有很长的路要走，但它并非一无是处。

什么是恶心? 什么是丢失？

让我们对这项技术施加一点压力，看看会有什么结果 我们可能会得到这样的想法: 单例应该是可管理的 更隐晦一点

class Nattily (n :: Nat) where
natty :: Natty n
instance Nattily Z where
natty = Zy
instance Nattily n => Nattily (S n) where
natty = Sy natty

让我们可以写，比如说,

instance Nattily n => Applicative (Vec n) where
pure = vReplicate natty
(<*>) = vApply

这是可行的，但是现在这意味着我们原来的 Nat类型已经产生了 三本: 一本，一个独生子女家庭和一个独生子女班。我们 交换显式 Natty n值的过程相当繁琐 和 Nattily n字典。此外，Natty不是 Nat: 我们有 对运行时值有某种依赖性，但不是在 没有完全依赖类型的语言使依赖 打字这么复杂！

同时，虽然 Nat可以被提升，但是 Vec不能，你不能 通过索引类型进行索引。完全依赖于依赖类型的语言强加 没有这样的限制，在我的职业生涯中，作为一个依赖打字的炫耀者, 我已经学会了在我的演讲中包括两层索引的例子, 只是为了教那些做了单层索引的人 很难，但可能不指望我像一个房子的 平等。 GADT 通过翻译 当给构造函数提供一个 特定的返回类型变成明确的方程式要求，像这样。

data Vec (n :: Nat) (x :: *)
= n ~ Z => VNil
| forall m. n ~ S m => VCons x (Vec m x)

在我们的两个方程中，两边都有类 Nat。

现在对向量上的索引进行相同的翻译。

data InVec :: x -> Vec n x -> * where
Here :: InVec z (VCons z zs)
After :: InVec z ys -> InVec z (VCons y ys)

变成了

data InVec (a :: x) (as :: Vec n x)
= forall m z (zs :: Vec x m). (n ~ S m, as ~ VCons z zs) => Here
| forall m y z (ys :: Vec x m). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)

现在我们在 as :: Vec n x和 VCons z zs :: Vec (S m) x，其中两边在句法上有 不同的(但可以证明是相等的)类型 装备了这样一个概念！

还有什么缺失? 嗯，哈斯克尔大部分地区缺失的类型 你可以推广的术语语言只有变量 和非 GADT 构造函数，真的。一旦你有了这些，type family机器允许你编写类型级别的程序: 一些 这些函数可能与您考虑在 术语水平(例如，在 Nat中加入加法，这样就可以给出一个 很好的类型附加到 Vec) ，但这只是一个巧合！

在实践中，还缺少一样东西，那就是 图书馆 使用我们的新能力来索引类型的值 和 Monad在这个勇敢的新世界变得怎样? 我正在考虑这个问题，但是 还有很多事要做。

运行类型级程序

Haskell 和大多数依赖类型的编程语言一样，有两个 < em > 运行时系统的运行方式 程序(仅闭合表达式，类型擦除后，高度 优化) ，然后还有类型检查器运行程序的方式 (你的类型族，你的“类型类 Prolog”，带有打开的表达式) 因为执行的程序是不同的 依赖类型的语言有单独的运行时和 静态执行模型的 一样语言的程序，但不 令人担忧的是，运行时模型仍然允许您执行类型擦除，而且, 证明擦除: 这就是 Coq 的 提取机制给你的; 这至少是 Edwin Brady 的编译器所做的(尽管 Edwin 擦除不必要的重复值，以及类型和 阶段的区别可能不是 句法范畴句法范畴的区别 但它活得好好的。

依赖类型语言(即总计语言)允许类型检查器运行 程序免于任何比长时间等待更糟糕的恐惧 Haskell 变得更加依赖于类型，我们面临着什么的问题 它的静态执行模型应该是 将静态执行限制为总函数，这将允许我们 同样的奔跑自由，但可能迫使我们做出区分(至少 在数据和代码之间，因此我们可以告诉 是强制终止还是提高生产力。但这不是唯一的 我们可以自由地选择一个弱得多的执行模型，即 不愿意运行程序，代价是产生更少的方程 实际上，这就是 GHC 实际上 GHC 核心的打字规则没有提到 跑步 程序，但只用于检查证据的方程式。当 转换到核心，GHC 的约束求解器尝试运行类型级别的程序, 产生了一条银色的证据，证明给定的表达 等于它的正规形式。这种证据生成方法有点 不可预测且不可避免地不完整: 它害怕 例如，看起来很可怕的递归，这可能是明智的 我们不需要担心的是 IO的执行 类型检查器中的计算: 请记住，类型检查器不必给出 launchMissiles与运行时系统的含义相同！

亨德利-米尔纳文化

Hindley-Milner 型系统实现了真正可怕的巧合 四个明显的区别，与不幸的文化 副作用，许多人不能看到的区别 假设巧合是不可避免的! 我是什么 谈什么？

• 术语 对类型
• 显式写的东西 对隐式写的东西
• 在运行时 对的存在在运行时之前删除
• 非依赖性抽象 对依赖性定量

我们习惯于写术语，留下类型推断... 和 然后删除。我们习惯于量化类型变量 相应的类型抽象和应用程序正在悄无声息地发生 静止的。

你不需要离香草 Hindley-Milner 太远 在这些区别变得不一致之前，这就是 不是坏事。首先，如果我们愿意把它们分成几个类型，我们可以有更多有趣的类型 同时，我们不必在下列情况下编写类型类字典 我们使用重载函数，但是那些字典肯定是 在运行时呈现(或内联) 期望在运行时擦除的不仅仅是类型，但是(与类型一样) 类) ，某些隐式推断的值将不会是 被抹去了。例如，vReplicate的数值参数通常可以从所需向量的类型推断出来，但是我们仍然需要在运行时知道它。

我们应该检查哪种语言设计选择，因为 巧合不再成立? 例如，Haskell 提供的 无法显式实例化 forall x. t量词 打印检查器不能通过统一 t来猜测 x，我们没有其他办法 说出 x必须是什么。

更广泛地说，我们不能把“类型推理”当作一个单一的概念 我们要么一无所有，要么一无所有。首先，我们需要分头行动 关于“一般化”方面(米尔纳的“让”规则) ，这严重依赖于 限制哪些类型的存在，以确保一个愚蠢的机器可以 从“专业化”方面猜一个(米尔纳的“ var”规则) 它和你的约束求解器一样有效。我们可以期待 顶级类型将变得更难推断，但内部类型 信息仍然相当容易传播。

Haskell 的下一步

我们看到类型和种类的水平增长非常相似(和他们 已经在 GHC 中共享了一个内部代表) 合并他们。如果我们可以的话，采取 * :: *会很有趣: 我们输了 逻辑 很久以前，当我们允许底部，但 < em > 类型 健全通常是一个较弱的要求。我们必须检查。如果我们必须有 不同的类型、种类等水平，我们至少可以确保一切 在类型级别及以上的总是可以提升。这将是伟大的 只是为了重用类型的多态性，而不是 在种类级别重新发明多态性。

我们应该简化和概括目前的制约制度 允许 异质性方程 a ~ b其中 a和 b在语法上并不相同(但可以证明是相等的) 旧的技术(在我的论文，上个世纪) ，使依赖性很大 更容易处理。我们可以表达约束 表达式，从而放宽限制 升职了。

我们应该通过 引入依赖函数类型 pi x :: s -> t 这样的类型可以应用 明确地到任何类型的 s的表达式 生活在 十字路口的类型和术语语言(所以, 变量，构造函数，后面还有更多) Lambda 和 application 在运行时不会被擦除，所以我们会 会写字

vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z     x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)

不用 Natty取代 Nat。 pi的域可以是任意的 可提升的类型，因此如果可以提升 GADT，我们可以编写依赖 量词序列(或“望远镜”，de Briuijn 称之为它们)

pi n :: Nat -> pi xs :: Vec n x -> ...

我们需要多长就多长。

这些步骤的重点是通过直接使用更通用的工具来实现 消除复杂性，而不是使用弱工具和笨重的编码。目前的部分买入使得 Haskell 的依赖类型的好处比它们需要的更昂贵。

太难了？

依赖型的人让很多人紧张，他们让我紧张, 但我喜欢紧张，至少我发现很难不紧张 无论如何。但是这种无知的迷雾也无济于事 这其中有一部分是因为我们仍然 有很多东西需要学习。但是不那么激进的方法的支持者 众所周知，人们对依赖型人格的恐惧并不总是确定 事实摆在眼前。我不会说出名字的。这些“无法确定的类型检查”、“图灵不完整”、“没有阶段区分”、“没有类型消除”、“到处都是证据”等等，尽管它们是垃圾，但神话依然存在。

依赖类型的程序当然不必这样做 总是被证明是正确的。一个人可以改善自己的基本卫生 程序，在类型中强制执行附加的不变式，而不完全 在这个方向上的一些小步骤 往往导致更强有力的担保，而只有很少或根本没有额外的担保 证明义务。依赖类型的程序是不正确的 不可避免的 满了的证明，事实上，我通常采取的存在任何 证明在我的代码作为线索，以 质疑我的定义。

因为，就像任何发音能力的提高一样，我们可以自由地说脏话 新事物和公平。例如，有许多卑劣的方法 定义二进制搜索树，但这并不意味着不存在 好方法。重要的是不要假设糟糕的经历是不可能的 更好，即使它削弱了自我承认它。设计的依赖 定义是一种新的技能，需要学习，并成为一个 Haskell 程序员不会自动让你成为一个专家 程序是肮脏的，你为什么要剥夺别人公平的自由？

为什么还要和 Haskell 纠缠不清？

我真的很喜欢依赖类型，但我的大多数黑客项目是 - 还在哈斯克尔-为什么 Haskell 有一个可行的(尽管远非理想的)治疗方法 哈斯克尔拥有强大的工业实力 依赖类型语言还处于早期阶段 社区和基础设施的发展，但我们会实现这一目标的 在可能的情况下真正的代际转换，例如，通过 元编程和数据类型泛型 围绕着人们正在做什么，因为哈斯克尔的步骤 依赖型，看到有很多好处可以获得 也推动了当代语言的发展。

John，这是关于依赖类型的另一个常见误解: 当数据只在运行时可用时，依赖类型不起作用。下面是 getLine 示例的实现方法:

data Some :: (k -> *) -> * where
Like :: p x -> Some p


fromInt :: Int -> Some Natty
fromInt 0 = Like Zy
fromInt n = case fromInt (n - 1) of
Like n -> Like (Sy n)


withZeroes :: (forall n. Vec n Int -> IO a) -> IO a
withZeroes k = do
Like n <- fmap (fromInt . read) getLine
k (vReplicate n 0)


*Main> withZeroes print
5
VCons 0 (VCons 0 (VCons 0 (VCons 0 (VCons 0 VNil))))

编辑: 嗯，那应该是对养猪工人的回答的评论。我显然不及格。

Pigworker 对于为什么我们 应该会走向依赖类型给出了一个很好的讨论: (a)它们很棒; (b)它们实际上会 简化很多 Haskell 已经做过的事情。

至于“为什么不呢?”问题，有几点我认为。第一点是，虽然依赖类型背后的基本概念很简单(允许类型依赖于值) ，但是这个基本概念的分支是微妙而深刻的。例如，值和类型之间的区别仍然存在，但是讨论它们之间的区别比在 yer Hindley-Milner 或 System f 中变得更加微妙。在某种程度上，这是由于依赖类型从根本上来说是困难的(例如，一阶逻辑是不可判断的)。但是我认为更大的问题是我们缺乏一个好的词汇来捕捉和解释正在发生的事情。随着越来越多的人学习依赖类型，我们将发展出更好的词汇，因此事情将变得更容易理解，即使潜在的问题仍然很难。

第二点与 Haskell 是依赖类型的 在成长这一事实有关。因为我们正在朝着这个目标不断地进步，但是实际上并没有实现，我们只能停留在一种语言上，这种语言在增量补丁的基础上增量补丁。随着新思想的流行，同样的事情也发生在其他语言中。Java 过去没有(参数)多态性; 当他们最终添加它时，它显然是一个增量式的改进，带有一些抽象漏洞和功能受损。事实证明，混合使用子类型和多态性本身就很困难; 但这并不是 Java 泛型工作方式的原因。它们之所以这样工作，是因为约束是对旧版本 Java 的增量改进。同上，在 OOP 发明的那个年代，人们开始编写“ Objective”C (不要与 Objective-C 混淆)等等。请记住，C + + 一开始是以 C 的严格超集为幌子的。添加新的范例总是需要重新定义语言，否则就会导致一些复杂的混乱。我的观点是，向 Haskell 添加真正的依赖类型将需要一定量的内切和重新构造语言——如果我们要做得正确的话。但是要做出这样的改革真的很难，而我们正在取得的渐进式进展在短期内似乎更便宜。实际上，并没有多少人黑进 GHC，但仍有大量的遗留代码需要保留。这也是为什么会有这么多衍生语言的部分原因，比如 DDC、 Cayenne、 Idris 等等。