为什么不依赖键入？

Question

我看到几个消息来源反映了"Haskell逐渐成为一种依赖型语言"的观点.暗示似乎是随着越来越多的语言扩展,Haskell正朝着这个方向漂移,但还没有.

基本上我想知道两件事.首先,很简单,"作为一种依赖型语言"究竟意味着什么？(希望没有太过技术性.)

第二个问题是......有什么缺点？我的意思是,人们知道我们正朝着这个方向前进,所以必须有一些优势.然而,我们还没有,所以必须有一些下行阻止人们一路走下去.我的印象是问题是复杂性急剧增加.但是,并不是真正了解依赖打字是什么,我不确定.

我所知道的是,每次我开始阅读一种依赖类型的编程语言时,文本都是完全不可理解的......大概这就是问题所在.(？)

Answer 1

依赖类型的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)

因此,您有一个类型级别值与运行时值相关联:检查运行时副本会优化类型级别值的静态知识.尽管术语和类型是分开的,但我们可以通过使用单体结构作为一种环氧树脂,以相依类型的方式工作,从而在相之间产生结合.从允许类型中的任意运行时表达式开始,这还有很长的路要走,但事实并非如此.

讨厌的是什么？少了什么东西？

让我们对这项技术施加一些压力,看看什么开始摇摆不定.我们可能会认为单身人士应该更容易管理

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在哪里形成具有语法上不同(但可证明相等)的类型之间形成等式约束.GHC核心目前还没有这样的概念!

还缺少什么？好吧,大多数Haskell都缺少类型级别.你可以推广的术语语言只有变量和非GADT构造函数.一旦你有了这些,type family机器允许你编写类型级程序:其中一些可能非常类似于你会考虑在术语级别编写的函数(例如,配备Nat添加,所以你可以给出一个好的类型来追加Vec) ,但这只是巧合!

在实践中,缺少的另一个东西是一个库,它利用我们的新功能按值索引类型.在这个勇敢的新世界中有什么Functor 和Monad成为什么？我在考虑它,但还有很多工作要做.

运行类型级程序

与大多数依赖类型的编程语言一样,Haskell有两种 操作语义.运行时系统运行程序的方式(仅在关闭表达式,在类型擦除之后,高度优化)然后是类型检查程序运行程序的方式(您的类型系列,您的"类型类Prolog",使用打开的表达式).对于Haskell,您通常不会将两者混合起来,因为正在执行的程序使用不同的语言.依赖类型的语言具有针对相同语言的程序的单独的运行时和静态执行模型,但不用担心,运行时模型仍然允许您进行类型擦除,实际上是证据擦除:这就是Coq的提取机制给你; 这至少是Edwin Brady的编译器所做的事情(虽然Edwin删除了不必要的重复值,以及类型和证明).相位区别可能不再是句法范畴的区别 ,但它仍然存在并且很好.

依赖类型语言,总是允许类型检查程序运行程序,而不用担心比漫长的等待更糟糕的事情.随着Haskell变得更依赖于类型,我们面临的问题是它的静态执行模型应该是什么？一种方法可能是将静态执行限制为总函数,这将允许我们运行相同的自由,但可能迫使我们在数据和codata之间进行区分(至少对于类型级代码),以便我们可以判断是否强制终止或提高生产力.但这不是唯一的方法.我们可以自由选择一个更弱的执行模型,它不愿意运行程序,代价是通过计算得出更少的方程式.实际上,这就是GHC实际上做的事情.GHC核心的输入规则没有提及运行 程序,但仅用于检查方程式的证据.在转换为核心时,GHC的约束求解器会尝试运行您的类型级程序,从而生成一个银色的证据,表明给定的表达式等于其正常形式.这种证据生成方法有点不可预测,并且不可避免地是不完整的:例如,它与可怕的递归相抗衡,这可能是明智的.我们不需要担心的一件事是在类型检查器中执行IO 计算:请记住,类型检查器不必具有 launchMissiles与运行时系统相同的含义!

欣德利 - 米尔纳文化

Hindley-Milner型系统实现了四种截然不同的真正巧合,伴随着不幸的文化副作用,许多人无法看出区别之间的区别,并认为巧合是不可避免的!我在说什么？

• 术语与类型
• 明确写的东西vs隐式写的东西
• 出现在运行时VS擦除运行时间之前
• 非依赖抽象与依赖量化

我们习惯于编写术语并留下类型进行推断......然后删除.我们习惯于使用相应的类型抽象来量化类型变量,并且静默地和静态地发生应用程序.

在这些区别不对齐之前,你不必偏离香草的Hindley-Milner,这并不是坏事.首先,如果我们愿意在一些地方写它们,我们可以有更多有趣的类型.同时,当我们使用重载函数时,我们不必编写类型类字典,但这些字典在运行时肯定存在(或内联).在依赖类型的语言中,我们希望在运行时擦除的不仅仅是类型,而且(与类型类一样)一些隐式推断的值不会被擦除.例如,vReplicate数字参数通常可以从所需向量的类型中推断出来,但我们仍然需要在运行时知道它.

我们应该选择哪种语言设计选择,因为这些巧合不再适用？例如,Haskell没有提供forall x. t明确实例化量词的方法是正确的吗？如果类型x检查员无法通过统一来猜测t,我们没有其他方式可以说x必须是什么.

