스코프가 있는 캐퍼빌리티

스코프가 있는 캐퍼빌리티 (Scoped Capabilities)

이 페이지는 Scala 3의 캡처 체킹(capture checking)에서 등장하는 any 캐퍼빌리티가 어떻게 스코프(범위)와 엮여 있는지, 그리고 fresh라는 관련 개념이 왜 필요한지를 설명해요. 앞서 다룬 이스케이프 체킹 이야기를 바탕으로, 캐퍼빌리티가 어디서 정의되고 어디까지 흘러갈 수 있는지를 이해하게 됩니다.

출처: Scala 3 Reference

본문

서론 (Introduction)

앞서 이스케이프 체킹을 이야기할 때 우리는 스코프 규율(scoping discipline)을 언급했어요. 즉 캡처 집합에는 그 집합이 정의된 지점에서 보이는 캐퍼빌리티만 담길 수 있다는 뜻이죠. 그런데 그러면 자연스럽게 이런 질문이 생겨요. 보편 캐퍼빌리티인 any는 도대체 어디에 정의되어 있는 걸까요?

여기서 핵심 원칙은, any가 등장할 때마다 각각 서로 다른 캐퍼빌리티를 나타낸다는 거예요. 각 any는 같은 레벨 또는 더 바깥 레벨의 캐퍼빌리티들을, 다른 any까지 포함해서 하위 캡처(subsu )할 수 있어요. 이 성질은 분리 체킹(separation checking)에서 중심이 되는데, 분리 체킹에서는 각 any가 자기 자신만의, 자신이 하위 캡처하는 숨은 캐퍼빌리티 집합을 가지게 되거든요.

any 말고도 관련된 캐퍼빌리티로 fresh가 있어요. 이건 import caps.fresh로 사용할 수 있고, 함수 타입의 결과 타입에 등장할 수 있죠. 함수 결과에서 any가 둘러싼 스코프의 로컬 any를 가리킨다면, fresh는 새롭게 존재적으로 묶인(existentially bound) 캐퍼빌리티를 도입해서 호출할 때마다 서로 구별되고 격리된 결과가 나온다는 걸 보장해요. fresh에 대해서는 아래에서 자세히 다룹니다.

`any`가 나타나는 위치 (Where any Appears)

any(또는 fresh)가 나타날 수 있는 위치는 네 가지로 구분해요.

로컬 any (Local anys): 모든 클래스, 메서드 본문, 블록은 자기만의 로컬 any를 가져요. 이 any는 해당 스코프 안에서 사용된 캐퍼빌리티들을 추상화해서, 바깥 세계에는 단 하나의 이름으로 대표해 주죠. 로컬 any들은 어휘적 중첩(lexical nesting)에 기반한 하위 캡처 계층(subcapturing hierarchy)을 이룹니다.

파라미터 any (Parameter anys): any가 함수 파라미터 타입에 나타나면(예: def foo(x: T^)) 해당 파라미터에 묶인 자신만의 any를 갖게 돼요. 호출 지점에서는 이 파라미터 any가 실제로 전달된 캐퍼빌리티들로 인스턴스화됩니다.

결과 any (Result anys): any가 함수 결과 타입에 나타나면(예: A^ -> B^, 즉 A^{any} -> B^{any}) 둘러싼 스코프의 로컬 any를 가리켜요. 그런 함수를 두 번 호출해도 결과의 캡처 집합 경계는 같아요.

결과 fresh (Result freshs): any 대신 함수 타입의 결과 타입에 fresh라고 쓸 수 있어요(예: A^ -> B^{fresh}). 이는 함수를 호출할 때마다 새롭고 구별되는 캐퍼빌리티를 캡처한 결과가 나온다는 뜻이라서 이름도 fresh예요. 결과 any와 달리 결과 fresh는 격리되어 있어서, 둘러싼 스코프의 캐퍼빌리티들과 합쳐질 수 없어요. 참고로 fresh는 함수 타입에만 적용되고, 메서드 반환 타입에는 적용되지 않아요(메서드는 any를 사용하죠).

