为什么不从属地input？
我已经看到了几个消息来源，认为“Haskell正逐渐成为一种依赖型语言”。 这意味着，随着越来越多的语言扩展，Haskell正朝着这个大方向漂移，但还没有到来。
基本上有两件事情我想知道。 第一，很简单，“作为一种依赖型语言”实际上是什么意思 ？ （希望不要过于技术性）
第二个问题是…缺点是什么？ 我的意思是，人们知道我们正在走这条路，所以一定有一些优势。 但是，我们还没到，所以肯定会有一些不利因素阻止人们一路走来。 我觉得问题是复杂性急剧增加。 但是，并不真正了解什么依赖types，我不知道。
我所知道的是，每当我开始阅读一个依赖types的编程语言，文本是完全不可理解的……可能是这个问题。 （？）
依赖types实际上只是值和types级别的统一，所以你可以参数化types的值（在Haskell中已经可以使用types类和参数多态），并且你可以在值上参数化types（不是严格地说，在Haskell中是可能的，尽pipeDataKinds非常接近）。
编辑：显然，从这一点来看，我错了（见@ pigworker的评论）。 我将保留其余的这个作为我已经喂养的神话的logging。 ：P
从我听说的转向完全依赖types的问题是，它将打破types和值级别之间的相位限制，允许Haskell编译为具有擦除types的高效机器代码。 在我们目前的技术水平下，一个依赖types的语言必须在某个时刻通过解释器（或者立即，或者在被编译为依赖types的字节码或类似的东西之后）。
这不一定是一个基本的限制，但我没有个人意识到任何目前在这方面看起来很有希望的研究，但尚未将其纳入GHC。 如果其他人知道更多，我会很乐意纠正。
依赖键入Haskell，现在？
Haskell在很小程度上是一种依赖types的语言。 有一种types级数据的概念，现在由于DataKinds而更加明智地input，并且有一些方法（ GADTs ）给运行时types的数据提供表示。 因此， 运行时间的东西的价值有效地显示在types中 ，这就意味着一种语言的依赖types。
简单的数据types被提升到种类级别，以便它们包含的值可以在types中使用。 因此，原型的例子
data Nat = Z | S Nat data Vec :: Nat -> * -> * where VNil :: Vec Z x VCons :: x -> Vec nx -> Vec (S n) x
成为可能，并与此同时，定义如
vApply :: Vec n (s -> t) -> Vec ns -> Vec nt vApply VNil VNil = VNil vApply (VCons f fs) (VCons s ss) = VCons (fs) (vApply fs ss)
这很好。 请注意，长度n在该函数中是纯静态的，确保input和输出向量具有相同的长度，即使该长度在执行vApply 。 相比之下，实现一个给定x n副本（这对vApply来说是pure ）是非常棘手的（即不可能）
vReplicate :: x -> Vec nx
因为知道在运行时要创build多less个副本是非常重要的。 input单身人士
data Natty :: Nat -> * where Zy :: Natty Z Sy :: Natty n -> Natty (S n)
对于任何可推广的types，我们可以build立单身家庭，索引在推广types上，运行时重复其值。 Natty n是types级n :: Nat的运行时副本的types。 我们现在可以写
vReplicate :: Natty n -> x -> Vec nx vReplicate Zy x = VNil vReplicate (Sy n) x = VCons x (vReplicate nx)
所以你有一个types级的值被赋值为一个运行时值：检查运行时拷贝提高了对types级值的静态知识。 尽pipe术语和types是分开的，但我们可以通过将单体结构作为一种环氧树脂以独立的方式进行工作，从而在各个阶段之间build立联系。 在types中允许任意运行时expression式还有很长的路要走，但这并不是什么。
什么是讨厌的？ less了什么东西？
让我们对这项技术施加一点压力，看看什么开始摇摆。 我们可能会得到这样的想法，即单件应该可以更隐含地pipe理
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
这是有效的，但现在意味着我们最初的Nattypes产生了三份：一种，一个单身家庭和一个单身类。 我们有一个相当笨重的过程来交换显式的Natty n值和Nattily n字典。 而且， Natty不是Nat ：我们对运行时间值有一定的依赖性，但不是我们首先想到的types。 没有完全依赖types的语言使依赖types变得复杂！
与此同时，虽然Nat能够得到提升，但Vec不能。 您不能通过索引types进行索引。 完全依赖types的语言没有这样的限制，在我作为一个依赖types的炫耀的职业生涯中，我学会了在我的演讲中包含两层索引的例子，教会那些做过单层索引的人很难 – 但可能不要指望我像一幢房子一样折叠起来。 有什么问题？ 平等。 当你给构造函数一个特定的返回types为明确的等式需求时，GADT通过翻译你实现的约束而工作。 喜欢这个。
data Vec (n :: Nat) (x :: *) = n ~ Z => VNil | forall m. n ~ S m => VCons x (Vec mx)
在我们两个方程的每一个中，双方都有亲切的Nat 。
现在尝试相同的翻译索引的向量。
data InVec :: x -> Vec nx -> * where Here :: InVec z (VCons z zs) After :: InVec z ys -> InVec z (VCons y ys)
变
data InVec (a :: x) (as :: Vec nx) = forall mz (zs :: Vec xm). (n ~ S m, as ~ VCons z zs) => Here | forall myz (ys :: Vec xm). (n ~ S m, as ~ VCons y ys) => After (InVec z ys)
现在我们在as :: Vec nx和VCons z zs :: Vec (S m) x之间形成了等式约束，其中双方在句法上有区别（但是可以相等）。 GHC核心目前尚未配备这样一个概念！
还有什么遗漏？ 那么， 大部分的Haskell在types层面上都是缺失的。 您可以推广的术语语言只有variables和非GADT构造函数。 一旦你有了这些， type family机制允许你编写types级的程序：其中一些可能就像你会考虑在任期内编写的函数（例如，添加Nat来添加Nat ，所以你可以给出一个好的types给追加Vec ），但这只是一个巧合！
在实践中缺less的另一件事是一个图书馆 ，它利用我们的新能力通过价值来索引types。 Functor和Monad在这个勇敢的新世界中成为了什么？ 我在想，但还有很多事情要做。
运行types级别的程序
和大多数依赖types的编程语言一样，Haskell有两个可操作的语义。 运行时系统运行程序的方式（只有closuresexpression式，types擦除后，高度优化），然后typechecker运行程序（您的types族，您的“类类Prolog”，具有打开的expression式）的方式。 对于Haskell，通常不会混淆两者，因为正在执行的程序使用不同的语言。 依赖types的语言对于相同的程序语言有不同的运行时和静态执行模型，但是不用担心，运行时模型仍然允许你进行types擦除，而且实际上certificate擦除：这就是Coq的提取机制给你的; 这至less是Edwin Brady的编译器所做的（尽pipeEdwin会删除不必要的重复值，以及types和certificate）。 阶段的区分可能不再是句法范畴的区分，而是活生生的。
完全依赖于types的语言，允许types检测程序运行程序，而不用担心比长时间等待更糟的事情。 当Haskell变得更加依赖types的时候，我们面临着它的静态执行模型应该是什么的问题？ 一种方法可能是将静态执行限制在全部函数中，这样可以让我们有相同的运行自由度，但是可能会迫使我们在数据和数据之间做出区分（至less是types级代码），以便我们可以判断强制终止或生产力。 但这不是唯一的方法。 我们可以自由地select一个非常弱的执行模式，这是不愿意运行程序的，而只是通过计算使得更less的方程式出来。 而实际上，这就是GHC实际做的。 GHC核心的input规则没有提到正在运行的程序，只是为了检查方程的证据。 在翻译成核心的时候，GHC的约束求解器试图运行你的types级程序，产生一个小小的silverlight证据，表明一个给定的expression式等于它的正常forms。 这种证据生成方法有点不可预知，并且不可避免地是不完整的：例如，它害怕看起来很恐怖的recursion，这可能是明智的。 我们不需要担心的一件事就是在types检查器中执行IO计算：请记住types检查器不必为launchMissiles与运行时系统相同的意义！
欣德利米尔纳文化
辛德勒 – 米尔纳式的体系实现了四个明显区别的真正巧合，不幸的文化副作用是许多人看不出区别之间的区别，并认为巧合是不可避免的！ 我在说什么？
- 条款与types
- 明确地写出了事物与隐含的事物
- 在运行时间之前进行擦除，而在运行之前进行擦除
- 非依赖性抽象vs依赖性量化
我们习惯于写出术语，并且推断出types，然后擦除。 我们用来量化typesvariables，相应的types抽象和应用程序静静地发生。
在这些区别出来之前，你不必离开香草Hindley-Milner太远，这不是什么坏事 。 首先，如果我们愿意在几个地方写出它们，我们可以有更多有趣的types。 同时，当我们使用重载的函数时，我们不必编写types类字典，但是这些字典在运行时肯定存在（或内联）。 在依赖types语言中，我们期望在运行时不仅仅擦除types，而且（像types类一样）隐藏推断的值不会被擦除。 例如， vReplicate的数字参数通常可以从所需vector的types中推导出来，但是我们仍然需要在运行时知道它。
我们应该审查哪些语言deviseselect，因为这些巧合不再成立？ 例如，Haskell没有办法实例化一个forall x. t 量词明确吗？ 如果typechecker不能通过统一t来猜测x ，我们没有别的办法来说明x必须是什么。
更广泛地说，我们不能把“types推断”看作是一个单一的概念。 首先，我们需要拆分“泛化”方面（米尔纳的“让”规则），它严重依赖于限制哪些types存在，以确保愚蠢的机器可以从“专业化”方面（米尔纳的“变种“规则），这是一样有效的约束求解。 我们可以预计，顶级types将变得更难推断，但内部types信息将仍然相当容易传播。
下一步为Haskell
我们看到types和种类水平变得非常相似（他们已经在GHC中共享一个内部表示）。 我们不妨将它们合并。 如果可以的话，采用* :: *会很有趣：我们很久以前就失去了逻辑完整性，当我们允许底部的时候，但是types的健全性通常是一个较弱的要求。 我们必须检查。 如果我们要有明显的types，种类等等级，至less可以确保types层面及以上的一切都能得到促进。 只重用我们已经有的types的多态性会很好，而不是重新在类的层次上重新发明多态。
我们应该通过允许a和btypes在句法上不相同（但可以certificate是相等的）的异构方程来简化和推广当前的约束系统。 这是一个古老的技术（在我的论文中，上个世纪），使依赖更容易应付。 我们可以在GADT中expression对expression式的约束，从而放松对可以提升的内容的限制。
我们应该通过引入依赖函数typespi x :: s -> t来消除对单例构造的需要。 具有这种types的函数可以被明确地应用于任何typessexpression式，这些expression式存在于types和术语语言的交集 （所以variables，构造函数，稍后会有更多）。 相应的lambda和应用程序在运行时不会被擦除，所以我们可以写
vReplicate :: pi n :: Nat -> x -> Vec nx vReplicate Z x = VNil vReplicate (S n) x = VCons x (vReplicate nx)
没有用Natty取代Nat 。 pi的领域可以是任何可推广的types，所以如果GADTs可以被推广，我们可以写出依赖的量词序列（或称为“Briuijn”称之为“望远镜”），
pi n :: Nat -> pi xs :: Vec nx -> ...
无论我们需要多长时间
这些步骤的重点是通过直接使用更通用的工具来消除复杂性 ，而不是使用弱工具和笨重的编码。 目前的部分买入让Haskell的依赖types的好处比他们需要的更昂贵。
太难？
依赖types使很多人紧张。 他们让我紧张，但我喜欢紧张，或者至less我觉得很难不紧张。 但是这个话题无知却有如此无知的雾气。 其中一些原因是我们都还有很多东西需要学习。 但是不那么激进的方法的支持者已经知道要煽动对依赖types的恐惧，而没有总是确定事实与他们完全一致。 我不会命名。 这些“不可判断的types检查”，“图灵不完全”，“不相区分”，“不删除types”，“certificate无处不在”等等，即使它们是垃圾，神话依然存在。
当然不是那种依赖types的程序总是被certificate是正确的。 一个人可以改善自己的程序的基本卫生，强化额外的不变式的types，而不是完全规范。 朝这个方向迈出的小步通常会导致强有力的保证，而几乎没有额外的certificate义务。 依赖types的程序不可避免地充满了证据，事实上，我通常在我的代码中存在任何证据作为质疑我的定义的线索。
因为任何口头上的增加，我们都可以自由地说新的事情，也是公平的。 例如，定义二叉search树有很多不好的方法 ，但这并不意味着没有一个好的方法 。 重要的是不要认为不好的经历不能被改善，即使它让自我承认它。 依赖定义的devise是一项需要学习的新技能，作为Haskell程序员不会自动让你成为专家！ 即使有些节目是犯规的，你为什么会否认别人有公平的自由呢？
为什么仍然打扰Haskell？
我真的很喜欢依赖types，但是我的大部分黑客项目仍然在Haskell中。 为什么？ Haskell有types类。 Haskell有有用的库。 Haskell有一个可行的（虽然远非理想）处理编程的效果。 Haskell有一个工业强度的编译器。 依赖types的语言在社区和基础设施发展方面处于较早的阶段，但是我们会到达那里，通过元编程和数据typesgenerics的方式实现真正的世代交替。 但是，由于Haskell的依赖types的步骤，你只需要看看人们正在做什么，看看通过推动现有的语言向前发展，还有很多好处。
约翰对于依赖types另一个常见的误解是：数据只在运行时才可用。 以下是您可以执行getLine示例的方法：
data Some :: (k -> *) -> * where Like :: px -> 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))))
编辑：嗯，这应该是一个评论小猪工的答案。 我显然在SO失败。
小猪工给出了一个很好的讨论，为什么我们应该走向依赖types：（一）他们真棒; （b）他们实际上会简化 Haskell已经做的很多事情。
至于“为什么不呢？” 问题，我想有几点。 第一点是，虽然依赖types背后的基本概念很容易（允许types依赖于价值），但是这个基本概念的影响既微妙又深刻。 例如，价值和types之间的区别依然存在， 但讨论它们之间的区别比在Hindley – Milner或者System F中要细致得多。在某种程度上，这是由于依赖types基本上是困难的（例如，一阶逻辑是不可判定的）。 但是我认为更大的问题是，我们缺乏一个好的词汇来捕捉和解释正在发生的事情。 随着越来越多的人学习依赖types，我们将开发更好的词汇，所以事情会变得更容易理解，即使潜在的问题仍然困难。
第二点与Haskell 正在向依赖types发展的事实有关。 因为我们正朝着这个目标迈进，但实际上并没有实现这个目标，所以我们一直坚持使用增量补丁的语言。 其他语言也出现了类似的情况，新的想法开始stream行起来。 Java没有使用（参数）多态; 而当他们最后join时，这显然是一个渐进的改进，有一些抽象的泄漏和权力的削弱。 原来，混合子types和多态性本质上是困难的; 但这不是Java Generics如何工作的原因。 他们按照他们的方式工作，因为这种限制是对旧版本Java的一种渐进式改进。 同样，在OOP发明的那一天，人们开始写“客观”C（不要与Objective C混淆）等等。记住，C ++是在C的严格超集的幌子下开始的。范式总是需要重新定义语言，否则就会结束一些复杂的混乱。 我的观点是，为Haskell增加真正的依赖types将需要一定量的内脏和重构语言 – 如果我们要做的正确。 但是这种改革真的很难，而在短期内我们所取得的进展似乎更加便宜。 真的，没有那么多人攻击GHC，但有很多遗留代码来保持活力。 这就是为什么有如DDC，卡宴，伊德里斯等许多剥离语言的原因的一部分
