为什么 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 中，函数参数的值可以出现在 return 类型中。你可以写一个类型为

的函数

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

这表示“vecLen 是一个接受 Nat（称之为 n）和长度 n 和元素类型的 Vect 的函数a 和 return 是一个 Nat（称之为 m）使得 n = m”。目的是遍历链表 Vect 并得出其长度作为运行时 Nat 值。但问题是 vecLen 要求您已经 将向量的长度 作为运行时值，因为这正是我们正在讨论的 n 论点！ IE。可以实现只是

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

你不能不将n作为参数，因为Vect类型需要它的长度作为有意义的参数。这是一个有点严重的问题，因为 n 和 Vect n a 重复信息——没有干预 Vect n a 本身的“经典”定义是事实上 space-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 中零多重性的用途：它让您可以讨论类型内部可能不存在的值 yet/anymore/ever，这样您就可以对它们进行推理等。（我相信 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)

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

Why does Haskell 9.0 not have Zero in its linear types, but Idris 2 does?

haskell

types

linear-types

idris