그래서 T^(T^{any}의 약어)를 쓸 때, any는 "뭔가를 캡처한다"는 뜻이지 정확히 뭘 캡처하는지는 이름을 붙이지 않아요. 그리고 문맥에 따라 캡처 체커가 하위 캡처를 통해 어떤 캐퍼빌리티가 그 안으로 흘러들어갈 수 있는지 제약을 걸어요. 반면 T^{fresh}라고 쓰면 "새롭고 격리된 무언가를 캡처한다"는 뜻이 되고, 실질적인 차이는 아래 비교에서 확인할 수 있어요.

다른 비유로 보면, 이렇게 여러 any들은 프로그램 구조의 요소(스코프, 파라미터, 반환값 같은 것들)에 붙는, 암시적으로 이름 붙여진 존재적(∃) 또는 추상적 자기 캡처 집합의 일종이라고 할 수 있어요.

로컬 any (Local anys)

로컬 any들은 어휘적 중첩에 기반한 하위 캡처 계층을 이뤄요. 중첩된 스코프의 로컬 any는 자기 바깥 스코프의 로컬 any를 하위 캡처하죠. 안쪽 스코프는 바깥 스코프에서 쓸 수 있는 캐퍼빌리티는 물론이고 안쪽에서 새로 정의한 것까지 모두 쓸 수 있으니 당연한 일이에요. 최상위에는 진짜 보편 any, 즉 전역 스코프의 로컬 any가 있고, 모든 로컬 any들은 궁극적으로 이걸 하위 캡처합니다:

// top level: the global `any`
class Outer: // has local any₁
  val f1: File^ = File("f1") // File^{any₁}
  def method() = // has local any₂
    val f2: File^ = File("f2") // File^{any₂}
    var ref: () => Unit = null // () ->{any₂} Unit, can accept what can flow into any₂
    val closure = () => // has local any₃
      val f3: File^ = File("f3") // File^{any₃}
      val f4: File^ = f2 // ok, because {any₂} <: {any₃}
      val f5: File^ = f1 // ok, because {any₁} <: {any₃}
      ref = () => f3.read() // error, f3 is at the level of any₃ and cannot flow into any₂
      ...

각 캐퍼빌리티는 그걸 정의한 스코프의 로컬 any에 해당하는 레벨(level)을 가져요. 레벨은 캐퍼빌리티가 어디까지 흘러갈 수 있는지를 결정해요. 같은 레벨이거나 더 깊게 중첩된 any로는 흘러갈 수 있지만, 바깥 스코프 쪽으로(즉 캐퍼빌리티가 자기 어휘적 수명보다 더 오래 사는 방향으로)는 흘러갈 수 없죠. 컴파일러는 소유 체인(ownership chain)을 따라 올라가며 레벨 경계(level boundary)를 나타내는 심볼에 도달할 때까지 걸어가서 캐퍼빌리티의 레벨을 계산해요. 레벨 경계는 다음과 같아요:

클래스 (Classes)
정적 객체 (Static objects)
메서드 (Methods)

f1, f2, ref 같은 로컬 값들은 자기만의 레벨을 정의하지 않아요. 그들은 둘러싼 메서드나 클래스의 레벨을 물려받죠. 예를 들어 이런 의미가 있어요:

f1은 Outer의 레벨에 있어요. 즉 f1은 로컬 any₁을 하위 캡처해요.
f2와 ref는 모두 method의 레벨에 있어요. 둘 다 로컬 any₂를 하위 캡처하죠.
어휘적 중첩에 의해 {any₂} <: {any₃}는 성립하지만, {any₃} <: {any₂}는 성립하지 않아요. 그래서 {f3}이 {any₃}에 하위 캡처로 묶여 있기 때문에 클로저를 ref에 할당할 수 없어요.

캡처 청구하기 (Charging Captures)

캐퍼빌리티를 사용할 때는 그게 주변의 모든 스코프가 가진 캡처 집합 제약과 호환되는지 검사해야 해요. 이 과정을 캡처를 환경에 청구한다(charging the capability to the environment)고 불러요.

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
def outer(fs: FileSystem^): Unit =
  def inner: () ->{fs} Unit =
    () => fs.read()  // fs is used here
  inner()

캡처 체커가 fs.read()를 볼 때, fs가 각 둘러싼 스코프로 흘러들어갈 수 있는지를 확인해요:

