분리 체킹

분리 체킹 (Separation Checking)

분리 체킹(separation checking)은 캡처 체킹의 확장 기능으로, 캐퍼빌리티에 대한 접근이 유일하고 별칭(alias)이 없도록 강제해요. 이 기능은 언어 import 하나로 켤 수 있어요.

출처: Scala 3 Reference

본문

서론 (Introduction)

분리 체킹은 캐퍼빌리티에 대한 유일하고 별칭이 없는 접근을 강제하는 캡처 체킹의 확장이에요. 이 기능은 다음 언어 import로 켤 수 있어요:

import language.experimental.separationChecking

(또는 대응하는 설정 -language:experimental.separationChecking을 써도 돼요.) 이 import는 캡처 체킹을 켜는 language.experimental.captureChecking import에 더해서 반드시 함께 줘야 해요. 언어 import가 둘인 이유는, 분리 체킹이 본래의 캡처 체킹만큼 성숙하지 않아서 현재 시점에 안전성과 표현력의 균형을 제대로 잡았는지 확신이 덜 서기 때문이에요.

캡처 체킹에서는 any의 각 등장, 즉 ^의 사용마다 캐퍼빌리티의 수명에 묶인 문맥 의존적 의미를 가져요. 분리 체킹은 그 모델을 더 정교하게 만들어요. 각 any가 숨기는 캐퍼빌리티들을 추적하면서, 그 숨은 집합들이 서로 분리되어 있거나 타입이 허용하는 곳에서만 겹치도록 강제하죠.

분리 체킹의 목적은 캐퍼빌리티에 대한 특정 접근이 별칭이 되지 않게 하는 거예요. 행렬 곱셈을 예로 들어 볼게요. Matrix가 Stateful Capabilities에서 설명한 Mutable 타입이고, 요소를 할당하는 setElem이라는 update 메서드가 있다고 해요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Matrix(nrows: Int, ncols: Int) extends Mutable:
  update def setElem(i: Int, j: Int, x: Double): Unit = ???
  def getElem(i: Int, j: Int): Double = ???

행렬 a와 b를 곱해서 c에 넣는 메서드는 이렇게 선언할 수 있겠죠:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Matrix(nrows: Int, ncols: Int) extends Mutable:
  update def setElem(i: Int, j: Int, x: Double): Unit = ???
  def getElem(i: Int, j: Int): Double = ???
def multiply(a: Matrix, b: Matrix, c: Matrix): Unit = ???

하지만 이 시그니처만으로는 어느 행렬이 입력이고 어느 것이 출력인지 알 수 없어요. 입력 행렬이 출력으로 재사용되지 않는다는 보장도 없죠. 그렇게 되면 잘못된 결과가 나올 거예요.

분리 체킹은 multiply의 다음 수정된 시그니처에 특별한 해석을 부여해요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Matrix(nrows: Int, ncols: Int) extends Mutable:
  update def setElem(i: Int, j: Int, x: Double): Unit = ???
  def getElem(i: Int, j: Int): Double = ???
def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit = ???

실제로 단 한 글자만 추가됐어요. c의 타입에 이제 보편 캐퍼빌리티(universal capability)가 붙었죠. 이 시그니처는 한꺼번에 두 가지 바람직한 성질을 강제합니다:

• 행렬 a와 b는 읽기 전용이에요. multiply는 이들의 update 메서드를 호출하지 않아요. 반면 c 행렬은 업데이트될 수 있어요.
• 행렬 a, b는 행렬 c와 달라야 하지만, a와 b는 같은 행렬을 가리킬 수 있어요.

즉, 사실상 업데이트될 수 있는 것은 모두 별칭이 아니어야(unalias) 해요.

분리 체킹 (Separation Checking)

