haskell - 为什么 Haskell 9.0 的线性类型没有零，而 Idris 2 有？

Question

来自 Idris 2 关于线性类型的出版物 "Idris 2: Quantitative Type Theory in Practice" :

For Idris 2, we make a concrete choice of semiring, where a multiplicity can be one of:

• 0: the variable is not used at run time
• 1: the variable is used exactly once at run time
• ω: no restrictions on the variable’s usage at run time

但是对于 Haskell :

In the fashion of levity polymorphism, the proposal introduces a data type Multiplicity which is treated specially by the type checker, to represent the multiplicities:

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

他们为什么不加一个零？

Answer 1

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

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

这表示“vecLen 是一个函数，它接受 Nat (称为 n )和 Vect 的长度 n 和元素类型 a 并返回 Nat (称为 m ) 使得 n = m"。意图是遍历链表Vect并将其长度作为运行时Nat值(value)。但问题是 vecLen要求您已经将向量的长度作为运行时值，因为这正是 n我们正在谈论的论点! IE。可以实现

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

你不能不带n作为一个论点，因为 Vect type 需要它的长度作为参数才有意义。这是一个有点严重的问题，因为同时拥有 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 具有其他语言无法巧妙解决的整个依赖类型删除问题 - 代价是必须对依赖类型的其他所有内容使用笨拙的编码!)
在后一种意义上，“依赖”Haskell(即用 singletons 加强)采用依赖的、不受限制的参数的方式是这样的:

--        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)