바로 바깥의 클로저 () => fs.read()는 자기 캡처 집합에 fs를 허용해야 해요 ✓
바깥 메서드 inner는 fs를 반영해야 해요(캡처 집합으로 반영하고 있죠) ✓
바깥 메서드 outer도 fs를 반영해야 해요(파라미터로 반영하고 있어요) ✓

어느 스코프든 캐퍼빌리티를 받아들이기를 거부하면 캡처 체킹은 실패해요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
def process(fs: FileSystem^): Unit =
  val f: () -> Unit = () => fs.read()  // error: fs cannot flow into {}

여기 클로저는 순수하게(() -> Unit) 선언됐어요. 즉 로컬 any가 빈 집합이라는 뜻이죠. 빈 집합에는 fs가 흘러들어갈 수 없으므로 체커는 이 코드를 거부합니다.

가시성과 넓히기 (Visibility and Widening)

캐퍼빌리티가 바깥 스코프로 흘러나갈 때는 계속 보여야(visible) 해요. 로컬 캐퍼빌리티는 자기 정의 스코프 바깥의 타입에는 등장할 수 없어요. 그럴 때 캡처 집합은 보이는 가장 작은 상위 캡처 집합으로 넓혀집니다(widened):

def test(fs: FileSystem^/*{any₁}*/): Logger^{fs} =
  val localLogger = Logger(fs)
  localLogger  // Type widens from Logger^{localLogger} to Logger^{fs}

여기서 localLogger는 로컬 변수라서 결과 타입에 등장할 수 없어요. 캡처 집합 {localLogger}는 fs를 캡처하므로 {fs}로 넓혀지고, test 바깥에서도 보이게 됩니다.

트라이-위드-리소스, 다시 보기 (Try-With-Resources, Again)

로컬 any는 try-with-resources 패턴에 대한 이스케이프 체킹을 가능하게 하는 메커니즘 중 하나예요. 이들은 스코프가 있는 캐퍼빌리티가 가변 변수에 (직접적이든 간접적이든) 할당되는 것을 통해 탈출하는 것을 막아요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
def withFile[T](path: String)(block: File^ => T): T = ???
def test(): Unit =
  var esc: File^/*{any₁}*/ = null

  withFile("test.txt"): f /* : File^{any₂} */ =>
    esc = f   // error, since any₂ cannot flow into any₁

다른 메커니즘은 함수 결과에서 any를 신중하게 다루는 것(아래 참조)으로, f를 붙잡고 있는 클로저를 반환하는 걸 막아줘요.

나중에 나올 캐퍼빌리티 분류자(capability classifiers) 섹션은, 탈출이 바람직한 상황에서 캐퍼빌리티가 자기 레벨을 벗어나는 걸 허용하는 제어된 메커니즘을 추가할 거예요.

클래스의 로컬 any (Local anys of Classes)

클래스는 자기 본문의 스코프에 해당하는 자신만의 로컬 any를 받아요. 이 any는 클래스의 각 인스턴스에 붙게 될 새 any의 템플릿 역할을 하죠. 클래스 본문 안에서 클래스의 any를 가리키는 참조는 암시적으로 경로 this가 붙습니다:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
class Logger(fs: FileSystem^) extends SharedCapability: // local any₁
  // Logger has its own local any₁, accessed as this.any₁
  val file: File^ = fs.open("log.txt")  // File^{this.any₁}
  def log(msg: String): Unit = file.write(msg)

클래스가 다른 클래스나 트레이트를 상속하면, extends 절에 있는 모든 수퍼타입의 any들이 본질적으로 현재 클래스의 any와 통합돼요. 이렇게 통합되는 이유는 모든 상속된 멤버가 this를 통해 접근되기 때문에 로컬 any들이 하위 타입 관계를 통해 서로 일치하게 되기 때문이에요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
trait Super extends ExclusiveCapability: // local any₁
  val doSomething: () => Unit // () ->{any₁} Unit

class Logger(fs: FileSystem^) extends Super: // local any₂
  val file: File^ = fs.open("log.txt") // File^{any₂}
  def log(msg: String): Unit = file.write(msg)
  val doSomething = () => log("hello") // ok, since {file} <: {this.any₂} =:= {this.any₁}