분리 체킹 뒤에 있는 아이디어는 단순해요. 이제부터 any의 각 등장을 별도의 최상위(top) 캐퍼빌리티로 해석한다는 거예요. A^나 B => C 같은 파생 문법도 여기에 포함돼요. 그리고 캡처 체킹을 수행하는 동안 각 any가 어떤 캐퍼빌리티들을 하위 캡처하는지를 계속 추적해요. 캡처 체킹이 어떤 캐퍼빌리티 x를 최상위 캐퍼빌리티 anyᵢ로 넓혔다면, x는 anyᵢ에 의해 **숨겨졌다(hidden)**고 말해요. 규칙은 이렇습니다. 최상위 캐퍼빌리티 anyᵢ에 숨겨진 캐퍼빌리티는, anyᵢ를 볼 수 있는 코드에서 독립적으로 참조되거나 다른 anyⱼ에 숨겨질 수 없어요.

이 검사들은 배타적(exclusive) 캐퍼빌리티와 그 읽기 전용 버전에만 적용돼요. 타입이 SharedCapability를 확장하는 캐퍼빌리티는 면제됩니다.

예를 들어 볼게요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def aliasing(): Unit =
  val y = Ref(1)
  val x: Ref^ = y
  x.get
  y.get // error

이 원칙은 x처럼 기본 캡처 집합으로 any를 가진 캐퍼빌리티가 별칭이 없거나 "fresh"함을 보장해요. 위 코드의 y처럼 기존에 존재하던 별칭들은 x가 보이는 동안에는 접근할 수 없습니다.

이제 이 원칙을 정확하게 다듬어 볼게요.

정의:

캐퍼빌리티 c의 전이 캡처 집합(transitive capture set) tcs(c)는 기본 캡처 집합 C를 가질 때, c 자신에 더해 C의 전이 캡처 집합을 합한 것이에요.

캡처 집합 C의 전이 캡처 집합 tcs(C)는 C의 모든 요소 c에 대한 tcs(c)의 합집합이에요.

두 캡처 집합은, 하나가 배타적 캐퍼빌리티 x를 포함하고 다른 하나도 x를 포함하거나 그 읽기 전용 버전 x.rd를 포함하면 **간섭한다(interfere)**고 해요. 반대로 두 캡처 집합은 그 전이 캡처 집합들이 간섭하지 않으면 **분리되었다(separated)**고 해요.

분리 검사는 다음 시나리오에서 적용됩니다:

애플리케이션 검사 (Checking Applications)

함수 적용 f(e_1, ..., e_n)을 검사할 때, f의 형식 파라미터에 있는 각 any를 fresh한 최상위 캐퍼빌리티로 인스턴스화하고, 인자 타입들을 이렇게 인스턴스화된 파라미터 타입들과 비교해요. 그리고 각 인자 eᵢ에 대해 인스턴스화된 각 최상위 캐퍼빌리티의 숨은 집합이, 다른 모든 인자들의 캡처 집합뿐 아니라 함수 접두부(prefix)와 함수 결과의 캡처 집합과도 분리되어 있는지 확인해요. 예를 들어 다음 호출은

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Matrix(nrows: Int, ncols: Int) extends Mutable:
  update def setElem(i: Int, j: Int, x: Double): Unit = ???
  def getElem(i: Int, j: Int): Double = ???
def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit = ???
def badMultiply(): Unit =
  val a = Matrix(10, 10)
  val b = Matrix(10, 10)
  multiply(a, b, a) // error

거부될 거예요. a가 Matrix^ 타입을 가진 multiply 마지막 파라미터의 숨은 집합에 나타나고, 동시에 첫 번째 파라미터의 캡처 집합에도 나타나니까요.

형식 파라미터의 캡처 집합이 충돌하는 파라미터를 명시적으로 이름 짓고 있다면, 두 집합 사이의 분리 오류는 보고하지 않아요. 예를 들어 두 효과적 함수 인자를 순서대로 적용하는 메서드 seq를 생각해 봐요. 이렇게 선언할 수 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
def seq(f: () => Unit, g: () ->{any, f} Unit): Unit =
  f(); g()

