为什么Haskell9.0的线性类型没有零，而Idris2有？

html5 • • 问答

从关于线性类型的 Idris 2 出版物“Idris 2：实践中的定量类型理论”：

对于 Idris 2，我们做出了一个具体的半环选择，其中多重性可以是以下之一：

  • 0：运行时不使用该变量
  • 1：变量在运行时只使用一次
  • ?：在运行时对变量的使用没有限制

但是对于Haskell：

该提案以 levity 多态性的方式引入了一种Multiplicity由类型检查器特别处理的数据类型，以表示多重性：

data Multiplicity
  = One    -- represents 1
  | Many   -- represents ?

他们为什么不加一个零？

回答

在 Idris 中，函数参数的值可以出现在返回类型中。您可能会编写一个带有类型的函数

vecLen : (n : Nat) -> Vect n a -> (m : Nat ** n = m)

这表示“vecLen是一个函数，它接受一个Nat（调用它n）和一个Vect长度n和元素类型a并返回一个Nat（调用它m）这样的函数n = m”。目的是遍历链表Vect并将其长度作为运行Nat时值。但问题是，vecLen需要你已经拥有的矢量作为运行值的长度，因为这是非常n我们正在谈论的说法！即可以实现只是

vecLen n _ = (n ** Refl) -- does no real work

你不能没有采取n作为参数，因为Vect类型需要它的长度作为参数才有意义。这是一个有点严重的问题，因为同时拥有n和Vect n a 重复的信息——在没有干预的情况下，“经典”Vect n a本身的定义实际上是空间二次方的n！所以我们需要一种方法来接受一个我们知道“原则上存在”但在运行时可能“实际上不存在”的参数。这就是零多重性的用途。

vecLen : (0 n : Nat) -> Vect n a -> (m : Nat ** n = m)
-- old definition invalid, you MUST iterate over the Vect to collect information on n (which is what we want!)
vecLen _ [] = (0 ** Refl)
vecLen _ (_ :: xs) with (vecLen _ xs)
    vecLen _ (_ :: xs) | (n ** Refl) = (S n ** Refl)

这是 Idris 中零多重性的用法：它让您可以谈论类型中可能不存在/不再存在/永远不存在的值，因此您可以对它们进行推理等（我相信 Edwin Brady 做过的一次谈话，他使用或至少注意到您可以使用零多重性来推断可变资源的先前状态。）

但是 Haskell 并没有这种依赖类型......所以没有零多重性的用例。从另一个角度来看， 的零重数形式f :: a -> b只是f :: forall (x :: a). b，因为 Haskell 以一种 Idris 和其他依赖类型语言无法轻易实现的方式进行了批量类型擦除。（从这个意义上说，IMO，我认为 Haskell 有整个依赖类型擦除问题，其他语言有这样的麻烦，巧妙地解决了 - 代价是必须对依赖类型的其他所有内容使用笨拙的编码！）

在后一种意义上，singletons采用依赖的、不受限制的参数的“依赖”Haskell（即加强了）方式是这样的：

--        vvvvvv +  vvvvvvvv duplicate information!
vecLen :: SNat n -> Vect n a -> SNat n
vecLen n _ = n -- allowed, ergh!

而“零多重性”版本只是

vecLen :: Vect n a -> SNat n
-- must walk Vect, cannot match on erased types like n
vecLen Nil = SZ
vecLen (_ `Cons` xs) = SS (goodLen xs)

  • @srghma 正如[在手册中](https://idris2.readthedocs.io/en/latest/tutorial/multiplicities.html) 所说，`Vect na -> (m : Nat ** n = m)` 什么都不是但是是`{0 n : Nat} -> {0 a : _} -> Vect na -> (m : Nat ** n = m)`的简写。*有些东西*必须引入`n`这个名字！它*被*用作值（即在类型中）的*描述*的一部分，而不是作为运行时值。
  • 是的。`{}` 和 `()` 之间的唯一区别在于解析/类型检查：`{}` 参数是隐式的。但他们*在那里*。在语言的基础理论中，我不确定“{}”是否存在。
以上是为什么Haskell9.0的线性类型没有零，而Idris2有？的全部内容。
THE END
分享
二维码
< <上一篇
下一篇>>