클래스의 캡처 체킹(Capture Checking of Classes)에서 설명했듯이, 캡처 체커는 클래스의 self-type을 통해 클래스 any의 내용에 대한 제약을 추론하고 검증하며, 불일치가 있으면 보고해요.

인스턴스를 만들 때는 클래스의 템플릿 any가 새 객체에 특정된 새 any로 치환됩니다:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
class Logger(fs: FileSystem^) extends SharedCapability: // local any₁
  // Logger has its own local any₁, accessed as this.any₁
  val file: File^ = fs.open("log.txt")  // File^{this.any₁}
  def log(msg: String): Unit = file.write(msg)
def test(fs: FileSystem^) = /* local any₁ */
  val logger1 = Logger(fs)  // New logger1.any for this instance, capturing fs
  val logger2 = Logger(fs)  // New logger2.any, distinct from logger1.any

참고로 logger1과 logger2에 붙은 any들은 앞서 설명한 규칙에 따라 메서드 test의 로컬 any를 하위 캡처해요.

개념적으로 클래스의 로컬 any는 클래스와 그 모든 수퍼타입에 존재하는 암시적 캡처 집합 멤버처럼 동작합니다:

class Logger(fs: FileSystem^) extends Super:
  type Cap^
  val file: File^{Cap} = ...
  // ...

함수 타입의 파라미터·결과 any (Parameter and Result anys in Function Types)

지금까지 우리는 어휘적 중첩 계층을 따르는 로컬 any를 다뤘어요. 하지만 any는 특별한 바인딩 규칙이 적용되는 함수 파라미터 타입과 결과 타입에도 나타날 수 있어요.

존재적 바인딩 (Existential Binding)

이런 메서드를 생각해 봐요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
trait FileSystem extends SharedCapability:
  def open(name: String): File^
  def read(): Unit
class Logger(fs: FileSystem^) extends SharedCapability: // local any₁
  // Logger has its own local any₁, accessed as this.any₁
  val file: File^ = fs.open("log.txt")  // File^{this.any₁}
  def log(msg: String): Unit = file.write(msg)
def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs)

이 메서드는 fs를 캡처하는 Logger를 만들어요. 반환 타입을 Logger^{fs}로 더 구체적으로 지정할 수도 있었지만, 현재 정의도 유효하고, 반환된 로거가 정확히 뭘 캡처하는지 숨기고 싶을 땐 이쪽이 더 나을 수도 있어요. 위처럼 쓴다면 반환 타입에 암시된 any는 당연히 fs 캐퍼빌리티를 흡수할 수 있어야 해요. 즉 이 any는 fs가 보이는 스코프에서 정의되어야 한다는 뜻이에요.

논리학에서 이런 스코프를 얻는 일반적인 방법은 존재 수량자(existential binder)를 쓰는 거예요. makeLogger의 타입을 이렇게 표현할 수 있어요:

makeLogger: (fs: ∃any₁.FileSystem^{any₁}): ∃fresh. Logger^{fresh}

말로 풀면, makeLogger는 어떤 보편 캐퍼빌리티 any₁을 캡처하는 타입 FileSystem의 파라미터 fs를 받아서, 어떤 (아마 다른) fresh 캐퍼빌리티를 캡처하는 Logger를 반환한다는 뜻이에요.

함수 파라미터의 존재 수량자를 함수 자신의 보편 "forall"로 바꿀 수도 있어요. 그런 대안 표기법에서 makeLogger의 타입은 이렇게 읽힙니다:

makeLogger: ∀any₁.(fs: FileSystem^{any₁}): ∃fresh. Logger^{fresh}

여기에는 캡처 다형성(capture polymorphism)과 연결고리가 있어요. 함수 파라미터의 any는 호출 지점에서 임의의 캐퍼빌리티로 인스턴스화할 수 있는 추가 캡처 파라미터처럼 동작합니다.

함수 타입의 확장 규칙 (Expansion Rules for Function Types)

메서드 타입의 관례는 함수 타입에도 그대로 이어져요. 결과에 fresh가 있는 함수 타입, 예를 들어

(x: T) -> U^{fresh}

은 존재적으로 묶인 fresh가 있는 것으로 해석됩니다:

(x: T) -> ∃fresh.U^{fresh}

