为什么不独立输入？
我看到有几个消息来源反映了“Haskell正逐渐成为一种依赖型语言”的观点。 这意味着，随着越来越多的语言扩展，Haskell正在朝着这个大方向发展，但目前还没有。
基本上有两件事我想知道。 首先，很简单，“作为一种依赖型语言”究竟意味着什么？ （希望不要太过于技术性。）
第二个问题是......缺点是什么？ 我的意思是，人们知道我们正在走这条路，所以必须有一些优势。 然而，我们还没有到来，所以肯定会有一些不利因素阻止人们一路走下去。 我觉得问题是复杂性急剧增加。 但是，并不真正了解依赖类型是什么，我不知道。
我所知道的是，每次我开始阅读关于一种依赖型编程语言的时候，文本都是完全不可理解的......可能是这个问题。 （？）
依赖类型实际上只是值和类型级别的统一，所以你可以参数化类型的值（Haskell中已经可以使用类型类和参数多态），并且你可以参数化值的类型（不是严格来说，可能在Haskell中，尽管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在该函数中是纯静态的，确保输入和输出向量具有相同的长度，即使该长度在执行vApply 。 与此相反，它更棘手（即，不可能）来实现，这使得该函数n给定的副本x （这将是pure对vApply的<*>
vReplicate :: x -> Vec n x
因为知道在运行时要创建多少个副本是非常重要的。 输入单身人士。
data Natty :: Nat -> * where
Zy :: Natty Z
Sy :: Natty n -> Natty (S n)
对于任何可升级的类型，我们都可以构建单身家族，按照推广类型进行索引，并由运行时重复其值。 Natty n是类型级n :: Nat的运行时副本的类型。 我们现在可以写
vReplicate :: Natty n -> x -> Vec n x
vReplicate Zy x = VNil
vReplicate (Sy n) x = VCons x (vReplicate n x)
所以你有一个类型级的值被赋值为运行时值：检查运行时拷贝提高了对类型级值的静态知识。 尽管术语和类型是分开的，但我们可以通过使用单体结构作为一种环氧树脂，从而以相关类型的方式进行工作，从而在各阶段之间建立联系。 在允许类型中的任意运行时表达式方面还有很长的路要走，但这并不是什么。
什么是讨厌的？ 少了什么东西？
让我们对这项技术施加一点压力，看看什么开始发生摇摆。 我们可能会认为singletons应该可以更隐含地管理
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 ：我们对运行Natty有一定的依赖性，但不是我们首先想到的类型。 没有完全依赖类型的语言使依赖类型变得复杂！
与此同时，尽管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 nx和VCons z zs :: Vec (S m) x之间形成等式约束，其中双方在句法上有区别（但可证明是相等的）种类。 GHC核心目前尚未配备这种概念！
还有什么遗漏？ 那么， 大部分Haskell在类型级别上都是缺失的。 您可以推广的术语语言实际上只有变量和非GADT构造函数。 一旦你有了这些， type family机制允许你编写类型级别的程序：其中一些可能非常类似于你在术语级别编写的函数（例如，为Nat增加了一个加法，所以你可以给出一个好的类型给追加Vec ），但这只是一个巧合！
在实践中缺失的另一件事是一个图书馆，它利用我们的新能力，通过价值来索引类型。 Functor和Monad在这个勇敢的新世界中成为了什么？ 我在想，但还有很多事情要做。
运行Type-Level程序
Haskell和大多数依赖类型的编程语言一样，有两个可操作的语义。 运行时系统运行程序的方式（仅限于关闭表达式，类型擦除后，高度优化），然后typechecker运行程序（您的类型族，您的“类类Prolog”，带有开放表达式）的方式。 对于Haskell来说，你通常不会混淆两者，因为正在执行的程序使用不同的语言。 依赖类型的语言对于相同的程序语言具有不同的运行时和静态执行模型，但不用担心，运行时模型仍然允许您进行类型擦除和实际上的证明擦除：这就是Coq的提取机制为您提供的; 这至少是Edwin Brady的编译器所做的（尽管Edwin会删除不必要的重复值，以及类型和证明）。 阶段的区别可能不再是句法范畴的区别，但它仍然活着，而且很好。
完全依赖于类型的语言，允许类型检测程序运行程序，不用担心任何比长时间等待更糟的事情。 随着Haskell变得更加依赖类型，我们面临着它的静态执行模型应该是什么的问题？ 一种方法可能是将静态执行限制为全部函数，这会使我们有相同的运行自由度，但可能会迫使我们在数据和数据之间做出区分（至少对于类型级代码），以便我们可以判断是否强制终止或生产力。 但这不是唯一的方法。 我们可以自由选择一个更弱的执行模型，它不愿意运行程序，只需要通过计算使得更少的方程式出来。 实际上，这正是GHC实际所做的。 GHC核心的输入规则没有提到正在运行的程序，而只是用于检查方程式的证据。 在翻译成核心时，GHC的约束求解器试图运行你的类型级程序，产生一个小小的银色痕迹，证明给定表达式等于它的正常形式。 这种证据生成方法有点不可预测，并且不可避免地是不完整的：例如，它可怕地看到可怕的递归，这可能是明智的。 我们不需要担心的一件事是在类型检查器中执行IO计算：请记住类型检查器不必为launchMissiles与运行时系统相同的意义！
欣德利米尔纳文化
欣德利 - 米尔纳式系统实现了四种不同区别的真正巧合，其中不幸的文化副作用是许多人无法区分区别并认为巧合是不可避免的！ 我在说什么？
我们习惯于写出术语并且推断出类型，然后擦除。 我们习惯于通过相应的类型抽象和应用程序来静态地静态地进行类型变量的量化。
在这些区别出来之前，你不必离开香草Hindley-Milner太远，这并不是什么坏事。 首先，如果我们愿意在几个地方写出它们，我们可以有更多有趣的类型。 同时，当我们使用重载函数时，我们不必编写类型类字典，但是这些字典在运行时肯定存在（或内联）。 在依赖类型语言中，我们期望在运行时不仅仅擦除类型，而且（如类型类）那样，一些隐式推断的值不会被擦除。 例如， vReplicate的数字参数通常可以从所需向量的类型中推导出来，但我们仍然需要在运行时了解它。
我们应该审查哪些语言设计选择，因为这些巧合不再成立？ 例如，Haskell没有办法实例化一个forall x. t forall x. t量词明确？ 如果类型检查者不能通过统一t来猜测x ，我们没有其他方法可以说出x必须是什么。
更广泛地说，我们不能把“类型推断”看作是一个单一的概念，我们可以全部或者不包含任何的概念。 首先，我们需要分解“泛化”方面（米尔纳的“让”规则），它严重依赖于限制哪些类型存在，以确保愚蠢的机器可以从“专业化”方面猜测一个（Milner's“var “规则），它与你的约束求解器一样有效。 我们可以预计，顶级类型将变得更难推断，但内部类型信息仍然相当容易传播。
下一步为Haskell
我们看到类型和种类水平变得非常相似（他们已经在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)
无需用Natty替换Nat 。 pi的领域可以是任何可推广的类型，所以如果GADTs可以被提升，我们可以写出相关的量词序列（或称为de Briuijn称之为“望远镜”），
pi n :: Nat -> pi xs :: Vec n x -> ...
无论我们需要多长时间。
这些步骤的重点是通过直接使用更通用的工具来消除复杂性，而不是使用弱工具和笨重的编码。 目前的部分买入让Haskell的依赖类型的好处比他们需要的更昂贵。
太难？
依赖类型会让很多人紧张。 他们让我感到紧张，但我喜欢紧张，或者至少我觉得很难不紧张。 但这并不能说明这个话题中有这么一个无知的雾。 其中一些原因是我们都还有很多东西需要学习。 但是已经知道不那么激进的方法的支持者会鼓励对依赖类型的恐惧，但并不总是确保事实与他们完全一致。 我不会命名。 这些“不可判定的类型检查”，“图灵不完整”，“没有相位区分”，“无类型擦除”，“无处不在”等等，即使它们是垃圾，神话依然存在。
当然不是那种依赖类型的程序必须始终被证明是正确的。 人们可以改善自己的程序的基本卫生习惯，在类型中强制执行额外的不变量，而不需要完整的规范。 朝这个方向迈出的小步通常会导致强有力的保证，而很少或没有额外的证明义务。 依赖类型的程序不可避免地充满了证据，事实上，我通常会在我的代码中出现任何证据作为质疑我的定义的线索。
因为任何口头禅的增加，我们都可以自由地说出肮脏的新事物和公平的事物。 例如，定义二叉搜索树有很多不好的方法，但这并不意味着没有好方法。 重要的是不要认为不好的经历不能被改善，即使它让自我承认它。 依赖定义的设计是一项需要学习的新技能，作为Haskell程序员不会自动让你成为专家！ 即使有些节目是犯规的，你为什么会否认其他人有公平的自由？
为什么仍然打扰Haskell？
我真的很喜欢依赖类型，但我的大多数黑客项目仍然在Haskell中。 为什么？ Haskell有类型类。 Haskell有有用的库。 Haskell对效果的编程有一个可行的（虽然远非理想）处理。 Haskell拥有一个工业强度的编译器。 依赖类型语言在社区和基础设施的发展中处于早期阶段，但是我们会到达那里，通过元编程和数据类型泛型的方式实现真正的世代交替。 但是，由于Haskell采用依赖类型的步骤，您只需要查看人们在做什么，就可以看到通过向前推进当前语言的方式获得很多好处。
约翰对于依赖类型的另一个常见误解是：当数据仅在运行时可用时，它们不起作用。 以下是如何执行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的答案的评论。 我显然在SO失败。
链接地址: http://www.djcxy.com/p/80855.html