여기서 g 파라미터는 자기 잠재 캡처 집합에 f를 명시적으로 언급해요. 이는 같은 캡처 집합의 any가 첫 번째 인자를 숨길 필요가 없다는 뜻이에요. 이미 같은 집합에 명시적으로 나타나 있으니까요. 결과적으로 분리 기준을 위반하지 않고 같은 함수를 seq에 두 번 넘길 수 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
def seq(f: () => Unit, g: () ->{any, f} Unit): Unit =
  f(); g()
def useSeq(): Unit =
  val r = Ref(1)
  val plusOne = () => r.set(r.get + 1)
  seq(plusOne, plusOne)

seq의 g 파라미터 캡처 집합에서 파라미터 f를 명시적으로 언급하지 않으면 분리 오류가 날 거예요. 두 인자의 전이 캡처 집합이 모두 r을 포함하므로 분리되지 않기 때문이에요.

문장 순서 검사 (Checking Statement Sequences)

캐퍼빌리티 x가 문장 순서 속 어떤 지점에서 사용되면, {x}가 이전 모든 정의들의 숨은 집합과 분리되어 있는지 확인해요.

예시:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
val a: Ref^ = Ref(1)
val b: Ref^ = a
val x = a.get // error

여기 마지막 줄은 분리 기준을 위반해요. a.get에서 캐퍼빌리티 a를 사용하는데, a는 b의 정의에 의해 숨겨져 있기 때문이에요. 참고로 이 검사는 명시적인 최상위 캐퍼빌리티가 관여할 때만 적용돼요. 다음과 같이 작성하는 것도 충분히 가능하죠:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
val a: Ref^ = Ref(1)
val b: Ref^{a} = a
val x = a.get // ok

또한 b의 명시적 타입을 빼고 추론에 맡길 수도 있어요. 그래도 분리 오류가 나지 않아요.

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def inferAlias(): Unit =
  val a: Ref^ = Ref(0)
  val b = a
  val x = a.get // ok

타입 검사 (Checking Types)

타입이 최상위 캐퍼빌리티를 포함하면, 그 숨은 집합들이 같은 타입의 다른 부분과 간섭하지 않는지 확인해요.

예시:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def checkTypes(a: Ref^): Unit =
  val b: (Ref^, Ref^) = (a, a)       // error
  val c: (Ref^, Ref^{a}) = (a, a)    // error
  val d: (Ref^{a}, Ref^{a}) = (a, a) // ok

여기 b의 정의는 오류예요. 타입에 있는 두 ^의 숨은 집합이 모두 a를 포함하기 때문이에요. 마찬가지로 c의 정의도 오류예요. 타입 속 ^의 숨은 집합이 a를 포함하고, a가 타입의 다른 어딘가 캡처 집합의 일부이기도 하니까요. 반면 d의 정의는 합법적이에요. 확인할 숨은 집합이 없으니까요.

반환 타입 검사 (Checking Return Types)

any가 메서드의 반환 타입에 나타나면, 이는 호출 지점에서 알려진 것과는 다른 최상위 캐퍼빌리티를 뜻해요. 분리 체킹은 실제로 그렇게 되도록 보장해요. 예를 들어 다음은 괜찮아요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def newRef(): Ref^ = Ref(1)

이것도 괜찮고요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def newRef(): Ref^ =
  val a = Ref(1)
  a

하지만 다음 정의들은 분리 오류를 일으켜요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def badReturn(): Unit =
  val a = Ref(1)
  def newRef(): Ref^ = a // error

규칙은 이래요. 반환 타입의 any 숨은 집합은 함수 바깥에 정의된 배타적 또는 읽기 전용 캐퍼빌리티를 참조할 수 없어요. 파라미터도 예외가 아니에요. 또 하나의 불법 버전이 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def incr(a: Ref^): Ref^ =
  a.set(a.get + 1)
  a

이건 거부되어야 해요. 그렇지 않으면 다음과 같은 나쁜 예를 쓸 수 있게 되니까요:

val a = Ref(1)
val b: Ref^ = incr(a)