이 규칙은 모든 종류의 함수 화살표(->, =>, ?->, ?=>)에 동일하게 적용돼요. 따라서 이 경우 fresh는 함수 파라미터 x를 흡수할 수 있어요. x는 함수 결과 안에서 지역적으로 묶여 있으니까요.

존재적으로 묶이는 캐퍼빌리티로 확장되는 것은 fresh뿐이고, 함수를 어떻게 쓰든 그 결과는 같아요. 예를 들어 이 두 타입 모두 결과 캐퍼빌리티가 존재적으로 묶여 있어요:

A => B^{fresh}                         // ∃fresh. A ->{any} B^{fresh}
(x: A) -> B -> C^{fresh}               // (x: A) -> ∃fresh. B -> C^{fresh}

사실상 우리는 어떤 "2급(first/second-class)" 존재적 캡처 타입을 가지는 셈인데, 이 타입은 신중하게 제한되어 있고 타입 구조와 fresh의 등장으로부터 암시됩니다. 일급 존재 타입(first-class existential types)과 달리 이 방식은 프로그래머가 명시적으로 pack/unpack을 할 필요가 없어요. 시스템이 fresh가 타입 어디에 나타나는지로부터 바인딩 구조를 자동으로 결정해 주거든요.

요약 (Summary)

함수 결과 타입에서 fresh가 나타나면, 결과 타입 위로 스코프를 갖는 수량자가 묶는 새 존재 변수로 치환돼요.
함수 파라미터 타입에 any의 공변적(covariant) 등장이 있으면, 그 등장을 파라미터 타입 위로 스코프를 갖는 새 존재 변수로 치환해요.
함수 결과 타입의 any 등장은 존재 변수로 번역되지 않아요. 이들은 둘러싼 스코프의 로컬 any를 가리키죠. 함수 타입 결과의 그냥 T^도 여기에 포함되는데, T^{any}의 약어니까요.

함수 타입 결과에서의 any vs fresh (any vs fresh in Function Type Results)

위 규칙들은 함수 타입을 쓸 때 중요한 실용적 차이를 만들어요. 이렇게 생각해 봐요:

import language.experimental.captureChecking
import caps.*
import caps.fresh
class A
class B

def test(): Unit =
  val f: (x: A^) -> B^{fresh} = ???  // B^{fresh}: existentially bound
  val g: A^ -> B^             = ???  // B^{any}: enclosing scope's local any

  val _: A^ -> B^        = f   // error: fresh is not in {any}
  val _: A^ -> B^{fresh} = f   // ok
  val _: (x: A^) -> B^{fresh} = g   // error: g* is not in {fresh}
  val _: A^ -> B^        = g   // ok

결과가 B^{any}일 때, 반환된 값의 캡처는 둘러싼 스코프의 로컬 any에 묶여요. g를 두 번 호출하면 같은 캡처 집합 경계를 가진 값이 나오고, 체커는 둘을 동일하게 취급해요. B^{fresh}일 때는 f를 호출할 때마다 구별되는 존재적 캐퍼빌리티를 가진 값이 나와서, 서로 다른 호출의 결과가 별칭(alias)이 아니라는 것을 체커가 증명할 수 있어요.

이 두 타입은 서로 바꿔 쓸 수 없어요. 결과 fresh는 로컬 any로 흘러들어갈 수 없고(존재자는 둘러싼 스코프에서 보이지 않으니까요), 로컬 any도 결과 fresh로 흘러들어갈 수 없어요(fresh는 다른 존재자나 공유 캐퍼빌리티만 하위 캡처할 수 있으니까요).

바깥 경계 fresh (Outer-Bound fresh)

기본적으로 함수 결과 타입의 fresh는 바로 바깥 함수가 묶어요. 하지만 가끔은 fresh를 더 바깥 함수가 묶길 원할 때가 있어요. 타입 별칭이나 캡처 집합 파라미터를 써서 fresh를 안쪽 함수 타입을 통해 "터널링"하면 가능합니다.

이런 타입 정의를 봐요:

import language.experimental.captureChecking
import caps.*
class A
type F[X] = (t: String) -> X

이 별칭을 쓰면 이렇게 작성할 수 있어요:

