我看到一些消息来源回应了“Haskell 正在逐渐成为一种依赖类型的语言”的观点。这似乎意味着随着越来越多的语言扩展，Haskell 正在朝着这个大方向发展，但还没有。
基本上有两件事我想知道。首先，很简单，“作为一种依赖类型的语言”实际上是什么意思？（希望不要太技术化。）
第二个问题是……缺点是什么？我的意思是，人们知道我们正朝着那个方向前进，所以它一定有一些优势。然而，我们还没有到那里，所以一定有一些不利因素阻止人们一路前进。我的印象是，问题是复杂性急剧增加。但是，我不确定什么是依赖类型，我不确定。
我所知道的是，每次我开始阅读有关依赖类型编程语言的内容时，文本都是完全难以理解的......大概就是这个问题。（？）
Haskell 在某种程度上是一种依赖类型的语言。有一个类型级数据的概念，由于 ，现在可以更明智地进行类型化DataKinds，并且有一些方法 ( GADTs) 可以为类型级数据提供运行时表示。因此，运行时内容的值有效地显示在 types中，这就是依赖类型语言的含义。
简单数据类型被提升到种类级别，以便它们包含的值可以在类型中使用。因此，原型示例
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在该函数中是纯静态的，确保输入和输出向量具有相同的长度，即使该长度在
vApply. 相比之下，实现n复制给定x（将是pureto vApply's <*>）的函数要复杂得多（即，不可能）
vReplicate :: x -> Vec n x
因为知道在运行时要制作多少份副本至关重要。输入单例。
data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
对于任何可提升的类型，我们都可以构建单例族，在提升的类型上建立索引，并由其值的运行时副本占据。Natty n是 type-level 的运行时副本的类型n
:: Nat。我们现在可以写
vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)
因此，您有一个与运行时值挂钩的类型级值：检查运行时副本可以提炼类型级值的静态知识。即使术语和类型是分开的，我们也可以通过使用单态结构作为一种环氧树脂以依赖类型的方式工作，从而在相之间建立键。这距离在类型中允许任意运行时表达式还有很长的路要走，但它不是什么都没有。
让我们对这项技术施加一点压力，看看是什么开始摇摆不定。我们可能会认为单例应该更隐含地易于管理
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)
在我们的两个方程中，两边都有 kind 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) xGHC核心目前还没有配备这样的概念！
还缺少什么？好吧，大多数 Haskell都从类型级别中丢失了。您可以推广的术语语言实际上只有变量和非 GADT 构造函数。一旦你有了这些，type family机器就允许你编写类型级别的程序：其中一些可能很像你会考虑在术语级别编写的函数（例如，配备Nat加法，所以你可以给出一个好的类型来 append for Vec） ，但这只是巧合！
在实践中缺少的另一件事是利用我们的新能力按值索引类型的库。在这个勇敢的新世界里做什么Functor
和成为什么？Monad我正在考虑，但还有很多事情要做。
与大多数依赖类型的编程语言一样，Haskell 有两种 操作语义。运行时系统运行程序的方式是（仅封闭表达式，类型擦除后，高度优化），然后是类型检查器运行程序的方式（您的类型系列，您的“类型类 Prolog”，带有开放表达式）。对于 Haskell，您通常不会将两者混为一谈，因为正在执行的程序使用不同的语言。依赖类型的语言对于相同的程序语言有单独的运行时和静态执行模型，但不用担心，运行时模型仍然允许你进行类型擦除，实际上，证明擦除：这就是 Coq 的提取机制给你；这至少是 Edwin Brady 的编译器所做的（尽管 Edwin 删除了不必要的重复值以及类型和证明）。相位区分可能不再是句法类别的区分 ，但它仍然存在并且很好。
完全依赖类型的语言允许类型检查器运行程序，而不必担心比长时间等待更糟糕的事情。随着 Haskell 变得更加依赖类型，我们面临的问题是它的静态执行模型应该是什么？一种方法可能是将静态执行限制为全部函数，这将允许我们同样自由地运行，但可能会迫使我们在数据和余数据之间做出区分（至少对于类型级代码），以便我们可以判断是否强制终止或生产力。但这不是唯一的方法。我们可以自由选择一个更弱的执行模型，它不愿意运行程序，代价是仅仅通过计算得出的方程更少。实际上，这就是 GHC 实际所做的。GHC核心的打字规则没有提到运行
程序，但仅用于检查方程式的证据。当转换到核心时，GHC 的约束求解器会尝试运行您的类型级程序，生成一些银色的证据，证明给定表达式等于其正常形式。这种证据生成方法有点不可预测，而且不可避免地不完整：例如，它避免了看起来很可怕的递归，这可能是明智的。我们不需要担心的一件事是在类型检查器中执行IO
计算：请记住，类型检查器不必给出
launchMissiles与运行时系统相同的含义！
Hindley-Milner 类型系统实现了四个不同区别的真正令人敬畏的巧合，但不幸的是，许多人无法看到区别之间的区别并认为巧合是不可避免的！我在说什么？
我们习惯于编写术语并让类型被推断......然后被删除。我们习惯于用相应的类型抽象和应用程序以静默和静态的方式对类型变量进行量化。
在这些区别不一致之前，您不必偏离原版的 Hindley-Milner 太远，这不是坏事。首先，如果我们愿意在几个地方编写它们，我们可以有更多有趣的类型。同时，当我们使用重载函数时，我们不必编写类型类字典，但这些字典在运行时肯定存在（或内联）。在依赖类型语言中，我们期望在运行时擦除的不仅仅是类型，而且（与类型类一样）一些隐式推断的值不会被擦除。例如，vReplicate的数字参数通常可以从所需向量的类型推断出来，但我们仍然需要在运行时知道它。
我们应该审查哪些语言设计选择，因为这些巧合不再成立？例如，Haskell 没有提供forall x. t显式实例化量词的方法是否正确？如果类型检查器无法x通过 unifiying 进行猜测t，我们就没有其他方法可以说明x必须是什么。
更广泛地说，我们不能将“类型推断”视为我们拥有或一无所有的单一概念。首先，我们需要将“泛化”方面（米尔纳的“让”规则）从“专业化”方面（米尔纳的“var " 规则），它与您的约束求解器一样有效。我们可以预期顶级类型将变得更难推断，但内部类型信息将仍然相当容易传播。
我们看到类型和种类级别变得非常相似（并且它们已经在 GHC 中共享内部表示）。我们不妨合并它们。如果可以的话，这会很有趣* :: *：我们
很久以前就失去了逻辑稳健性，当时我们允许底部，但类型
稳健性通常是一个较弱的要求。我们必须检查。如果我们必须有不同的类型、种类等级别，我们至少可以确保类型级别及以上的所有内容都可以随时提升。重用我们已经对类型拥有的多态性，而不是在种类级别重新发明多态性，那就太好了。
我们应该通过允许异构方程来简化和概括当前的约束系统，a ~ b其中a和
b在句法上不相同（但可以证明是相等的）。这是一种古老的技术（在我的论文中，上个世纪），它使依赖性更容易应对。我们将能够在 GADT 中表达对表达式的约束，从而放宽对可推广内容的限制。
我们应该通过引入依赖函数类型来消除对单例构造的需要，pi x :: s -> t. 具有这种类型的函数可以显式应用于任何类型的表达式，s这些表达式存在于类型语言和术语语言的交集中（因此，变量、构造函数，稍后还会有更多）。相应的 lambda 和应用程序不会在运行时被擦除，因此我们可以编写
vReplicate :: pi n :: Nat -> x -> Vec n x
vReplicate Z x = VNil
vReplicate (S n) x = VCons x (vReplicate n x)
无需替换Nat为Natty. 的域pi可以是任何可推广的类型，因此如果可以推广 GADT，我们可以编写相关的量词序列（或 de Briuijn 所说的“望远镜”）
pi n :: Nat -> pi xs :: Vec n x -> ...
到我们需要的任何长度。
这些步骤的重点是通过直接使用更通用的工具来消除复杂性，而不是使用弱工具和笨重的编码。当前的部分购买使得 Haskell 的依赖类型的好处比它们需要的更昂贵。
依赖类型让很多人感到紧张。它们让我紧张，但我喜欢紧张，或者至少我发现无论如何都很难不紧张。但这无助于围绕该主题的无知迷雾。其中一些是因为我们还有很多东西要学。但众所周知，不那么激进的方法的支持者会激起对依赖类型的恐惧，但并不总是确保事实与他们完全一致。我不会点名。这些“无法确定的类型检查”、“图灵不完整”、“没有相位区分”、“没有类型擦除”、“到处都有证明”等等，这些神话仍然存在，即使它们是垃圾。
当然，依赖类型程序不一定总是被证明是正确的。可以改善程序的基本卫生，在类型中强制执行额外的不变量，而无需一路达到完整的规范。朝这个方向迈出的小步通常会导致更强有力的保证，而很少或没有额外的证明义务。依赖类型的程序不可避免地充满了证明，这是不正确的，事实上，我通常将代码中存在的任何证明作为质疑我的定义的线索。
因为，随着清晰度的任何增加，我们可以自由地说出肮脏的新事物以及公平的事物。例如，定义二叉搜索树的方法有很多，但这并不意味着没有好的方法。重要的是不要认为糟糕的经历是无法改善的，即使它会削弱自我承认这一点。依赖定义的设计是一项需要学习的新技能，成为 Haskell 程序员并不会自动使您成为专家！即使有些程序是犯规的，你为什么要剥夺其他人公平的自由？
我真的很喜欢依赖类型，但我的大部分黑客项目仍然在 Haskell 中。为什么？Haskell 有类型类。Haskell 有有用的库。Haskell 对带有效果的编程有一个可行的（尽管远非理想）处理。Haskell 有一个工业级的编译器。依赖类型语言在社区和基础设施的发展中处于更早的阶段，但我们将通过元编程和数据类型泛型等方式实现真正的代际转变。但是你只需要看看人们在 Haskell 向依赖类型迈出的步伐所做的事情，就会发现推动当代语言向前发展也会带来很多好处。
依赖类型实际上只是值和类型级别的统一，因此您可以对类型的值进行参数化（在 Haskell 中已经可以使用类型类和参数多态性）并且您可以对值的类型进行参数化（严格来说，在 Haskell 中尚不可能） ，虽然DataKinds非常接近）。
编辑： 显然，从现在开始，我错了（参见@pigworker 的评论）。我将保留其余部分作为我被灌输的神话的记录。:P
据我所知，转向完全依赖类型的问题在于，它会打破类型和值级别之间的相位限制，从而允许将 Haskell 编译为具有擦除类型的高效机器代码。以我们目前的技术水平，依赖类型的语言必须在某个时候通过解释器（立即，或者在编译为依赖类型的字节码或类似的之后）。
这不一定是基本限制，但我个人并不知道当前有任何在这方面看起来很有希望但尚未进入 GHC 的研究。如果其他人知道更多，我很乐意得到纠正。
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 已经做的很多事情。
至于“为什么不？” 问题，我认为有几点。第一点是，虽然依赖类型背后的基本概念很简单（允许类型依赖于值），但该基本概念的影响既微妙又深刻。例如，值和类型之间的区别仍然存在并且很好；但是讨论它们之间的区别变得很遥远比你的 Hindley —— Milner 或 System F 更细微。在某种程度上，这是由于依赖类型从根本上来说是困难的（例如，一阶逻辑是不可判定的）。但我认为更大的问题实际上是我们缺乏一个很好的词汇来捕捉和解释正在发生的事情。随着越来越多的人了解依赖类型，我们将开发出更好的词汇表，因此事情会变得更容易理解，即使潜在的问题仍然很困难。
第二点与 Haskell 正在增长的事实有关朝向依赖类型。因为我们正在朝着这个目标逐步取得进展，但实际上并没有做到这一点，所以我们被困在一种在增量补丁之上具有增量补丁的语言。随着新思想的流行，其他语言也发生了同样的事情。Java 过去没有（参数）多态性。当他们最终添加它时，这显然是一个渐进式的改进，带有一些抽象漏洞和削弱的能力。事实证明，混合子类型和多态本质上是困难的。但这不是 Java 泛型以它们的方式工作的原因。由于限制是对旧版本的 Java 进行增量改进，因此它们以它们的方式工作。同上，早在 OOP 被发明并且人们开始编写“目标”的那一天 C（不要与 Objective-C 混淆）等等。请记住，C++ 是在作为 C 的严格超集的幌子下开始的。添加新的范例总是需要重新定义语言，否则会导致一些复杂的混乱。我的观点是，将真正的依赖类型添加到 Haskell 将需要一定量的内脏和重组语言——如果我们要做得对的话。但要进行这种彻底的改革真的很难，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。C++ 以作为 C 的严格超集的幌子开始。添加新的范例总是需要重新定义语言，否则会导致一些复杂的混乱。我的观点是，将真正的依赖类型添加到 Haskell 将需要一定量的内脏和重组语言——如果我们要做得对的话。但要进行这种彻底的改革真的很难，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。C++ 以作为 C 的严格超集的幌子开始。添加新的范例总是需要重新定义语言，否则会导致一些复杂的混乱。我的观点是，将真正的依赖类型添加到 Haskell 将需要一定量的内脏和重组语言——如果我们要做得对的话。但要进行这种彻底的改革真的很难，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。否则会导致一些复杂的混乱。我的观点是，将真正的依赖类型添加到 Haskell 将需要一定量的内脏和重组语言——如果我们要做得对的话。但要进行这种彻底的改革真的很难，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。否则会导致一些复杂的混乱。我的观点是，将真正的依赖类型添加到 Haskell 将需要一定量的内脏和重组语言——如果我们要做得对的话。但要进行这种彻底的改革真的很难，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。真的很难承诺进行这种大修，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。真的很难承诺进行这种大修，而我们一直在取得的渐进式进展在短期内似乎更便宜。确实，攻击 GHC 的人并不多，但仍有大量遗留代码需要保持活力。这就是为什么有这么多衍生语言（如 DDC、Cayenne、Idris 等）的部分原因。