捕获检查

概述

捕获检查器扩展引入了新的类型，并强制执行了一些用于处理这些类型的规则。

功能和捕获类型

捕获检查是根据形式为 T^{c₁, ..., cᵢ} 的捕获类型进行的。这里 T 是一个类型，而 {c₁, ..., cᵢ} 是一个捕获集，包含对功能 c₁, ..., cᵢ 的引用。

功能在语法上是方法或类参数、局部变量或封闭类的 this。功能的类型必须是具有非空捕获集的捕获类型。我们还说作为功能的变量是跟踪的。

从某种意义上说，每个功能都从它捕获的另一个更广泛的功能获得其权限。最广泛的功能，所有其他功能最终都源于它，写成 cap。我们称之为通用功能。如果 T 是一个类型，那么 T^ 是 T^{cap} 的简写，表示 T 可以捕获任意功能。

以下是一个示例

class FileSystem

class Logger(fs: FileSystem^):
  def log(s: String): Unit = ... // Write to a log file, using `fs`

def test(fs: FileSystem^) =
  val l: Logger^{fs} = Logger(fs)
  l.log("hello world!")
  val xs: LazyList[Int]^{l} =
    LazyList.from(1)
      .map { i =>
        l.log(s"computing elem # $i")
        i * i
      }
  xs

这里，test 方法接受 FileSystem 作为参数。fs 是一个功能，因为它的类型具有非空捕获集。该功能被传递给 Logger 构造函数，并作为 Logger 类中的字段保留。因此，局部变量 l 的类型为 Logger^{fs}：它是一个保留 fs 功能的 Logger。

在 test 中定义的第二个变量是 xs，它是一个惰性列表，通过记录和映射连续数字从 LazyList.from(1) 获得。由于列表是惰性的，它需要保留对记录器 l 的引用以进行计算。因此，列表的类型是 LazyList[Int]^{l}。另一方面，由于 xs 仅记录而不执行其他文件操作，因此它仅间接保留 fs 功能。这就是为什么 fs 不出现在 xs 的捕获集中。

捕获类型具有子类型关系，其中具有“较小”捕获集的类型是具有较大捕获集的类型的子类型（子捕获 关系将在下面更详细地定义）。如果类型 T 没有捕获集，则称为纯类型，并且是向 T 添加捕获集的任何捕获类型的子类型。

函数类型

通常的函数类型 A => B 现在代表一个可以捕获任意功能的函数。我们称这样的函数为不纯函数。相反，新的单箭头函数类型 A -> B 代表一个不能捕获任何功能的函数，或者换句话说，是纯函数。可以在纯函数的箭头后面添加一个捕获集。例如，A ->{c, d} B 将是一个可以捕获功能 c 和 d 但不能捕获其他功能的函数。此类型是 (A -> B)^{c, d} 的简写，即具有可能的捕获 {c, d} 的函数类型 A -> B。

不纯函数类型 A => B 被视为 A ->{cap} B 的别名。也就是说，不纯函数是可以捕获任何内容的函数。

捕获注释 ^ 的绑定优先级高于函数箭头。因此 A -> B^{c} 被解读为 A -> (B^{c})。

类似的约定适用于上下文函数类型。A ?=> B 是一个不纯的上下文函数，A ?-> B 是它的纯补充。

注意 1：标识符 -> 和 ?-> 现在在用作中缀类型运算符时被视为软关键字。它们仍然可以作为项的常规标识符使用。例如，映射语法 Map("x" -> 1, "y" -> 2) 仍然受支持，因为它只适用于项。

注意 2：纯函数类型与不纯函数类型之间的区别不适用于方法。事实上，由于方法不是值，因此它们永远不会直接捕获任何内容。方法中对功能的引用将计入封闭对象的捕获集中。

按名称参数类型

类似于函数类型的约定也扩展到按名称参数。在

def f(x: => Int): Int

实际参数可以引用任意能力。因此以下情况是可以的

f(if p(y) then throw Ex() else 1)

另一方面，如果f是这样定义的

def f(x: -> Int): Int

实际参数f不能引用任何能力，因此上面的调用将被拒绝。也可以允许特定的能力，例如

