Haskell for Dummies中的简单依赖类型示例.它们在Haskell的实践中如何有用？我为什么要关心依赖类型？

Question

我现在听到很多关于依赖类型的东西,我听说DataKinds与依赖类型有某种关系(但我不确定这个......只是在Haskell Meetup上听到过).

有人可以通过一个超级简单的Haskell示例说明依赖类型是什么,它有什么用？

在维基百科上写的是依赖类型可以帮助防止错误.你能举个简单的例子来说明Haskell中的依赖类型如何防止错误？

我现在可以在五分钟内开始使用的东西来防止我的Haskell代码中的错误？

依赖类型基本上是从值到类型的函数,如何在实践中使用它？为什么那么好？

Answer 1

迟到了,这个答案基本上是一个无耻的插件.

Sam Lindley和我写了一篇关于Hasochism的论文,这是Haskell中依赖类型编程的乐趣和痛苦.它提供了大量关于Haskell 现在可能的例子,并用Agda/Idris生成的依赖类型语言绘制了比较点(有利和有利).

虽然它是一篇学术论文,但它是关于实际的程序,你可以从Sam的回购中获取代码.我们有很多小例子(例如mergesort输出的有序性)但我们最终得到一个文本编辑器示例,我们使用宽度和高度索引来管理屏幕几何:我们确保组件是常规矩形(向量的向量,而不是衣衫褴褛的清单列表),它们完全吻合.

依赖类型的关键功能是保持单独数据组件之间的一致性(例如,矩阵中的头部向量和尾部中的每个向量必须具有相同的长度).这比写条件代码时更重要.这种情况(有一天会被视为天真可笑)是以下所有类型保留重写

• if b then t else e => if b then e else t
• if b then t else e => t
• if b then t else e => e

虽然我们可能正在进行测试,b因为它为我们提供了一些有用的洞察力,让我们了解下一步做什么是合适的(甚至是安全的),但是没有一种洞察力是通过类型系统来调解的:b真理证明t其e缺乏理由并且其虚假证明是错误的尽管很关键.

普通的老式Hindley-Milner确实为我们提供了一种确保一致性的方法.每当我们有多态函数时

f :: forall a. r[a] -> s[a] -> t[a]

我们必须a始终如一地实例化:但是第一个参数a必须修复,第二个参数必须发挥作用,并且我们在研究结果时会学到一些有用的结果.允许类型级别的数据是有用的,因为某些形式的一致性(例如,事物的长度)更容易用数据(数字)表示.

但真正的突破是GADT模式匹配,其中模式的类型可以细化它匹配的参数的类型.你有一个长度的矢量n; 你看是否是零或缺点; 现在你知道是否n为零.这是一种测试形式,其中每种情况下代码的类型比整体类型更具体,因为在每种情况下,已经学习的东西都反映在类型级别.它是通过测试来学习的,这种语言至少在一定程度上依赖于语言.

这是一个愚蠢的游戏,无论你使用什么类型的语言.用1替换类型表达式中的每个类型变量和每个基本类型,并以数字方式计算类型(求和,乘以产品,s -> t意味着t- 到 -s)看看你得到了什么:如果你得到0,你就是一个逻辑学家; 如果你得到1,你就是软件工程师; 如果你获得2的权力,你就是一名电子工程师; 如果你得到无限,你就是程序员.在这个游戏中发生的事情是粗略地尝试衡量我们正在管理的信息以及我们的代码必须做出的选择.我们通常的类型系统擅长管理编码的"软件工程"方面:拆包和插入组件.但是一旦做出选择,类型就无法观察它,并且只要有选择要做,类型就无法指导我们:非依赖类型系统接近所有值.给定类型相同.这是他们在防止bug方面的一个非常严重的限制.

Answer 2

常见示例是在列表的类型中对列表的长度进行编码，因此您可以执行类似（伪代码）的操作。

cons :: a -> List a n -> List a (n+1)

哪里n是整数。这样，您可以指定添加一个要列出的对象将其长度加一。

然后，您可以防止head（使您获得列表的第一个元素）在空列表上运行

 head :: n > 0 => List a n -> a

或做类似的事情

to3uple :: List a 3 -> (a,a,a)

这种方法的问题是，您head必须先证明该列表不为空，然后才能调用任意列表。

有时证明可以由编译器完成，例如：

 head (a `cons` l)

否则，您必须做类似的事情

 if null list
    then ...
    else (head list)

在这里调用是安全的head，因为您在else分支中，因此可以保证长度不为null。

但是，Haskell目前不执行依赖类型，所有给出的示例都不能很好地工作，但是您应该能够使用声明这种类型的列表，DataKind因为您可以将int类型提升为可以实例化的类型List a b。List Int 1。（b是采用文字的幻像类型）。

如果您对这种类型的安全性感兴趣，可以看看液体Haskell。

这是此类代码的示例

{-# LANGUAGE DataKinds, KindSignatures, TypeFamilies, TypeOperators #-}

import GHC.TypeLits


data List a (n:: Nat) = List [a] deriving Show

cons :: a -> List a n -> List a (n + 1)
cons x (List xs) = List (x:xs)

singleton :: a -> List a 1
singleton x = List [x]

data NonEmpty
data EmptyList

type family ListLength a where
  ListLength (List a 0) =  EmptyList
  ListLength (List a n) = NonEmpty

head' :: (ListLength (List a n) ~ NonEmpty) => List a n -> a
head' (List xs) = head xs

tail' :: (ListLength (List a n) ~ NonEmpty) => List a n -> List a (n-1)
tail' (List xs) = List (tail xs)

list = singleton "a"

head' list -- return "a"

尝试做head' (tail' list) 不会编译并付出

Couldn't match type ‘EmptyList’ with ‘NonEmpty’
Expected type: NonEmpty
  Actual type: ListLength (List [Char] 0)
In the expression: head' (tail' list)
In an equation for ‘it’: it = head' (tail' list)