多重性
Idris 2 是基于 量化类型理论（QTT） ，这是由 Bob Atkey 和 Conor McBride 开发的核心语言。在实践中，Idris 2 中的每个变量都有一个 数量 与之相关。数量是的取值是下列其中之一：
0，表示变量在运行时被 擦除1，表示变量在运行时 正好使用一次不受限制 ，这与 Idris 1 的行为相同
我们可以通过检查孔看到变量的多重性。例如，如果我们有以下关于向量的 append 的骨架定义...
append : Vect n a -> Vect m a -> Vect (n + m) a
append xs ys = ?append_rhs
...我们可以看一下 append_rhs 这个孔：
Main> :t append_rhs
0 m : Nat
0 a : Type
0 n : Nat
ys : Vect m a
xs : Vect n a
-------------------------------------
append_rhs : Vect (plus n m) a
0 旁边的 m, a 和 n 表示它们在范作用域内，但在运行时将会出现 0 次，也就是说，将会 保证 它们在运行时会被删除。
多重性可以显式地写在函数类型中，如下所示：
ignoreN : (0 n : Nat) -> Vect n a -> Nat- 这个函数在运行时n将不可见duplicate : (1 x : a) -> (a, a)- 这个函数必须准确地只使用x一次（因此，顺便说一下，祝你实现它。这个例子没有实现，因为它需要使用x两次！)
如果没有多重性注解，参数是不受限制的。另一方面，如果名字被隐式绑定（比如上面两个例子中的 a ），那么参数就会被抹去。所以，上面的类型也可以写成：
ignoreN : {0 a : _} -> (0 n : Nat) -> Vect n a -> Natduplicate : {0 a : _} -> (1 x : a) -> (a, a)
本节描述了多重性对你的 Idris 2 程序的实际意义，并有几个例子。特别描述了：
如果将 Idris 1 程序转换到 Idris 2 ，对于大多数程序来说，其中你需要了解的最重要的问题是 擦除 。然而，最有趣的，也是给 Idris 2 带来更多表现力的，是 线性 ，所以我们将从线性开始。
线性
1 多重性表达了一个变量必须被精确的只使用一次。我们所说的 "使用 " 是指以下两种情况：
如果变量是一个数据类型或原始值，它将被模式匹配，例如，通过成为 case 语句的主题，或成为模式匹配的函数参数等等，
如果该变量是一个函数，则该函数被应用（即只用一个参数运行）
首先，我们将看到这在一些函数和数据类型的小例子上是如何工作的，然后看它如何被用来编码 资源协议 。
上面，我们看到了 duplicate 的类型。让我们试着以交互的方式来写它，看看出了什么问题。我们首先给出类型和一个带孔的骨架定义
duplicate : (1 x : a) -> (a, a)
duplicate x = ?help
检查一个孔的类型可以告诉我们作用域内每个变量的多重性。如果我们检查 ?help 的类型，我们会发现我们在运行时不能使用 a ，而且我们必须准确地只使用 x 一次：
Main> :t help
0 a : Type
1 x : a
-------------------------------------
help : (a, a)
如果我们用 x 来表示对中的一部分...
duplicate : (1 x : a) -> (a, a)
duplicate x = (x, ?help)
...那么剩下的孔的类型告诉我们，我们不能把它用于其他地方了：
Main> :t help
0 a : Type
0 x : a
-------------------------------------
help : a
如果我们尝试定义 duplicate x = (?help, x) ，也会发生同样的情况（试试吧！）。
为了避免解析上的歧义，如果你为一个变量给出一个明确的多重性，就像对 duplicate 的参数那样，你也需要给它一个名字。但是，如果这个名字不在类型的作用域内使用，你可以用 _ 来代替名字，如下所示：
duplicate : (1 _ : a) -> (a, a)
多重性 1 背后的意图是，如果我们有一个函数，其类型为以下形式...
f : (1 x : a) -> b
...那么类型系统给出的保证是： 如果 f x` 被精确使用一次，那么 x 被精确使用一次 。所以，如果我们坚持试图定义 duplicate ...:
duplicate x = (x, x)
...然后 Idris 会抱怨：
pmtype.idr:2:15--8:1:While processing right hand side of Main.duplicate at pmtype.idr:2:1--8:1:
There are 2 uses of linear name x
类似的直觉也适用于数据类型。考虑以下类型， Lin ，它包装了一个必须使用一次的参数， Unr ，它包装了一个可以不受限制使用的参数
data Lin : Type -> Type where
MkLin : (1 _ : a) -> Lin a
data Unr : Type -> Type where
MkUnr : a -> Unr a
如果 MkLin x 被使用一次，那么 x 被使用一次。但是如果 MkUnr x 被使用一次，就不能保证 x 被使用的频率。我们可以通过开始为 Lin 和 Unr 写投影函数来更清楚地看到这一点，以便提取参数
getLin : (1 _ : Lin a) -> a
getLin (MkLin x) = ?howmanyLin
getUnr : (1 _ : Unr a) -> a
getUnr (MkUnr x) = ?howmanyUnr
检查孔的类型表明，对于 getLin ，我们必须准确地使用 x 一次（因为 val 参数被使用一次，通过对其进行模式匹配为 MkLin x ，如果 MkLin x 被使用一次，x 必须使用一次）：
Main> :t howmanyLin
0 a : Type
1 x : a
-------------------------------------
howmanyLin : a
然而，对于 getUnr ，我们仍然必须使用 val 一次，再次对其进行模式匹配，但是使用 MkUnr x 一次并不会对 x 产生任何限制。因此， x 在 getUnr 的正文中可以不受限制地使用：
Main> :t howmanyUnr
0 a : Type
x : a
-------------------------------------
howmanyUnr : a
如果 getLin 有一个不受限制的参数...
getLin : Lin a -> a
getLin (MkLin x) = ?howmanyLin
...那么 x 在 howmanyLin 中是不受限制的：
Main> :t howmanyLin
0 a : Type
x : a
-------------------------------------
howmanyLin : a
记住从 MkLin 的类型中得到的直觉是，如果 MkLin x 正好使用一次， x 也正好使用一次。但是，我们没有说 MkLin x 会被精确使用一次，所以对 x 没有限制。
资源协议
利用能够表达参数的线性用法的一种方法是在定义资源使用协议时，我们可以使用线性来确保任何独特的外部资源只有一个实例，我们可以使用参数为线性的函数来表示该资源的状态转换。例如，一扇门可以处于两种状态之一， Open 或 Closed
data DoorState = Open | Closed
data Door : DoorState -> Type where
MkDoor : (doorId : Int) -> Door st
(好吧，我们在这里只是假装--想象一下 doorId 是对一个外部资源的引用！)
我们可以定义开门和关门的函数，明确描述它们如何改变门的状态，并且它们在门中是线性的
openDoor : (1 d : Door Closed) -> Door Open
closeDoor : (1 d : Door Open) -> Door Closed
记住，直觉是这样的：如果 openDoor d 被精确使用一次，那么 d 也会被精确使用一次。因此，只要门 d 在创建时具有多重性 1 ，我们就 知道 一旦对它调用 openDoor ，我们将不能再使用 d 。考虑到 d 是一个外部资源，而 openDoor 已经改变了它的状态，这是一件好事！
我们可以通过使用以下类型的 newDoor 函数来确保我们创建的任何门都具有多重性 1
newDoor : (1 p : (1 d : Door Closed) -> IO ()) -> IO ()
也就是说， newDoor 需要一个函数，它正好运行一次。这个函数需要一个门，这个门被精确地使用一次。我们将在 IO 中运行它，以表明当我们创建门时，与外部世界有一些互动。由于多重性 1 意味着门必须被精确地使用一次，我们需要在完成后能够删除门
deleteDoor : (1 d : Door Closed) -> IO ()
因此，一个正确的 门 协议的使用例子是
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d
d'' = closeDoor d' in
deleteDoor d''
交互性的建立这个程序是很有启发性的，沿途会出现一些漏洞，看看 d , d' 等变量的多重性如何变化。比如说
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d in
?whatnow
检查 ?whatnow 的类型，发现 d 现在已经用完了，但我们还必须要使用 d' 正好一次：
Main> :t whatnow
0 d : Door Closed
1 d' : Door Open
-------------------------------------
whatnow : IO ()
请注意， d 的多重性 0 意味着我们仍然可以 谈论它 - 特别是，我们仍然可以在类型中推理它 - 但我们不能在程序的其余部分的相关位置再次使用它。在整个程序中影射 d 这个名字也是可以的
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d = openDoor d
d = closeDoor d in
deleteDoor d
如果我们没有正确遵循协议——创建门，打开它，关闭它，然后删除它—— 那么程序就不能通过类型检查。例如，我们可以尝试在完成之前不删除门
doorProg : IO ()
doorProg
= newDoor $ \d =>
let d' = openDoor d
d'' = closeDoor d' in
putStrLn "What could possibly go wrong?"
这给出了以下错误：
Door.idr:15:19--15:38:While processing right hand side of Main.doorProg at Door.idr:13:1--17:1:
There are 0 uses of linear name d''
关于这里的细节还有很多要讲的!但是，这在很大程度上显示了我们如何在类型层面上使用线性来捕获资源使用协议。如果我们有一个需要保证线性使用的外部资源，比如 Door ，我们就不需要在 IO 单子中对该资源进行操作，因为我们已经对操作进行了排序，并且没有访问任何过时的资源状态。这类似于交互式程序在 Clean编程语言 中的工作方式，事实上这也是 IO 在Idris 2中的内部实现方式，用一个特殊的 %World 类型来表示外部世界的状态，它总是被线性地使用
public export
data IORes : Type -> Type where
MkIORes : (result : a) -> (1 x : %World) -> IORes a
export
data IO : Type -> Type where
MkIO : (1 fn : (1 x : %World) -> IORes a) -> IO a
在类型系统中拥有多重性，会引起一些有趣的问题，例如：
我们是否可以使用线性信息来告知内存管理，例如，对不需要进行垃圾回收的函数进行类型级别的保证？
应如何将多重性纳入
Functor,Applicative和Monad等接口？如果我们有
0，和1作为多重性，为什么要止步于此？为什么没有2，3或者更多（例如 Granule ）多重性多态怎么样，就像 Linear Haskell 提案 中那样？
即使没有这些， 现在 我们能做什么？
擦除
1 多重性在我们可以表达的属性种类方面给了我们很多可能性。但是， 0 多重性也许更重要，因为它允许我们精确地知道哪些值在运行时是相关的，哪些是编译时才有的（也就是说，哪些是被删除的）。使用 0 多重性意味着一个函数的类型现在可以准确地告诉我们它在运行时需要什么。
例如，在 Idris 1 中你可以得到一个向量的长度，如下所示
vlen : Vect n a -> Nat
vlen {n} xs = n
这很好，因为它在恒定时间内运行，但代价是 n 在运行时必须可用，所以在运行时我们总是需要向量的长度，如果我们曾经调用 vlen 。Idris 1 可以推断出是否需要长度，但是程序员没有简单的方法来确定。
在 Idris 2 中，我们需要明确指出，在运行时需要 n
vlen : {n : Nat} -> Vect n a -> Nat
vlen xs = n
(顺便说一下，还要注意在 Idris 2 中，在类型中绑定的名字也可以在定义中使用，而不需要明确地重新绑定它们)
这也意味着，当你调用 vlen 时，你需要可用的长度。例如，这将产生一个错误
sumLengths : Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen ys
Idris 2 会报告：
vlen.idr:7:20--7:28:While processing right hand side of Main.sumLengths at vlen.idr:7:1--10:1:
m is not accessible in this context
这意味着它需要使用 m 作为参数传递给 vlen xs ，在这里它需要在运行时可用，但是 m 在 sumLengths 中不可用，因为它有多重性 0 。
我们可以通过将 sumLengths 的右侧替换成一个孔来更清楚地看到这一点......
sumLengths : Vect m a -> Vect n a -> Nat
sumLengths xs ys = ?sumLengths_rhs
...然后在REPL检查孔的类型：
Main> :t sumLengths_rhs
0 n : Nat
0 a : Type
0 m : Nat
ys : Vect n a
xs : Vect m a
-------------------------------------
sumLengths_rhs : Nat
相反，我们需要为 m 和 n 提供无限制多重性的绑定
sumLengths : {m, n : _} -> Vect m a -> Vect n a —> Nat
sumLengths xs ys = vlen xs + vlen xs
请记住，在绑定器上不给出多重性，就像这里的 m 和 n 一样，意味着变量的使用不受限制。
如果你要将 Idris 1 程序转换到 Idris 2 中使用，这可能是你需要考虑的最大问题。但需要注意的是，如果你有绑定的隐式参数，例如...
excitingFn : {t : _} -> Coffee t -> Moonbase t
...那么最好确保 t 真的被需要，否则由于运行时间不必要地建立 t 的实例，性能可能会受到影响！
关于擦除的最后一点说明：试图对一个具有多重性 0 的参数进行模式匹配是一个错误，，除非其值可以从其他地方推断出来。因此，下面的定义会被拒绝
badNot : (0 x : Bool) -> Bool
badNot False = True
badNot True = False
这被拒绝了，错误是：
badnot.idr:2:1--3:1:Attempt to match on erased argument False in
Main.badNot
然而，下面的情况是好的，因为在 sNot 中，尽管我们似乎在被删除的参数 x 上进行了匹配，但它的值是可以从第二个参数的类型中唯一推断出来的
data SBool : Bool -> Type where
SFalse : SBool False
STrue : SBool True
sNot : (0 x : Bool) -> SBool x -> Bool
sNot False SFalse = True
sNot True STrue = False
到目前为止，Idris 2 的经验表明，在大多数情况下，只要你在 Idris 1 程序中使用非绑定隐式参数，它们在 Idris 2 中无需过多修改即可工作。 Idris 2 类型检查器将指出你在运行时需要非绑定隐式参数的地方--有时这既令人惊讶又具有启发性！
类型的模式匹配
思考依值类型的一种方式是将它们视为语言中的 "一等 " 对象，因为它们可以像其他结构体一样被分配给变量、传递和从函数中返回。但是，如果它们是真正的一等对象，我们也应该能够对它们进行模式匹配。Idris 2 允许我们这样做。例如
showType : Type -> String
showType Int = "Int"
showType (List a) = "List of " ++ showType a
showType _ = "something else"
我们可以进行以下尝试：
Main> showType Int
"Int"
Main> showType (List Int)
"List of Int"
Main> showType (List Bool)
"List of something else"
对函数类型进行模式匹配很有意思，因为返回类型可能取决于输入值。例如，让我们为 showType 添加一个案例
showType (Nat -> a) = ?help
检查 help 的类型将告诉我们：
Main> :t help
a : Nat -> Type
-------------------------------------
help : String
所以，返回类型 a 取决于类型 Nat 的输入值，我们需要想出一个值来使用 a ，比如说
showType (Nat -> a) = "Function from Nat to " ++ showType (a Z)
请注意，绑定器上的多重性，以及在 非擦除式 类型上的模式匹配能力，意味着以下两种类型是不同的
id : a -> a
notId : {a : Type} -> a -> a
在 notId 的情况下，我们可以在 a 上进行匹配，得到的函数肯定不是同一函数
notId {a = Integer} x = x + 1
notId x = x
Main> notId 93
94
Main> notId "???"
"???"
能够区分相关和不相关的类型参数有一个重要的结果，在一个函数中，如果 a 有多重性 0 ，那么 只有 a 是参数化的。所以，在 notId 的情况下， a 不是 参数，所以我们不能因为它是多态的而对该函数的行为方式得出任何结论，因为类型告诉我们它可能对 a 进行模式匹配。
另一方面，这只是一个巧合，在非依值类型的语言中，类型是 不相关的 并会被抹去，而值是 相关的 且会在运行时保留。Idris 2 是基于 QTT 的，允许我们精确区分相关和不相关的参数。类型可以是相关的，值（如 n 向量的索引）可以是不相关的。
关于多重性的更多细节，见 Idris 2: Quantitative Type Theory in Action 。