def f(x: ->{c} Int): Int

这里，实际参数f被允许使用c能力，但不能使用其他能力。

子类型和子捕获

捕获影响子类型。通常我们写T₁ <: T₂来表示类型T₁是类型T₂的子类型，或者等效地，T₁符合T₂。类似的子捕获关系适用于捕获集。如果C₁和C₂是捕获集，我们写C₁ <: C₂来表示C₁被C₂覆盖，或者，交换操作数，C₂覆盖C₁。

子类型扩展到捕获类型如下

• 纯类型是捕获类型的子类型。也就是说，对于任何类型T，捕获集C，T <: C T。
• 对于捕获类型，较小的捕获集产生子类型：如果C₁ <: C₂且T₁ <: T₂，则C₁ T₁ <: C₂ T₂。

如果C₂解释了C₁中的每个元素c，则子捕获关系C₁ <: C₂成立。这意味着以下三个条件之一必须为真

• c ∈ C₂,
• c引用某个类Cls的参数，并且C₂包含Cls.this，
• c的类型具有捕获集C，并且C₂解释了C的每个元素（即，C <: C₂）。

示例 1. 给定

fs: FileSystem^
ct: CanThrow[Exception]^
l : Logger^{fs}

我们有

{l}  <: {fs}     <: {cap}
{fs} <: {fs, ct} <: {cap}
{ct} <: {fs, ct} <: {cap}

包含根能力{cap}的集合覆盖了所有其他捕获集。这是由于最终每个能力都是从cap创建的。

示例 2. 再次考虑之前的 FileSystem/Logger 示例。LazyList[Int] 是 LazyList[Int]^{l} 的一个真子类型。因此，如果该示例中的 test 方法声明为结果类型 LazyList[Int]，我们将得到一个类型错误。以下是错误消息