import language.experimental.captureChecking
import caps.*
class A
type F[X] = (t: String) -> X
import caps.fresh

val x: (s: String) -> F[A^{fresh}] = ???

이 경우 fresh는 안쪽 함수 (t: String) -> ...가 아니라 바깥 함수 (s: String) -> ...가 묶어요. fresh가 안쪽 함수 타입 정의 바깥에 등장하기 때문이에요. 별칭의 타입 인자로 전달됐으니까요. 확장된 타입은 이렇습니다:

x: ∃fresh. (s: String) -> (t: String) -> A^{fresh}

이 기법은 캐퍼빌리티가 중첩된 함수 호출에 걸쳐 걸쳐있어야 하면서도 바깥 스코프에서 존재적으로 묶여 있어야 할 때 유용해요.

파라미터 any와 로컬 any (Parameter anys and Local anys)

함수 본문 안에서 파라미터 any는 함수의 로컬 any와 같은 레벨이에요. 즉 함수의 로컬 any는 파라미터에서 온 캐퍼빌리티들을 하위 캡처할 수 있어요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
def process(x: File^/* parameter {any₁} */): Unit = /* local any₂ */
  val y: File^/*{any₂}*/ = x  // OK: x's any is at process's level, same as process's local any
  val f: () =>/*{any₂}*/ Unit = () => x.read()  // OK: closure's local any subsumes x

파라미터 x는 process의 레벨에 있는 캐퍼빌리티를 가져요. process의 로컬 any(그리고 중첩된 클로저들)는 같은 레벨이거나 더 깊이 중첩되어 있으므로 이를 하위 캡처할 수 있어요.

결과 fresh는 격리된다 (Result freshs are Isolated)

결과 fresh(즉 함수 결과 타입에서 존재적 캡처 집합을 할당받은 것들)는 스코프가 있는 자원이 탈출하게 할 수 있는 캐퍼빌리티는 흡수할 수 없어요. 파일을 캡처한 클로저를 직접 반환해서 파일을 새어나가게 하려는 시도를 생각해 봐요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
def withFile[T](path: String)(block: File^ => T): T = ???
withFile[() => File^]("test.txt"): f =>
//       ^^^^^^^^^^^ T = () => File^, i.e., () ->{any} File^{any} for some outer any
  () => f  // error // error // error: We want to return this as () => File^

람다 (f: File^) => () => f의 추론된 타입은 이렇습니다:

(f: File^) -> () ->{f} File^{f}

안쪽 클로저는 f를 명시적으로 캡처해요. 기대 타입 File^ => () => File^에 맞추려면 다음 단계를 거쳐 넓혀야 해요:

(f: File^) -> () ->{f} File^{f}         // inferred: captures f explicitly
(f: File^) -> () ->{any} File^{any}     // widen to any
(f: File^) -> ∃fresh. () ->{fresh} File^{fresh} // apply existential rule for result `fresh`

마지막 단계는 바깥 함수 타입에 존재적으로 묶인 결과 fresh를 만들어 내요. 그런데 기대 타입 () => File^는 withFile의 둘러싼 스코프, 즉 함수 전체 바깥에 묶인 any를 가지고 있어요. 캡처 체커는 이 존재적으로 묶인 fresh가 바깥 any로 흘러드는 것을 막기 때문에, 이 할당은 실패합니다.

만약 ∃fresh. () ->{fresh} File^{fresh}를 () => File^로 넓히는 것을 허용했다면 스코프가 있는 파일이 탈출할 수 있었을 거예요:

import language.experimental.captureChecking
import caps.*
trait File extends SharedCapability:
  def read(): Unit
  def write(msg: String): Unit

object File:
  def apply(name: String): File^ = ???
def withFile[T](path: String)(block: File^ => T): T = ???
val escaped: () => File^ = withFile[() => File^]("test.txt")(f => () => f) // error // error
//           ^^^^^^^^^^^ any here is in the outer scope
escaped().read()  // Use-after-close!

결과 fresh를 격리된 채로 유지함으로써, 캡처 체커는 존재자가 f를 숨기고 자기 스코프 밖으로 빼돌릴 수 없도록 보장해요.