更广泛地说,我们不能将"类型推理"视为我们全部或全部都没有的整体概念.首先,我们需要拆分"泛化"方面(Milner的"let"规则),它严重依赖于限制哪些类型存在以确保愚蠢的机器可以从"专业化"方面猜测一个(Milner的"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)

无需更换Nat的Natty.域pi可以是任何可升级类型,因此如果GADT可以被提升,我们可以编写依赖的量词序列(或de Briuijn称之为"望远镜")

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

我们需要的长度.

这些步骤的重点是通过直接使用更通用的工具来消除复杂性,而不是使用弱工具和笨重的编码.目前的部分支持使得Haskell的各种依赖类型的好处比它们需要的更加昂贵.

太难？

依赖类型让很多人感到紧张.他们让我紧张,但我喜欢紧张,或者至少我觉得很难不紧张.但是,围绕这个话题存在着如此无知的迷雾并没有多大帮助.其中一些原因是我们仍然需要学习很多东西.但是,已经知道不太激进的方法的支持者会引起对依赖类型的恐惧而不总是确保事实完全与它们相关.我不会说出名字.这些"不可判断的类型检查","图灵不完整","无相位区分","无类型擦除","无处不在",等等,神话仍然存在,即使它们是垃圾.

肯定不是必须始终证明依赖类型的程序是正确的.人们可以改善一个程序的基本卫生,在类型中强制执行其他不变量,而不必一直到完整的规范.在这个方向上的小步骤通常会导致更强大的保证,很少或没有额外的证明义务.依赖类型的程序不可避免地充满了证据是不正确的,事实上我通常会在代码中出现任何证据作为质疑我的定义的提示.

因为,随着任何关节的增加,我们可以自由地说出新事物和公平.例如,有很多可靠的方法来定义二叉搜索树,但这并不意味着没有好方法.重要的是不要假设糟糕的经历不能被改善,即使它让自我厌恶承认它.依赖定义的设计是一项需要学习的新技能,而作为Haskell程序员并不能自动成为专家!即使某些节目是犯规的,为什么你会否认其他人的公平自由？

为什么还要打扰Haskell？

我非常喜欢依赖类型,但我的大多数黑客项目仍然在Haskell中.为什么？Haskell有类型类.Haskell有很多有用的库.Haskell有一个可行的(虽然远非理想)处理编程与效果.Haskell有一个工业强度编译器.依赖类型语言处于社区和基础设施发展的早期阶段,但我们将实现这一目标,尽可能通过元编程和数据类型泛型进行实际的代际转换.但是你必须环顾一下人们正在做什么,因为Haskell采取了依赖类型的步骤,看到通过推动当前一代语言向前发展可以获得很多好处.

Answer 2

依赖类型实际上只是值和类型级别的统一,因此您可以对类型的值进行参数化(已经可以使用Haskell中的类型类和参数多态),并且您可以在值上参数化类型(严格来说,不是可能在Haskell中) ,虽然DataKinds非常接近).

编辑: 显然,从现在开始,我错了(参见@ pigworker的评论).我将保留其余部分作为我被喂养的神话的记录.:P

从我所听到的,转向完全依赖类型的问题是,它将打破类型和值级别之间的阶段限制,允许将Haskell编译为具有已擦除类型的高效机器代码.使用我们当前的技术水平,依赖类型的语言必须在某个时刻(立即或在编译为依赖类型的字节码或类似之后)通过解释器.

这不一定是一个根本性的限制,但我个人并不知道目前在这方面看起来很有希望的研究,但尚未将其纳入GHC.如果其他人知道更多,我会很乐意纠正.

Answer 3

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答案的评论.我明显失败了.

Answer 4

pigworker对我们为什么要走向依赖类型进行了很好的讨论:(a)它们很棒; (b)它们实际上会简化 Haskell已经做的很多事情.

至于"为什么不呢？" 问题,我认为有几点.第一点是虽然依赖类型背后的基本概念很容易(允许类型依赖于值),但基本概念的分支既微妙又深刻.例如,价值观和类型之间的区别仍然存在并且很好; 但是讨论它们之间的差变得远小于在揭掉辛德雷更细致-米尔纳或系统F.在一定程度上,这是由于这样的事实,取决于类型是从根本上硬(例如,第一阶逻辑是不可判定).但我认为更大的问题是我们缺乏一个很好的词汇来捕捉和解释正在发生的事情.随着越来越多的人了解依赖类型,我们将开发出更好的词汇,因此即使潜在的问题仍然很难,事情也会变得更容易理解.

第二点与Haskell 向依赖类型增长的事实有关.因为我们正在逐步实现这一目标,但实际上没有实现这一目标,我们仍然坚持使用在增量补丁之上增加补丁的语言.随着新思想的流行,其他语言也发生了同样的事情.Java没有使用(参数)多态; 当他们最终添加它时,显然是一种渐进的改进,带有一些抽象泄漏和残缺的力量.事实证明,混合子类型和多态性本质上很难; 但这并不是Java Generics以他们的方式工作的原因.它们以他们的方式工作,因为约束是对旧版Java的增量改进.同上,在OOP发明的那一天,人们开始编写"客观"C(不要与Objective C混淆)等等,请记住,C++最初是以C的严格超集为幌子.添加新的范式总是需要重新定义语言,否则最终会出现一些复杂的混乱.我在所有这一点上的观点是,在Haskell中添加真正的依赖类型将需要一定量的内容和重组语言 - 如果我们要做正确的话.但实际上很难进行这种改革,而我们一直在进行的渐进式进展在短期内似乎更便宜.真的,没有那么多人攻击GHC,但是有很多遗留代码可以保持活力.这就是为什么有这么多衍生语言如DDC,Cayenne,Idris等的部分原因.