11 |def test(using fs: FileSystem^): LazyList[Int] = {
   |                                                 ^
   |                                        Found:    LazyList[Int]^{fs}
   |                                        Required: LazyList[Int]

为什么它说 LazyList[Int]^{fs} 而不是 LazyList[Int]^{l}，毕竟这是返回值 xs 的类型？原因是 l 是 test 主体中的一个局部变量，因此它不能在该主体之外的类型中被引用。相反，发生的是类型被扩展到不提及 l 的最小超类型。由于 l 的捕获集是 fs，因此我们有 {fs} 覆盖 {l}，并且 {fs} 在 test 的结果类型中是可以接受的，因此 {fs} 是该扩展的结果。这种扩展被称为规避；它不是特定于捕获检查的，而是适用于 Scala 类型中的所有变量引用。

能力类

像 CanThrow 或 FileSystem 这样的类具有这样的属性，即它们的价值总是打算作为能力。我们可以通过使用 @capability 注解声明这些类来明确这种意图并节省样板代码。

能力类类型的捕获集始终为 {cap}。这意味着我们可以等效地将 FileSystem 和 Logger 类表示如下

import annotation.capability

@capability class FileSystem

class Logger(using FileSystem):
  def log(s: String): Unit = ???

def test(using fs: FileSystem) =
  val l: Logger^{fs} = Logger()
  ...

在这个版本中，FileSystem 是一个能力类，这意味着 {cap} 捕获集隐含在 Logger 和 test 的参数中。显式编写捕获集会产生警告

class Logger(using FileSystem^{cap}):
                   ^^^^^^^^^^^^^^
             redundant capture: FileSystem already accounts for cap

最后一个示例版本中的另一个无关更改是 FileSystem 能力现在作为隐式参数传递。用隐式参数对能力进行建模非常自然，因为它在多个能力发挥作用时极大地减少了连接开销。

闭包的捕获检查

如果闭包在其主体中引用能力，它将在其类型中捕获这些能力。例如，考虑

def test(fs: FileSystem): String ->{fs} Unit =
  (x: String) => Logger(fs).log(x)

这里，test 的主体是一个 lambda，它引用了能力 fs，这意味着 fs 被保留在 lambda 中。因此，lambda 的类型为 String ->{fs} Unit。

注意： 函数值始终用 =>（或 ?=> 用于上下文函数）编写。纯函数值和非纯函数值之间没有语法区别。区别只体现在它们的类型中。

闭包还会捕获其调用的函数捕获的所有能力。例如，在

def test(fs: FileSystem) =
  def f() = g()
  def g() = (x: String) => Logger(fs).log(x)
  f

中，test 的结果类型为 String ->{fs} Unit，即使函数 f 本身没有引用 fs。

类的捕获检查

用于捕获检查闭包的原则也适用于类。例如，考虑

class Logger(using fs: FileSystem):
  def log(s: String): Unit = ... summon[FileSystem] ...

def test(xfs: FileSystem): Logger^{xfs} =
  Logger(xfs)

这里，类 Logger 将能力 fs 作为（私有）字段保留。因此，test 的结果类型为 Logger^{xfs}

有时，跟踪的能力仅用于类的构造函数中，但并不打算作为字段保留。可以通过将参数声明为 @constructorOnly 来将此事实传达给捕获检查器。示例

import annotation.constructorOnly

class NullLogger(using @constructorOnly fs: FileSystem):
  ...
def test2(using fs: FileSystem): NullLogger = NullLogger() // OK

类的捕获引用包括本地能力和参数能力。本地能力是在类外部定义并从其主体引用的能力。参数能力作为参数传递给类的主要构造函数。本地能力是继承的：超类的本地能力也是其子类的本地能力。示例

@capability class Cap

def test(a: Cap, b: Cap, c: Cap) =
  class Super(y: Cap):
    def f = a
  class Sub(x: Cap) extends Super(x)
    def g = b
  Sub(c)

这里类Super拥有局部能力a，它被类Sub继承，并与Sub自己的局部能力b结合。类Sub还拥有一个与参数x相对应的参数能力。此能力在最终的构造函数调用Sub(c)中实例化为c。因此，该调用的捕获集为{a, b, c}。

类this类型的捕获集由捕获检查器推断，除非类型用类似于此的自我类型注释显式声明。

class C:
  self: D^{a, b} => ...

推断观察以下约束。

• 类C的this类型包含C的所有捕获引用。
• 类C的this类型是C每个父类的this类型的子类型。
• this的类型必须遵守所有使用this的约束。

例如，在

@capability class Cap
def test(c: Cap) =
  class A:
    val x: A = this
    def f = println(c)  // error

我们知道this的类型必须是纯的，因为this是类型为A的val的右侧。但是，在最后一行中，我们发现类的捕获集，以及this的捕获集，将包含c。这会导致矛盾，从而导致检查错误。

16 |    def f = println(c)  // error
   |                    ^
   |(c : Cap) cannot be referenced here; it is not included in the allowed capture set {}

捕获隧道

考虑以下Pair类的简单定义。

class Pair[+A, +B](x: A, y: B):
  def fst: A = x
  def snd: B = y

如果Pair像这样实例化（假设ct和fs是作用域中的两个能力），会发生什么？

def x: Int ->{ct} String
def y: Logger^{fs}
def p = Pair(x, y)

最后一行将被类型化为如下。

def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y)

这可能看起来很奇怪。Pair(x, y)值确实捕获了能力ct和fs。为什么它们没有在外部的类型中显示出来？

答案是捕获隧道。一旦类型变量被实例化为捕获类型，捕获就不会传播到此点之外。另一方面，如果类型变量在访问时再次被实例化，捕获信息会再次“弹出”。例如，即使p在技术上是纯的，因为它的捕获集为空，但写入p.fst将记录对捕获的能力ct的引用。因此，如果此访问被放入闭包中，该能力将再次成为外部捕获集的一部分。例如。

() => p.fst : () -> Int ->{ct} String

换句话说，对能力的引用在泛型实例化中从创建到访问“隧道穿透”；它们不会影响封闭泛型数据构造函数应用程序的捕获集。这一原则在使捕获检查简洁实用方面发挥着重要作用。

逃逸检查

一些捕获集受到限制，因此不允许它们包含通用能力。

具体来说，如果一个捕获类型是类型变量的实例，那么该捕获类型不允许携带通用能力cap。这里与隧道连接有关。当从类型变量实例化类型时，类型的捕获集必须存在于环境中。但cap本身并不作为环境中的全局实体可用。因此，应该产生错误。