여기서 b는 a의 별칭이지만 a를 숨기지는 않아요. 이후에 a를 참조하면 참조의 값이 2로 바뀌어 있어서 깜짝 놀라게 되죠. 그래서 파라미터는 결과 any의 숨은 집합에도 등장할 수 없어요. 적어도 일반적으로는요. 이 규칙의 예외는 다음 섹션에서 설명합니다.

함수 타입 결과의 fresh (fresh in Function Type Results)

메서드 반환 타입은 any를 쓰는 반면, 함수 타입은 결과 위치에 fresh를 써서 각 호출이 구별되는 캐퍼빌리티를 가진 결과를 낳는다는 것을 표현해요. 스코프가 있는 캐퍼빌리티에서 설명했듯이, 함수 결과의 fresh는 존재적으로 묶여 있어요. () -> Ref^{fresh}는 () -> ∃fresh. Ref^{fresh}를 뜻하죠.

분리 체킹의 관점에서 fresh 결과는 중요해요. 체커가 호출 간에 별칭이 아님을 증명할 수 있게 해 주니까요:

val mkRef: () -> Ref^{fresh} = () => Ref(1)
val a = mkRef()  // Ref^{fresh₁}
val b = mkRef()  // Ref^{fresh₂}

fresh₁과 fresh₂는 구별되는 존재자이므로, a와 b의 캡처 집합은 간섭하지 않아요. 분리되어 있는 거죠. 만약 함수 타입이 결과에 any를 썼다면 이 성질이 성립하지 않아요. 두 결과가 같은 캡처 집합 경계를 공유해서 별칭이 될 수 있으니까요.

같은 숨은 집합 규율도 적용돼요. 결과 fresh의 숨은 집합은 함수 바깥의 캐퍼빌리티를 담을 수 없어요. 예를 들어:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def badFresh(): Unit =
  val a = Ref(1)
  val bad: () => Ref^{fresh} = () => a  // error

여기 a는 클로저에 캡처되어 결과 fresh로 흘러들어가야 해요. 하지만 a가 함수 바깥에서도 보이므로, 이는 freshness 보장을 위반해요. 반환된 Ref가 진짜 새롭고 별칭이 없는 캐퍼빌리티가 아니게 되니까요.

소비 파라미터 (Consume Parameters)

결과 any에 파라미터를 반환하는 것은, 그 파라미터의 실제 인자가 이후에 사용되지 않을 때 안전해요. 파라미터에 consume 수정자를 추가하면 이 패턴을 신호하고 강제할 수 있어요. 이 새로운 소프트 수정자(soft modifier)를 쓰면, 다음 incr 변형이 합법적입니다:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def incr(consume a: Ref^): Ref^ =
  a.set(a.get + 1)
  a

여기서는 참조의 값을 증가시킨 다음 같은 참조를 반환하면서, 원래 참조를 이후에 사용할 수 없다는 조건을 강제하고 있어요. 그러면 다음이 합법적이 됩니다:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def incr(consume a: Ref^): Ref^ =
  a.set(a.get + 1)
  a
def consumeSequence(): Unit =
  val a1 = Ref(1)
  val a2 = incr(a1)
  val a3 = incr(a2)
  println(a3)

각 참조 aᵢ는 incr에 전달된 뒤로는 사용되지 않아요. 하지만 이 순서의 다음 연속은 오류가 됩니다:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Ref(init: Int) extends Mutable:
  private var current = init
  def get: Int = current
  update def set(x: Int): Unit = current = x

object Ref:
  def apply(init: Int): Ref^ = new Ref(init)
def incr(consume a: Ref^): Ref^ =
  a.set(a.get + 1)
  a
def badConsumeSequence(): Unit =
  val a1 = Ref(1)
  val a2 = incr(a1)
  val a3 = incr(a2)
  println(a3)
  val a4 = println(a2) // error
  val a5 = incr(a1)    // error

