现在是依赖类型 Haskell 了吗？
Haskell 在某种程度上是一种依赖类型语言。有一个类型级数据的概念，现在可以更合理地键入，这要归功于DataKinds，并且有一些方法（GADTs) 给出运行时间
类型级数据的表示。因此，运行时内容的值有效地显示在类型中，这就是语言依赖类型的含义。
简单的数据类型是promoted到种类的水平，以便价值观
它们包含可用于类型。因此，典型的例子
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 to vApply's <*>)
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)
因此，您有一个与运行时值关联的类型级值：
检查运行时副本可以提炼静态知识
类型级别的值。即使术语和类型是分开的，我们也可以
通过使用单例结构以依赖类型的方式工作
一种环氧树脂，在相之间形成键合。那是一个
距离允许类型中的任意运行时表达式还有很长的路要走，但这并不是什么。
什么是令人讨厌的？少了什么东西？
让我们对这项技术施加一点压力，看看会发生什么
摇晃。我们可能会认为单身人士应该是易于管理的
更隐晦一点
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 is not 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)
becomes
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 and
VCons z zs :: Vec (S m) x两侧在语法上都有
不同的（但可证明是相等的）类型。 GHC 核心目前还没有
具备这样的概念！
还缺少什么？出色地，哈斯克尔的大部分类型中缺少
等级。您可以推广的术语语言只有变量
和非 GADT 构造函数，真的。一旦你拥有了这些，type family机器允许您编写类型级程序：一些
这些可能很像您会考虑在
术语级别（例如，装备Nat添加，所以你可以给
附加的好类型Vec），但这只是巧合！
在实践中，另一件缺失的事情是library这使得
使用我们的新功能按值索引类型。做什么Functor
and Monad成为这个勇敢的新世界？我正在考虑，但是
还有很多事情要做。
运行类型级程序
Haskell 与大多数依赖类型编程语言一样，two操作语义。这就是运行时系统的运行方式
程序（仅闭合表达式，类型擦除后，高度
优化）然后是类型检查器运行程序的方式
（您的类型系列，您的“类型类 Prolog”，带有开放表达式）。对于 Haskell，你通常不会混合
两者向上，因为正在执行的程序位于不同的位置
语言。依赖类型语言具有独立的运行时和
静态执行模型same程序语言，但不
担心，运行时模型仍然允许您进行类型擦除，而且事实上，
证明擦除：这就是 Coq 的萃取机制给你；
这至少是 Edwin Brady 的编译器所做的（尽管 Edwin Brady
删除不必要的重复值以及类型和
证明）。相位区别可能不是区别句法范畴不再存在了，但它还活着，而且活得很好。
完全依赖类型的语言允许类型检查器运行
程序无需担心任何比漫长等待更糟糕的事情。作为
Haskell 变得更加依赖类型，我们面临着什么问题
它的静态执行模型应该是？一种方法可能是
将静态执行限制为全部函数，这将允许我们
同样的跑步自由，但可能会迫使我们做出区分（至少
对于类型级代码）在 data 和 codata 之间，这样我们就可以知道
是否强制终止或生产力。但这不是唯一的
方法。我们可以自由选择一个更弱的执行模型，即
不愿意运行程序，代价是产生更少的方程
只需通过计算即可得出。事实上，这就是 GHC 的实际意义
做。 GHC 核心的类型规则没有提及running程序，但仅用于检查方程的证据。什么时候
转化为核心，GHC 的约束求解器尝试运行您的类型级程序，
生成一点银色的证据表明给定的表达式
等于其正常形式。这个证据生成方法有点
不可预测且不可避免地不完整：它回避
例如，看起来很可怕的递归，但这可能是明智的。一
我们不需要担心的是执行IO类型检查器中的计算：记住类型检查器不必给出launchMissiles与运行时系统的含义相同！
欣德利-米尔纳文化
Hindley-Milner 类型系统实现了真正令人敬畏的巧合
四个明显的区别，以及不幸的文化
副作用是很多人看不出两者之间的区别
区别和假设的巧合是不可避免的！我是什么
谈论什么？
- terms vs types
- 明确写下的东西vs隐含地写下的东西
- 运行时存在vs运行前擦除
- 非依赖抽象vs相关量化
我们习惯于编写术语并让类型进行推断......并且
然后删除。我们习惯于用以下方式量化类型变量
相应的类型抽象和应用程序默默地发生并且
静态地。
你不必偏离原版 Hindley-Milner 太远
在这些区别变得不协调之前，那就是没什么坏事。首先，如果我们愿意用少数语言编写它们，我们可以拥有更有趣的类型
地方。同时，我们不必编写类型类字典
我们使用重载函数，但那些字典肯定是
在运行时存在（或内联）。在依赖类型语言中，我们
期望在运行时擦除的不仅仅是类型，但是（与类型一样
类），一些隐式推断的值将不会被
删除了。例如。，vReplicate的数字参数通常可以从所需向量的类型推断出来，但我们仍然需要在运行时知道它。
我们应该审查哪些语言设计选择，因为这些
巧合不再成立？例如，Haskell 提供的是吗？
没有办法实例化一个forall x. t明确的量词？如果
类型检查器无法猜测x通过统一t，我们没有其他办法
说什么x必须是。
更广泛地说，我们不能将“类型推断”视为一个整体概念
我们要么拥有全部，要么一无所有。首先，我们需要拆分
脱离“概括”方面（米尔纳的“让”规则），这在很大程度上依赖于
限制存在哪些类型以确保愚蠢的机器可以
猜测之一，从“专业化”方面（米尔纳的“var”规则）
这与您的约束求解器一样有效。我们可以预期
顶级类型将变得更难推断，但内部类型
信息将仍然相当容易传播。
Haskell 的后续步骤
我们看到类型和种类级别变得非常相似（并且它们
已经在 GHC 中共享内部代表）。我们不妨
合并它们。采取起来会很有趣* :: *如果我们可以：我们输了logical很久以前，当我们允许底部时，稳健性，但是type健全性通常是较弱的要求。我们必须检查。如果我们必须有
不同的类型、种类等级别，我们至少可以确保一切
类型级别及以上级别始终可以升级。这会很棒
只是为了重用我们已经拥有的类型的多态性，而不是
在种类层面重新发明多态性。
我们应该简化和概括当前的约束系统
允许异质方程a ~ b其中的种类a and
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 by Natty。的域为pi可以是任何
promotable 类型，因此如果 GADT 可以提升，我们可以编写依赖
量词序列（或 de Briuijn 所说的“望远镜”）
pi n :: Nat -> pi xs :: Vec n x -> ...
到我们需要的任何长度。
这些步骤的要点是消除复杂性通过直接使用更通用的工具，而不是使用弱工具和笨重的编码。目前的部分支持使得 Haskell 的依赖类型的好处比他们需要的更加昂贵。
太难？
依赖型让很多人感到紧张。他们让我紧张，
但我喜欢紧张，或者至少我发现很难不紧张
反正。但无知的迷雾却无济于事
围绕主题。部分原因是我们仍然
有很多东西要学。但不太激进方法的支持者已经
众所周知，它会激起对依赖类型的恐惧，而不总是确保
事实完全支持他们。我不会指名道姓。这些“不可判定的类型检查”、“图灵不完备”、“没有阶段区分”、“没有类型擦除”、“到处都有证明”等等，神话仍然存在，尽管它们是垃圾。
依赖类型程序肯定不是必须的
总是被证明是正确的。人们可以改善自己的基本卫生状况
程序，在类型中强制执行额外的不变量，而无需全部
获得完整规范的方法。朝这个方向迈出一小步
通常会在很少或没有额外的情况下产生更强有力的保证
证明义务。依赖类型程序是不正确的
不可避免地full证明，事实上，我通常会采取任何
我的代码中的证明作为提示质疑我的定义.
因为，随着清晰度的提高，我们可以自由地说脏话
新事物也很公平。例如，有很多糟糕的方法
定义二叉搜索树，但这并不意味着没有一个好方法 https://stackoverflow.com/a/10659438/828361。重要的是不要认为糟糕的经历不可能是
更好，即使承认这一点会削弱自我。依赖的设计
定义是一项需要学习的新技能，并且成为 Haskell
程序员不会自动让你成为专家！而且即使有些
程序是犯规的，你为什么要剥夺别人公平的自由？
为什么还要为 Haskell 烦恼？
我真的很喜欢依赖类型，但我的大多数黑客项目都是
仍在哈斯克尔。为什么？ Haskell 有类型类。 Haskell 很有用
图书馆。 Haskell 有一个可行的（尽管远非理想）治疗方法
具有效果的编程。 Haskell拥有工业实力
编译器。依赖类型语言处于更早期的阶段
不断发展的社区和基础设施，但我们会实现这一目标
真正可能的代际转变，例如，通过
元编程和数据类型泛型。但你只需要看看
围绕哈斯克尔的步骤人们正在做什么
依赖类型看到有很多好处可以通过
也推动了当代语言的发展。