现在我们可以重建这个原则如何在介绍性示例中产生错误，其中usingLogFile是这样声明的

def usingLogFile[T](op: FileOutputStream^ => T): T = ...

错误消息是

   |  val later = usingLogFile { f => () => f.write(0) }
   |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
   |The expression's type () => Unit is not allowed to capture the root capability `cap`.
   |This usually means that a capability persists longer than its allowed lifetime.

此错误消息是由以下逻辑产生的

• f参数的类型是FileOutputStream^，这使其成为一个能力。
• 因此，表达式() => f.write(0)的类型是() ->{f} Unit。
• 这使得传递给usingLogFile的整个闭包的类型成为依赖函数类型(f: FileOutputStream^) -> () ->{f} Unit。
• 闭包的预期类型是一个简单的、参数化的、不纯的函数类型FileOutputStream^ => T，对于类型变量T的某些实例化。
• 闭包的依赖函数类型的最小超类型，它是一个参数化函数类型，是FileOutputStream^ => () ->{cap} Unit
• 因此，类型变量T被实例化为() ->{cap} Unit，或简写为() => Unit，这会导致错误。

可变变量的类型也存在类似的限制。另一种试图破坏捕获检查的方法是将具有局部能力的闭包分配给全局变量。也许像这样

var loophole: () => Unit = () => ()
usingLogFile { f =>
  loophole = () => f.write(0)
}
loophole()

但这也不会编译，因为可变变量不能具有通用捕获集。

还需要防止在参数化类型的参数中返回或分配具有局部能力的闭包。例如，这里有一个稍微改进的攻击

class Cell[+A](x: A)
val sneaky = usingLogFile { f => Cell(() => f.write(0)) }
sneaky.x()

在创建Cell的点，参数的捕获集是f，这是可以的。但在使用时，它是cap（因为f不再在范围内），这再次导致错误

   |  sneaky.x()
   |  ^^^^^^^^
   |The expression's type () => Unit is not allowed to capture the root capability `cap`.
   |This usually means that a capability persists longer than its allowed lifetime.

观察对象图，我们观察到一个单调性属性：对象x的捕获集覆盖了通过x可达的所有对象的捕获集。此属性在类型系统中通过以下单调性规则反映出来

• 在具有字段 f 的类 C 中，捕获集 {this} 包含捕获集 {this.f} 以及对 this.f 应用于纯参数的任何应用的捕获集。

检查异常

Scala 通过语言导入启用检查异常。以下是一个示例，取自 更安全的异常页面，并在 论文 中进行了描述，该论文在 2021 年 Scala 研讨会上发表。

import language.experimental.saferExceptions

class LimitExceeded extends Exception

val limit = 10e+10
def f(x: Double): Double throws LimitExceeded =
  if x < limit then x * x else throw LimitExceeded()

新的 throws 子句扩展为一个隐式参数，它提供 CanThrow 功能。因此，函数 f 可以等效地写成这样

def f(x: Double)(using CanThrow[LimitExceeded]): Double = ...

如果缺少隐式参数，则会报告错误。例如，函数定义

def g(x: Double): Double =
  if x < limit then x * x else throw LimitExceeded()

将被以下错误消息拒绝

  |  if x < limit then x * x else throw LimitExceeded()
  |                               ^^^^^^^^^^^^^^^^^^^^^
  |The capability to throw exception LimitExceeded is missing.
  |The capability can be provided by one of the following:
  | - Adding a using clause `(using CanThrow[LimitExceeded])` to the definition of the enclosing method
  | - Adding `throws LimitExceeded` clause after the result type of the enclosing method
  | - Wrapping this piece of code with a `try` block that catches LimitExceeded

CanThrow 功能是 throw 表达式所必需的，并且由 try 表达式创建。例如，表达式

try xs.map(f).sum
catch case ex: LimitExceeded => -1

将被编译器扩展为类似以下内容

try
  erased given ctl: CanThrow[LimitExceeded] = compiletime.erasedValue
  xs.map(f).sum
catch case ex: LimitExceeded => -1

（ctl 功能仅用于类型检查，不需要出现在生成的代码中，因此可以声明为擦除的。）