이 두 할당 모두에서, 이전 애플리케이션의 인자에서 소비된 캐퍼빌리티를 사용하고 있어요.

consume 파라미터는 자원에 대한 선형 접근(linear access)을 강제해요. 이건 매우 유용할 수 있어요. 예를 들어 Scala의 ListBuffer나 ArrayBuffer 같은 버퍼를 생각해 봐요. 선형 접근을 강제할 수 있다면, 이 버퍼들을 마치 순수 함수형인 것처럼 다룰 수 있어요.

예를 들어 요소를 버퍼에 제자리에서 추가하는 함수 linearAdd를, 참조 투명성(referential transparency)을 위반하지 않으면서 정의할 수 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Buffer[T]() extends Mutable:
  private val elems = scala.collection.mutable.ArrayBuffer.empty[T]
  def apply(i: Int): T = elems(i)
  consume def +=(x: T): Buffer[T]^ =
    elems += x
    new Buffer[T]()

object Buffer:
  def apply[T](): Buffer[T]^ = new Buffer[T]()
def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
  buf += elem

linearAdd는 buf에 elem을 추가한 뒤 업데이트된 버퍼를 반환해요. buf를 덮어쓰지만 괜찮아요. buf의 consume 수정자가 호출 후에 인자가 사용되지 않도록 보장하니까요.

소비 파라미터와 읽기 접근 (Consume Parameters and Read Accesses)

consume을 생각하는 좋은 방식은, 전달된 캐퍼빌리티를 호출 이후로 **예약(reserve)**하는 것이라고 보는 거예요. 이전 Buffer 예시에서 이렇게 하면

val buf1 = linearAdd(buf, elem)

배타적 buf 캐퍼빌리티가 예약되므로 더 이상 buf에 접근할 수 없어요. 즉 linearAdd가 elem을 추가함으로써 buf를 안전하게 덮어쓸 수 있다는 뜻이에요.

마찬가지로 읽기 전용 캐퍼빌리티를 consume 파라미터에 넘길 때, 호출 이후로 예약되는 것은 바로 그 캐퍼빌리티뿐이에요. 예를 들어 읽기 전용 버퍼를 소비하는 메서드가 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Buffer[T]() extends Mutable:
  private val elems = scala.collection.mutable.ArrayBuffer.empty[T]
  def apply(i: Int): T = elems(i)
  consume def +=(x: T): Buffer[T]^ =
    elems += x
    new Buffer[T]()

object Buffer:
  def apply[T](): Buffer[T]^ = new Buffer[T]()
def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
  buf += elem
def contents[T](consume buf: Buffer[T]): Int ->{buf.rd} T =
  i => buf(i)

contents 메서드는 읽기 전용 버퍼를 받아서, 각 유효한 인덱스에 대해 그 인덱스의 버퍼 요소를 만들어 주는 함수로 바꿔요. 버퍼를 contents에 넘기는 것은 사실상 버퍼를 얼리는(freeze) 것과 같아요. buf.rd가 예약되므로 호출 지점 이후로는 배타적 buf 캐퍼빌리티를 사용할 수 없고, 그래서 더 이상의 추가(append)는 불가능하죠. 반면 버퍼를 읽는 것은 가능하고, 그 읽기 캐퍼빌리티를 이후 호출에서 다시 소비하는 것도 가능해요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Buffer[T]() extends Mutable:
  private val elems = scala.collection.mutable.ArrayBuffer.empty[T]
  def apply(i: Int): T = elems(i)
  consume def +=(x: T): Buffer[T]^ =
    elems += x
    new Buffer[T]()

object Buffer:
  def apply[T](): Buffer[T]^ = new Buffer[T]()
def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ =
  buf += elem
def contents[T](consume buf: Buffer[T]): Int ->{buf.rd} T =
  i => buf(i)
def repeatedRead(): Unit =
  val buf = Buffer[String]()
  val buf1 = linearAdd(buf, "hi") // buf unavailable from here
  val c1 = contents(buf1)         // only buf.rd is consumed
  val c2 = contents(buf1)         // buf.rd can be consumed repeatedly