캐퍼빌리티 탈출을 막는 것 외에도, 결과 fresh를 격리하는 원칙은 변경(mutation)·할당(allocation) 효과와 분리 체킹을 추적하는 데 중요해요. 예를 들어 호출할 때마다 새 가변 참조 셀을 반환하는 함수를 봐요:

import language.experimental.captureChecking
import caps.*
class Cell(init: Int):
  def set(x: Int): Cell^{this} = this
def test(): Unit =
  def freshCell(init: Int): Cell^ = new Cell(init)
  val c1 = freshCell(0).set(42) // Cell^{fresh₁}
  val c2 = freshCell(11)        // Cell^{fresh₂}, fresh₁ and fresh₂ are incomparable

이 경우 자연스러운 타입은 (init: Int) -> Cell^, 즉 위 규칙에 따라 (init: Int) -> ∃fresh.Cell[Int]^{fresh}가 되고, 이는 각 호출이 구별되는 새 Cell 인스턴스를 반환한다는 걸 반영합니다.

Rust의 수명(lifetime)과의 비교 (Comparison with Rust Lifetimes)

Rust에 익숙한 분들은 수명 체킹(lifetime checking)과의 유사점을 알아차리실 거예요. 두 시스템 모두 참조가 유효한 스코프 밖으로 탈출하지 못하게 막아요. Rust에서 참조 타입 &'a T는 명시적인 수명 파라미터 'a를 가져요. Scala의 캡처 체킹에서는 수명이 캐퍼빌리티 이름 자체에 접혀 들어가 있어요. T^{x}는 "x를 캡처하는 T"를 뜻하고, x의 레벨이 이 참조가 유효한 기간을 암묵적으로 결정하죠. 참조의 캡처 집합은 참조 자체의 상한(upper bound) 역할을 해요. 즉 그 안에 들어 있는 모든 캐퍼빌리티가 보이는 동안에만 살아있어요.

익숙한 withFile 패턴을 Rust로 어떻게 표현할 수 있을지 봐요:

struct File;
impl File { fn open(_path: &str) -> Option<File> { Some(File) } }

// Rust: the closure receives a reference bounded by 'a
fn with_file<R>(path: &str, f: impl for<'a> FnOnce(&'a File) -> R) -> R {
    let file = File::open(path).unwrap();
    f(&file)
}

fn main() {
    let f = File;
    let mut escaped: &File = &f;
    with_file("test.txt", |file| {
        escaped = file;  // Error: borrowed value does not live long enough
    });
}

Rust와 Scala 모두 타입 시스템이 핸들이 콜백 밖으로 탈출하는 것을 막아요. Rust는 'a가 클로저의 스코프 안에 포함되도록 요구함으로써 이를 달성하고, Scala는 file의 레벨이(즉 withFile에 묶여 있는) escaped의 레벨(즉 main에 묶여 있는)로 흘러들 수 없음을 확인함으로써 이를 달성해요.

핵심 용어 대응은 이렇습니다:

캐퍼빌리티 이름 ≈ 수명 파라미터: Rust가 &'a T라고 쓰는 곳에 Scala는 T^{x}라고 써요. 캐퍼빌리티 x는 레벨을 통해 수명을 암묵적으로 지니고 있어요.
캡처 집합 ≈ 수명 경계: 캡처 집합 {x, y}는 값의 수명을 그 안에 들어 있는 가장 짧게 사는 캐퍼빌리티보다 길어지지 않게 묶어요.
레벨 포함 관계 ≈ outlives: Rust의 'a: 'b(a가 b보다 오래 산다)는 Scala의 레벨 검사(바깥 스코프가 안쪽 스코프로 흘러들 수 있음)에 대응해요.

핵심 차이는 이렇습니다:

무엇을 추적하는가: Rust는 메모리 유효성을 추적하고(댕글링 포인터를 막음), Scala의 캡처 체킹은 캐퍼빌리티 사용을 추적해서(허가되지 않은 효과를 막음) 둘이 달라요.
명시 vs 암시: Rust의 수명은 명시적 파라미터예요(&'a T). Scala의 레벨은 프로그램 구조로부터 자동으로 계산돼요. 당신은 수명이 아니라 캐퍼빌리티에 이름을 붙이면 되죠.

스코프가 있는 캐퍼빌리티