与其他基于功能的方案一样，需要防止捕获结果中的功能。例如，以下是一个有问题的用例

def escaped(xs: Double*): (() => Double) throws LimitExceeded =
  try () => xs.map(f).sum
  catch case ex: LimitExceeded => () => -1
val crasher = escaped(1, 2, 10e+11)
crasher()

此代码需要被拒绝，否则对 crasher() 的调用会导致未处理的 LimitExceeded 异常被抛出。

在语言导入 language.experimental.captureChecking 下，代码确实被拒绝了

14 |  try () => xs.map(f).sum
   |  ^
   |The expression's type () => Double is not allowed to capture the root capability `cap`.
   |This usually means that a capability persists longer than its allowed lifetime.
15 |  catch case ex: LimitExceeded => () => -1

为了集成异常和捕获检查，只需要进行两个更改

• CanThrow 被声明为 @capability 类，因此所有对 CanThrow 实例的引用都会被跟踪。
• 转义检查扩展到 try 表达式。try 的结果类型不允许捕获通用功能。

一个更大的例子

作为一个更大的例子，我们展示了惰性列表的实现和一些用例。为简单起见，我们的列表仅在尾部部分是惰性的。这对应于 Scala-2 类型 Stream 所做的，而 Scala 3 的 LazyList 类型计算严格较少，因为它在第一个参数中也是惰性的。

以下是我们版本的惰性列表的基本特征 LzyList

trait LzyList[+A]:
  def isEmpty: Boolean
  def head: A
  def tail: LzyList[A]^{this}

请注意，tail 带有捕获注释。它表示惰性列表的尾部可能捕获与整个惰性列表相同的引用。

LzyList 的空情况按惯例编写

object LzyNil extends LzyList[Nothing]:
  def isEmpty = true
  def head = ???
  def tail = ???

以下是惰性 cons 节点的类公式

import scala.compiletime.uninitialized

final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]:
  private var forced = false
  private var cache: LzyList[A]^{this} = uninitialized
  private def force =
    if !forced then { cache = tl(); forced = true }
    cache

  def isEmpty = false
  def head = hd
  def tail: LzyList[A]^{this} = force
end LzyCons

LzyCons 类接受两个参数：一个头部 hd 和一个尾部 tl，它是一个返回 LzyList 的函数。函数及其结果都可以捕获任意功能。在私有可变字段 cache 中第一次解引用 tail 后，将记忆应用函数的结果。请注意，赋值 cache = tl() 的类型依赖于 {this} 捕获集的单调性规则。

以下是一个扩展方法，用于为惰性列表定义一个中缀连接运算符 #:。它类似于 ::，但它不会评估其右操作数，而是生成一个惰性列表。

extension [A](x: A)
  def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} =
    LzyCons(x, () => xs1)

请注意，#: 以一个不纯的按名调用参数 xs1 作为其右参数。#: 的结果是一个捕获该参数的惰性列表。

作为 #: 的一个示例用法，以下是一个方法 tabulate，它使用生成器函数 gen 创建一个给定长度的惰性列表。生成器函数允许有副作用。

def tabulate[A](n: Int)(gen: Int => A) =
  def recur(i: Int): LzyList[A]^{gen} =
    if i == n then LzyNil
    else gen(i) #: recur(i + 1)
  recur(0)

以下是如何使用 tabulate

class LimitExceeded extends Exception
def squares(n: Int)(using ct: CanThrow[LimitExceeded]) =
  tabulate(10): i =>
    if i > 9 then throw LimitExceeded()
    i * i

squares 的推断结果类型为 LzyList[Int]^{ct}，即它是一个惰性列表，其中包含 Int，当它通过调用 tail 一次或多次来细化时，可能会抛出 LimitExceeded 异常。

以下是一些用于映射、过滤和连接惰性列表的进一步扩展方法