참고로 linearAdd와 contents의 유일한 차이는, linearAdd의 consume 파라미터 타입이 Buffer[T]^인 반면 contents의 대응 파라미터 타입은 Buffer[T]라는 점이에요. 첫 번째 타입은 Buffer[T]^{any}로, 두 번째는 Buffer[T]^{any.rd}로 확장됩니다.

소비 메서드 (Consume Methods)

Scala 표준 라이브러리의 버퍼는 linearAdd 같은 두 인자 전역 함수 대신 단일 인자 메서드 +=를 써요. 이 경우 메서드 자체에 consume 수정자를 추가해서 선형성을 강제할 수 있어요.

class Buffer[T] extends Mutable:
  consume def +=(x: T): Buffer[T]^ = this // ok

Mutable 클래스에서 메서드에 붙은 consume은 update를 암시하므로, +=를 따로 update 메서드로 표시할 필요가 없어요. 그러면 이렇게 쓸 수 있어요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
class Buffer[T]() extends Mutable:
  private val elems = scala.collection.mutable.ArrayBuffer.empty[T]
  def apply(i: Int): T = elems(i)
  consume def +=(x: T): Buffer[T]^ =
    elems += x
    new Buffer[T]()

object Buffer:
  def apply[T](): Buffer[T]^ = new Buffer[T]()
def consumeMethods(): Unit =
  val b = Buffer[Int]() += 1 += 2
  val c = b += 3
  // b cannot be used from here

이 코드는 +로 함수형 append 하는 것과 동등하면서, 동시에 인자 버퍼의 저장 공간을 재사용하므로 더 효율적이에요.

freeze 래퍼 (The freeze Wrapper)

배열 같은 가변 데이터 구조를 만들고, 요소들에 할당해서 초기화한 다음, 아무 캐퍼빌리티도 캡처하지 않는 불변 타입으로 배열을 반환하고 싶을 때가 많아요. 이는 freeze 래퍼로 달성할 수 있어요.

예로, Array를 본뜬 클래스 Arr와 그 불변 대응물 IArr를 생각해 봐요:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
import scala.reflect.ClassTag

class Arr[T: ClassTag](len: Int) extends Mutable:
  private val arr: Array[T]^ = new Array[T](len)
  def apply(i: Int): T = arr(i)
  update def update(i: Int, x: T): Unit = arr(i) = x

object Arr:
  def apply[T: ClassTag](len: Int): Arr[T]^ = new Arr[T](len)

type IArr[T] = Arr[T]^{}

freeze 래퍼는 Arr에서 IArr로 안전하게 가게 해 줍니다:

import language.experimental.captureChecking
import language.experimental.separationChecking
import caps.*
import scala.reflect.ClassTag

class Arr[T: ClassTag](len: Int) extends Mutable:
  private val arr: Array[T]^ = new Array[T](len)
  def apply(i: Int): T = arr(i)
  update def update(i: Int, x: T): Unit = arr(i) = x

object Arr:
  def apply[T: ClassTag](len: Int): Arr[T]^ = new Arr[T](len)

type IArr[T] = Arr[T]^{}
import caps.freeze

val f: IArr[String] =
  val a = Arr[String](2)
  a(0) = "hello"
  a(1) = "world"
  freeze(a)

freeze 메서드는 caps에서 이렇게 정의됩니다:

def freeze(consume x: Mutable): x.type = x

임의의 캡처 집합을 가진 Mutable 타입의 값을 소비해요(어떤 캡처 집합이든 암시된 {any.rd}에 일치하니까요). 실제 consume 시그니처는 x.type이 반환된다고 선언하지만, 캡처 체킹 이후의 실제 반환 타입은 특별해요. x.type 대신에, 최상위 캡처 집합이 {}로 매핑된 기본 Mutable 타입이에요. freeze의 적용은 분리 체킹이 활성화된 경우에만 안전합니다.