extension [A](xs: LzyList[A]^)
  def map[B](f: A => B): LzyList[B]^{xs, f} =
    if xs.isEmpty then LzyNil
    else f(xs.head) #: xs.tail.map(f)

  def filter(p: A => Boolean): LzyList[A]^{xs, p} =
    if xs.isEmpty then LzyNil
    else if p(xs.head) then xs.head #: xs.tail.filter(p)
    else xs.tail.filter(p)

  def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} =
    if xs.isEmpty then ys
    else xs.head #: xs.tail.concat(ys)

  def drop(n: Int): LzyList[A]^{xs} =
    if n == 0 then xs else xs.tail.drop(n - 1)

它们的捕获注释都与预期一致

• 映射一个惰性列表会生成一个惰性列表，该列表捕获原始列表以及（可能不纯的）映射函数。
• 过滤一个惰性列表会生成一个惰性列表，该列表捕获原始列表以及（可能不纯的）过滤谓词。
• 连接两个惰性列表会生成一个捕获两个参数的惰性列表。
• 从惰性列表中删除元素会提供一个安全的近似值，其中原始列表在结果中被捕获。事实上，只有列表的一部分后缀在运行时被保留，但我们的模型识别了惰性列表及其后缀，因此这些额外的知识将无用。

当然，传递给 map 或 filter 的函数也可以是纯函数。毕竟，A -> B 是 (A -> B)^{cap} 的子类型，它与 A => B 相同。在这种情况下，纯函数参数将不会出现在 map 或 filter 的结果类型中。例如

val xs = squares(10)
val ys: LzyList[Int]^{xs} = xs.map(_ + 1)

映射列表 ys 的类型在其捕获集中只有 xs。实际的函数参数没有出现，因为它很纯。同样，如果惰性列表 xs 是纯的，它也不会出现在任何方法结果中。这表明基于能力的效果系统与捕获检查自然地是效果多态的。

这结束了我们的示例。值得一提的是，定义和使用标准严格列表的等效程序根本不需要任何捕获注释。它将完全按照现在在标准 Scala 3 中编写的那样编译，但你将免费获得捕获检查。本质上，=> 已经意味着“可以捕获任何东西”，并且由于在严格列表中，副作用操作不会保留在结果中，因此没有额外的捕获需要记录。严格列表当然可以在其元素中捕获副作用闭包，但随后会应用隧道，因为这些元素由类型变量表示。这意味着我们也不需要在那里注释任何东西。

另一种可能性是惰性列表的变体，它要求传递给 map、filter 及其类似操作的所有函数都是纯的。例如，此列表上的 map 将这样定义

extension [A](xs: LzyList[A])
  def map[B](f: A -> B): LzyList[B] = ...

该变体也不需要任何捕获注释。

总之，数据结构设计有两个“最佳点”：副作用或资源感知代码中的严格列表，以及纯函数代码中的惰性列表。两者在没有显式注释的情况下都已正确捕获类型。捕获注释只在语义变得更复杂时才会发挥作用，因为我们处理延迟效果，例如在不纯的惰性列表或严格列表上的副作用迭代器中。与以前的技术相比，这种特性可能是我们捕获检查方法的最大优势之一，以前的技术往往更嘈杂。

函数类型缩写

待定

编译选项

以下选项与捕获检查相关。

• -Xprint:cc 打印带有捕获类型的程序，这些类型是由捕获检查推断出来的。
• -Ycc-debug 提供有关捕获检查的更详细的实现导向信息，如下一节所述。

支持这些选项的捕获检查实现目前位于 dotty.epfl.ch 上的 cc-experiment 分支中。

捕获检查内部机制

捕获检查器被设计为一个传播约束求解器，它在类型检查和一些初始转换之后作为一个独立的阶段运行。

约束变量代表未知的捕获集。为先前推断类型的每个部分，

• 为每个方法、类、匿名函数或按名称参数的访问引用，
• 为类构造函数调用中传递的参数，
• 引入一个约束变量。

显式写入类型中的捕获集被视为常量（在捕获检查之前，这些集合被简单地忽略）。

捕获检查器本质上使用通常的类型规则重新检查程序。每次检查捕获类型之间的子类型要求时，这都会转换为对捕获集的子捕获测试。如果两个集合是常量，这只是一个是或否的问题，其中否会产生错误消息。

如果比较 C₁ <: C₂ 中的较低集合 C₁ 是一个变量，则集合 C₂ 被记录为 C₁ 的超集。如果较高的集合 C₂ 是一个变量，则 C₁ 的元素被传播到 C₂。将元素 x 传播到集合 C 意味着 x 被包含在 C 中作为元素，并且它也被传播到 C 的所有已知超集。如果这样的超集是常量，则检查 x 是否包含在其中。如果不是这样，则原始比较 C₁ <: C₂ 没有解决方案，并报告错误。

类型检查器还对类型执行各种映射，例如在依赖函数中将实际参数类型替换为形式参数类型时，或在选择中使用“从...看”映射成员类型。映射跟踪类型中位置的方差。方差最初是协变的，它在函数参数位置翻转为逆变，并且在类型参数中可以是协变、逆变或非变的，具体取决于类型参数的方差。

在捕获检查时，相同的映射也对捕获集执行。如果捕获集是常量，则其元素（即能力）被映射为常规类型。如果此类映射的结果不是能力，则根据类型的方差近似结果。协变近似将类型替换为其捕获集。逆变近似将它替换为空捕获集。非变近似将封闭的捕获类型替换为一系列可能的类型，这些类型将被进一步传播和解析。

当对捕获集变量 C 执行映射 m 时，会创建一个新变量 Cm，其中包含映射的元素，并且与 C 链接。如果 C 随后通过传播获得更多元素，这些元素也会在通过 m 映射转换后传播到 Cm。Cm 还获得与 C 相同的超集，再次使用 m 映射。

捕获检查器的一个有趣方面是捕获隧道实现。捕获检查所基于的基础理论通过所谓的box和unbox操作显式地实现隧道。Boxing隐藏捕获集，而unboxing则恢复它。捕获检查器根据实际类型和预期类型插入虚拟的box和unbox操作，类似于类型检查器插入隐式转换的方式。当捕获集变量首次引入时，任何在捕获类型中作为类型参数实例的实例的捕获集都被标记为“boxed”。如果表达式的预期类型是具有boxed捕获集变量的捕获类型，则会插入boxing操作。插入的效果是，对boxed表达式中功能的任何引用都会被遗忘，这意味着捕获传播被停止。相反，如果表达式的实际类型具有boxed变量作为捕获集，则会插入unbox操作，这会将捕获集中的所有元素添加到环境中。

Boxing和unboxing对运行时没有影响，因此这些操作的插入只是模拟的；唯一可见的影响是捕获集中的变量在当前检查的表达式的环境中被撤回和插入。

-Ycc-debug选项提供了一些关于捕获检查器工作原理的见解。当它被打开时，boxed集会被显式地标记，并且捕获集变量会以ID和一些关于它们来源的信息打印出来。例如，字符串{f, xs}33M5V表示一个已知包含元素f和xs的捕获集变量。变量的ID是33。M表示该变量是通过从ID为5的变量映射而创建的。后者是一个常规变量，如V所示。

通常，捕获集后面的字符串由交替的数字和字母组成，其中每个数字表示一个变量ID，每个字母表示变量的来源。可能的字母是

• V：一个常规变量，
• M：一个变量，它是通过将字符串右侧指示的变量映射而产生的，
• B：类似于M，但映射是一个双射，
• F：一个变量，它是通过过滤字符串右侧指示的变量的元素而产生的，
• I : 由两个捕获集的交集产生的变量。
• D : 由两个捕获集的差集产生的变量。
• R : 一个细化类参数的普通变量，以便在类实例类型中知道构造函数参数的捕获集。

在编译运行结束时，-Ycc-debug 将打印之前输出中引用的变量的所有变量依赖关系。以下是一个示例

Capture set dependencies:
  {}2V                 ::
  {}3V                 ::
  {}4V                 ::
  {f, xs}5V            :: {f, xs}31M5V, {f, xs}32M5V
  {f, xs}31M5V         :: {xs, f}
  {f, xs}32M5V         ::

本节列出了之前诊断中出现的所有变量及其依赖关系，递归地。例如，我们了解到

• 变量 2、3、4 为空，没有依赖关系。
• 变量 5 有两个依赖关系：变量 31 和 32，它们都来自映射变量 5。
• 变量 31 有一个常量固定超集 {xs, f}
• 变量 32 没有依赖关系。