Scala 3 Capture Checking과 Tracked Capabilities

Scala의 타입 시스템은 프로그램에서 값이 어떤 형태를 가지는지를 상당히 정교하게 표현할 수 있다.

어떤 함수가 String을 받아 Int를 반환하는지, 어떤 타입의 값을 사용할 수 있는지, 어떤 구현이 필요한지를 컴파일 단계에서 확인할 수 있다.

그런데 함수가 무엇을 반환하는지뿐 아니라 그 함수가 실행될 때 무엇에 접근할 수 있는지도 타입으로 표현할 수 있을까.

예를 들어 다음과 같은 함수가 있다고 하자.

def readConfig(fs: FileSystem): String =
  fs.read("config.txt")

이 함수가 파일을 읽기 위해서는 FileSystem이라는 객체가 필요하다.

조금 다르게 보면 fs는 단순한 데이터가 아니라 파일 시스템에 접근할 수 있는 권한을 가지고 있다. fs가 없다면 이 코드는 파일을 읽을 방법이 없다.

이런 객체를 capability라고 볼 수 있다.

Scala 3의 capture checking은 이런 capability에 대한 reference가 프로그램 안에서 어디로 전달되고 어떤 값이나 함수에 포함되는지를 타입 시스템에서 추적하려는 기능이다.

현재 Scala 공식 문서에서도 capture checking은 아직 experimental한 연구 기능으로 분류되어 있다. 하지만 단순한 실험 문법에 그치지 않고 resource management, effect polymorphism, checked exception, 상태를 가진 capability, separation checking 같은 문제를 하나의 타입 시스템 안에서 다루려는 꽤 큰 시도다.

Capability란 무엇인가

Capability라는 말부터 조금 추상적으로 들릴 수 있다.

여기서는 어떤 작업을 수행할 수 있게 해주는 객체나 reference라고 생각하면 된다.

예를 들어 파일 시스템에 접근하는 API가 있다고 하자.

trait FileSystem:
  def read(path: String): String
  def write(path: String, data: String): Unit

어떤 함수가 FileSystem을 전달받지 않았다면 이 API를 사용할 수 없다.

def loadConfig(fs: FileSystem): String =
  fs.read("config.txt")

fs는 파일 시스템에 접근할 수 있는 capability다.

같은 방식으로 network connection이나 database session도 capability로 볼 수 있다.

trait Network:
  def send(data: String): Unit

trait Database:
  def query(sql: String): List[String]

이런 구조의 장점은 권한이 코드 어디에서나 암묵적으로 존재하는 것이 아니라 필요한 곳에 reference 형태로 전달된다는 것이다.

하지만 여기서 한 가지 문제가 생긴다.

Capability를 함수에 전달한 다음 그 reference가 다른 곳으로 빠져나가면 어떻게 될까.

Capture란 무엇인가

Scala에서 closure는 자신이 정의된 바깥 scope의 값을 사용할 수 있다.

val prefix = "LOG"

val printMessage =
  (message: String) => println(s"$prefix: $message")

printMessage 함수의 매개변수는 message 하나뿐이다.

하지만 함수 안에서는 바깥에 있는 prefix도 사용한다.

이런 경우 closure가 prefix를 capture했다고 표현한다.

Capability에서도 같은 일이 생길 수 있다.

def makeReader(fs: FileSystem) =
  () => fs.read("config.txt")

makeReader가 반환하는 함수에는 fs라는 매개변수가 직접 보이지 않는다.

하지만 반환된 closure 안에서는 여전히 fs를 사용하고 있다.

val reader = makeReader(fs)

reader()

즉 reader는 FileSystem capability를 capture하고 있다.

일반적인 Scala 타입만 보면 reader는 단순히 다음과 같은 함수다.

() => String

이 타입만으로는 이 함수가 파일 시스템에 접근한다는 사실을 알 수 없다.

Capture checking이 추가하려는 정보가 바로 이것이다.

Capability가 빠져나가면 어떤 문제가 생길까

Scala 공식 문서에서는 FileOutputStream을 이용한 간단한 예제를 보여준다.

어떤 작업에 파일을 잠시 빌려주고 작업이 끝나면 파일을 닫는 함수를 생각해보자.

def usingLogFile[T](op: FileOutputStream => T): T =
  val logFile = FileOutputStream("log")
  val result = op(logFile)
  logFile.close()
  result

보통은 다음처럼 사용할 수 있다.

usingLogFile { file =>
  file.write(0)
}

file은 함수가 실행되는 동안만 사용되고 작업이 끝나면 닫힌다.

그런데 다음과 같이 사용할 수도 있다.

val later =
  usingLogFile { file =>
    () => file.write(0)
  }

later()

usingLogFile이 끝날 때 logFile은 이미 닫혔다.

하지만 반환된 함수가 file을 capture하고 있기 때문에 나중에 다시 접근하려고 한다.

실행 시점에야 문제가 드러난다.

Capture checking의 목적 중 하나는 이런 문제를 컴파일 단계에서 알아내는 것이다. 공식 문서에서는 FileOutputStream^처럼 capability를 tracked 상태로 선언해서 해당 reference가 허용된 scope 밖으로 빠져나가는지를 검사한다.

`^`는 무엇을 의미할까

Capture checking을 활성화한 코드에서는 다음과 같은 타입을 볼 수 있다.

FileOutputStream^

처음 보면 ^가 새로운 종류의 타입처럼 보이지만, 중요한 것은 이 값이 capability로 추적된다는 의미다.

앞의 예제를 다음처럼 바꿀 수 있다.

def usingLogFile[T](op: FileOutputStream^ => T): T =
  val logFile = FileOutputStream("log")
  val result = op(logFile)
  logFile.close()
  result

이제 compiler는 op에 전달한 FileOutputStream reference가 어디에 capture되는지를 추적한다.

따라서 다음 코드는 문제가 된다.

val later =
  usingLogFile { file =>
    () => file.write(0)
  }

반환되는 함수가 file capability를 가지고 밖으로 빠져나가기 때문이다.

Capture checking을 이해할 때 중요한 점은 ^가 단순히 "위험한 타입"을 표시하는 문법이 아니라는 것이다.

Compiler에게 이 reference의 이동과 capture를 추적하라고 알려주는 역할에 가깝다.

Capture set

Capture checking에서는 어떤 값이 capture하고 있는 capability들의 집합을 capture set이라고 부른다.

개념적으로 다음과 같은 타입을 생각할 수 있다.

T^{c1, c2}

T 타입의 값이 c1, c2라는 capability를 capture하고 있다는 의미다.

예를 들어 어떤 함수가 fs라는 파일 시스템 capability를 사용한다면 개념적으로 다음과 같이 표현할 수 있다.

() ->{fs} String

이 함수는 매개변수를 받지 않고 String을 반환하지만, 내부적으로 fs를 capture하고 있다.

Network까지 함께 사용한다면 capture set은 더 커질 수 있다.

() ->{fs, network} String

일반적인 타입 시스템이

입력 타입 -> 출력 타입

을 표현했다면 capture checking은 여기에

이 computation이 어떤 capability에 의존하는가

라는 정보를 하나 더 붙이는 셈이다.

Scala의 실제 capture checking에서는 capturing type을 T^{...} 형태로 표현하며 capture set 안에는 method parameter, class parameter, local variable, enclosing class의 this 같은 capability reference가 들어갈 수 있다.

Pure function과 capturing function

Capture checking에서는 함수가 외부 capability를 capture하는지 여부도 구분할 수 있다.

Scala 3 capture checking에서는 함수 타입을 표현하는 두 가지 표기가 있다. 일반적으로 익숙한 것은 다음과 같은 형태다.

T => U

그리고 capture checking에서는 외부 capability를 capture하지 않는 pure function을 구분하기 위해 다음과 같은 표기도 사용한다.

T -> U

Scala에서 보통 함수 타입이라고 하면 익숙한 것은 => 쪽이다.

String => Int

String을 받아 Int를 반환하는 일반적인 함수다.

Capture checking이 활성화된 환경에서는 이런 함수가 외부 capability를 capture할 수 있다.

반면

String -> Int

처럼 ->로 표현된 함수는 외부 capability를 capture하지 않는 pure function을 나타낼 수 있다.

예를 들어 다음 함수는 입력값만 사용한다.

val length: String -> Int =
  text => text.length

하지만 다음 함수는 다르다.

val saveLength =
  (text: String) =>
    fs.write("length.txt", text.length.toString)
    text.length

saveLength는 입력값뿐 아니라 바깥의 fs도 사용한다.

즉 fs를 capture하고 있다.

이런 차이를 타입 시스템에서 구분할 수 있게 되면 API를 설계할 때

이 함수에는 외부 capability를 사용하는 computation을 전달해도 된다

또는

이 함수에는 반드시 pure computation만 전달해야 한다

같은 조건을 타입으로 표현할 수 있다.

->를 이용한 pure function syntax 역시 현재 capture checking과 함께 발전하고 있는 experimental 기능이다.

기존 effect system과는 무엇이 다를까

여기까지 보면 capture checking이 effect system과 비슷해 보인다.

실제로 둘은 상당히 가까운 문제를 다룬다.

예를 들어 함수가 파일 시스템을 사용한다면 이를 하나의 effect로 생각할 수 있다.

readConfig
  effect: FileSystem

Network를 사용한다면:

send
  effect: Network

Capture checking에서는 effect를 별도의 이름으로 함수 타입에 붙이는 대신, 그 effect를 수행할 수 있게 해주는 capability reference를 추적한다.

즉

이 함수에는 FileSystem effect가 있다

보다

이 함수는 fs라는 FileSystem capability를 capture하고 있다

에 가까운 접근이다.

이 차이는 capability의 identity가 중요할 때 의미가 있다.

같은 FileSystem 타입이라도 서로 다른 capability를 구분할 수 있기 때문이다.

val userFiles: FileSystem
val systemFiles: FileSystem

둘 다 타입은 FileSystem이지만 같은 권한이라고 볼 필요는 없다.

Capture set은 단순히 FileSystem이라는 effect 이름을 기록하는 것이 아니라 어떤 capability reference를 capture하고 있는지 추적할 수 있다.

그래서 capture checking은 effect tracking과 상당히 밀접하면서도 capability-based security나 resource lifetime 같은 문제까지 함께 다룰 수 있다.

Capture polymorphism

여기서 현실적인 문제가 하나 생긴다.

함수가 어떤 capability를 capture하는지 타입에 모두 직접 적어야 한다면 고차 함수의 타입이 매우 복잡해질 수 있다.

대표적인 예가 map이다.

List(1, 2, 3).map { n =>
  n * 2
}

여기 전달되는 함수는 바깥의 어떤 capability도 사용하지 않는다.

하지만 다음처럼 사용할 수도 있다.

List(1, 2, 3).map { n =>
  logger.log(n.toString)
  n * 2
}

이번에는 map에 전달된 함수가 logger를 capture한다.

그렇다고 List.map을 pure function을 받는 경우와 logger, file system, network 같은 capability를 사용하는 경우마다 따로 정의할 수는 없다. 어떤 함수를 전달하느냐에 따라 가능한 capture set의 조합은 계속 달라질 수 있기 때문이다.

Capture checking은 이런 문제를 capture polymorphism으로 다룬다.

일반적인 List.map의 타입은 여전히 다음과 같은 형태를 유지할 수 있다.

def map[B](f: A => B): List[B]

Capture checking에서 A => B는 어떤 capability든 capture할 수 있는 함수 타입으로 해석된다. 따라서 map은 pure function도 받을 수 있고 logger 같은 capability를 capture하는 함수도 받을 수 있다.

중요한 것은 map이 그 차이를 무시하는 것이 아니라 compiler가 실제로 전달된 함수의 capture를 추적한다는 점이다.

앞의 List처럼 eager collection에서는 f가 map을 실행하는 동안 바로 사용되고 끝난다. 따라서 logger를 capture하는 함수를 전달했다고 해서 반환된 List[B] 자체가 logger를 계속 capture할 필요는 없다.

반면 계산을 나중으로 미루는 lazy collection에서는 이야기가 달라진다. 반환된 collection이 이후에 f를 실행해야 하므로 함수 자체를 가지고 있어야 하고, 그 함수가 capture한 capability도 함께 남을 수 있다.

개념적으로 lazy map은 다음과 같은 관계를 표현할 수 있다.

def map[B](f: A => B): LzyList[B]^{this, f}

반환된 LzyList가 원래 collection인 this와 전달받은 함수 f를 capture하고 있다는 뜻이다. 그리고 f가 logger를 capture하고 있다면 그 관계를 따라 logger 역시 추적될 수 있다.

이런 동작을 Scala 공식 문서에서는 implicit capture polymorphism이라고 부른다.

개발자가 map을 사용할 때마다 capture set을 별도의 타입 매개변수로 적지 않아도 compiler가 실제 함수가 무엇을 capture하는지에 따라 필요한 관계를 추론한다. 이 덕분에 map, filter 같은 일반적인 고차 함수의 형태를 크게 바꾸지 않으면서 capture checking을 적용할 수 있다.

반대로 API에서 capture set 자체를 명시적으로 다뤄야 하는 경우에는 explicit capture polymorphism도 사용할 수 있다. 이 경우에는 일반적인 타입 매개변수와 비슷하게 capture set을 별도의 parameter로 선언한다.

Capture polymorphism이 필요한 이유는 결국 일반적인 polymorphism과 비슷하다.

List[A]가 A의 실제 타입을 미리 알 필요가 없는 것처럼, 고차 함수도 전달받는 함수가 정확히 어떤 capability를 capture할지 미리 고정할 필요가 없다. 대신 compiler가 실제 사용 시점의 capture 정보를 추적한다.

이 덕분에 기존 Scala의 고차 함수와 functional programming 방식은 가능한 한 그대로 유지하면서, 그 안에서 발생하는 capability의 흐름을 타입 시스템이 검사할 수 있다.

eager collection과 lazy collection의 차이

Capture checking이 단순히 "이 함수가 어떤 외부 값을 썼는가"만 검사하는 것은 아니다.

Capability가 언제 사용되는지도 중요할 수 있다.

공식 문서의 예제를 보면 이 차이가 잘 드러난다.

val xs = usingLogFile { f =>
  List(1, 2, 3).map { x =>
    f.write(x)
    x * x
  }
}

List.map은 usingLogFile이 실행되는 동안 계산된다.

따라서 f는 파일이 열려 있는 동안만 사용된다.

반면 lazy collection이라면 상황이 달라진다.

val xs = usingLogFile { f =>
  LazyList(1, 2, 3).map { x =>
    f.write(x)
    x * x
  }
}

LazyList의 실제 계산은 나중에 일어날 수 있다.

그때는 usingLogFile이 이미 끝나 파일이 닫혀 있을 수 있다.

Capture-aware하게 정의된 LazyList라면 compiler는 반환된 값이 f를 capture하고 있다는 사실을 추적하고 이 코드를 거부할 수 있다. 공식 문서가 capture checking의 첫 사례로 resource lifetime을 사용하는 이유가 여기에 있다.

Contextual abstraction과 capability

Scala에서는 using과 given을 통해 dependency를 context parameter로 전달하는 경우가 많다.

trait Database:
  def query(sql: String): List[String]

def loadUsers(using db: Database): List[String] =
  db.query("select * from users")

이 코드에서 Database는 함수에 명시적인 첫 번째 인자로 보이지 않지만 loadUsers가 실행되려면 필요하다.

Capability 역시 이런 방식으로 전달할 수 있다.

이 점에서 Scala의 contextual abstraction과 capability-based programming은 꽤 자연스럽게 연결된다.

기존에는 using을 주로 type class instance나 configuration, execution context 같은 dependency를 전달하는 방식으로 사용했다면, capability 관점에서는

이 computation을 실행할 권한

을 전달하는 방식으로도 볼 수 있다.

예를 들어 특정 예외를 던질 수 있는 권한을 CanThrow capability로 표현하는 checked exception 실험도 이런 방향에 있다. Capture checking은 CanThrow가 scope 밖으로 escape하는지까지 검사할 수 있다.

다만 using을 사용한다고 자동으로 capability가 되는 것은 아니다.

중요한 것은 해당 reference가 tracked capability로 취급되고 compiler가 그 capture를 추적하느냐이다.

Stateful capability

Capability는 파일이나 network처럼 외부 resource에만 해당하는 것은 아니다.

변경 가능한 상태도 capability의 관점에서 볼 수 있다.

어떤 객체를 변경할 수 있다는 것은 그 객체의 상태에 영향을 줄 수 있는 권한을 가지고 있다는 뜻이기 때문이다.

예를 들어 mutable matrix를 생각해보자.

class Matrix:
  def get(i: Int, j: Int): Double = ...
  def set(i: Int, j: Int, value: Double): Unit = ...

Matrix에 대한 reference를 가지고 있다면 데이터를 읽을 수도 있고 수정할 수도 있다.

여기서 또 다른 문제가 생긴다.

같은 mutable object를 여러 reference가 동시에 가리키고 있다면 한쪽에서 값을 변경했을 때 다른 쪽의 가정이 깨질 수 있다.

Capture checking 위에서 이런 aliasing 문제까지 다루려는 기능이 separation checking이다.

Separation checking

다음과 같은 matrix multiplication 함수가 있다고 하자.

def multiply(
  a: Matrix,
  b: Matrix,
  c: Matrix
): Unit

a와 b를 곱해 결과를 c에 저장한다고 생각할 수 있다.

하지만 이 타입만으로는 다음 호출을 막지 못한다.

multiply(a, b, a)

입력 matrix인 a와 출력 matrix가 같은 객체다.

계산 도중 a를 수정하면 아직 계산에 사용해야 할 입력값까지 바뀔 수 있다.

Separation checking은 이런 mutable capability의 aliasing을 타입 시스템에서 제한하려는 기능이다.

Scala 공식 문서의 예제에서는 update 가능한 Matrix와 tracked output capability를 이용해서 입력 a, b와 출력 c가 분리되어 있다는 조건을 검사한다.

def multiply(
  a: Matrix,
  b: Matrix,
  c: Matrix^
): Unit

이 경우 c는 update 가능한 capability로 취급되고, compiler는 a나 b가 c와 같은 mutable capability를 공유하지 않는지 검사할 수 있다.

Separation checking은 capture checking보다도 더 experimental한 단계다. 공식 문서에서도 별도의 experimental import가 필요한 이유를 아직 safety와 expressivity 사이의 균형이 충분히 확립되지 않았기 때문이라고 설명한다.

Capture checking으로 무엇을 표현할 수 있을까

지금까지의 예제를 보면 capture checking이 특정 한 문제를 해결하기 위해 만들어진 기능은 아니라는 것을 알 수 있다.

Resource lifetime에서는 capability가 scope 밖으로 escape하지 못하게 할 수 있다.

usingLogFile { file =>
  ...
}

Effect 관점에서는 computation이 어떤 capability를 사용하는지 추적할 수 있다.

함수 → FileSystem capability capture

Contextual abstraction과 결합하면 어떤 computation을 실행할 수 있는 권한을 전달할 수도 있다.

Mutable state에서는 separation checking으로 aliasing까지 제한하려 한다.

Checked exception도 exception을 던질 수 있는 CanThrow를 capability로 표현할 수 있다.

결국 공통된 아이디어는 비슷하다.

프로그램에서 어떤 작업을 할 수 있게 만드는 권한을 reference로 표현하고, 그 reference가 어디에 capture되고 어디까지 이동할 수 있는지를 compiler가 추적하는 것이다.

AI agent의 Tracked Capabilities도 여기에서 나온다

Capture checking은 AI agent를 위해 만들어진 기능은 아니다.

하지만 최근 Martin Odersky와 EPFL 연구팀은 이 타입 시스템을 AI agent 보안에 적용했다.

아이디어는 비교적 직접적이다.

Agent가 file system과 network capability를 가지고 있다고 하더라도 기밀 데이터를 처리하는 특정 computation에서는 그 capability를 사용할 수 없도록 타입을 제한한다.

예를 들어 다음과 같은 함수 타입을 요구할 수 있다.

T -> U

외부 capability를 capture하지 않는 pure function이다.

기밀 데이터를 Classified[T]로 감싸고 내부 데이터를 변환하는 함수가 T -> U만 받도록 하면, agent가 다음과 같은 코드를 생성하더라도

secret.transform { data =>
  network.send(data)
  data
}

closure가 network capability를 capture하기 때문에 compiler가 거부할 수 있다.

이 접근의 흥미로운 점은 AI가 위험한 코드를 만들지 않기를 기대하는 것이 아니라, 만들어도 타입을 통과하지 못하게 한다는 데 있다.

하지만 이것은 capture checking의 활용 사례 중 하나다.

같은 메커니즘은 AI와 관계없이 resource management, API design, effect tracking, checked exception, mutable state 관리에도 적용할 수 있다.

Safe Mode

Capability를 타입으로 아무리 잘 추적해도 type cast나 reflection 같은 방법으로 그 정보를 없애버릴 수 있다면 보안 용도로 사용하기 어렵다.

Scala는 일반적인 application 개발을 위한 언어이기 때문에 개발자가 type system을 의도적으로 우회할 수 있는 기능들도 가지고 있다.

그래서 capture checking에는 Safe Mode라는 별도의 experimental mode도 있다.

import language.experimental.safe

Safe Mode에서는 unchecked cast와 runtime reflection 같은 일부 escape hatch를 제한하고 capture checking을 강제한다. 또한 mutation effect도 tracking 대상에 포함한다.

이 기능은 일반적인 Scala 프로그램 전체를 항상 이런 방식으로 작성하라는 것이 아니라, agent-generated code처럼 신뢰할 수 없는 코드를 실행하거나 capability safety가 특히 중요한 영역에서 더 강한 제한을 적용하기 위한 것이다.

실제 Scala 프로젝트에서 사용할 수 있을까

현재 시점에서는 capture checking을 일반적인 production Scala 기능처럼 보는 것은 이르다.

Scala 공식 문서에서 capture checking은 여전히 research project이며 highly experimental and unstable하다고 명시하고 있다. 기능과 문법도 빠르게 변하고 있어서 최신 Scala version을 사용하도록 권장한다.

Separation checking은 이보다 더 실험적인 단계다.

따라서 지금 당장 일반적인 Scala application의 모든 effect와 resource를 capture checking으로 모델링하는 것은 현실적인 선택이 아닐 수 있다.

그럼에도 이 기능이 흥미로운 이유는 Scala 타입 시스템이 어디까지 확장될 수 있는지를 보여주기 때문이다.

기존의 타입 시스템이 주로

이 값은 무엇인가

를 표현했다면 capture checking은

이 값은 무엇에 접근할 수 있는가

까지 타입의 일부로 가져오려 한다.

함수의 반환 타입뿐 아니라 그 함수가 어떤 capability를 가지고 있는지, 그 capability가 다른 closure나 객체 안으로 이동하는지, 특정 resource보다 오래 살아남는지를 compiler가 검사한다.

이런 정보가 타입에 들어오기 시작하면 API 설계 방식도 달라질 수 있다.

어떤 resource를 사용할 수 있는지 documentation에만 적는 것이 아니라 타입 자체가 제한할 수 있고, pure한 computation과 capability를 사용하는 computation의 경계도 더 명확하게 만들 수 있다.

타입이 프로그램의 권한까지 표현한다면

Scala는 오래전부터 타입 시스템을 프로그램 설계에 적극적으로 사용하는 언어였다.

Generics나 variance 같은 일반적인 타입 기능뿐 아니라 type class, higher-kinded type, match type, union/intersection type, contextual abstraction 같은 기능을 통해 많은 조건을 compile time으로 가져왔다.

Capture checking은 여기에서 또 다른 방향으로 나아간다.

값의 타입뿐 아니라 값이 가지고 있는 capability와 그 capability의 흐름까지 타입 시스템에서 추적하려는 것이다.

그 과정에서 effect system, resource management, capability-based security, lifetime, aliasing처럼 원래 서로 다른 문제로 보이던 영역이 하나의 메커니즘으로 연결되기 시작한다.

아직 experimental한 기능이고 실제 Scala 개발에서 어느 정도까지 사용될지는 알 수 없다.

문법과 타입 시스템의 복잡성이 더 커진다는 비용도 있다. Capture set이 복잡해질수록 개발자가 compiler의 추론과 error message를 이해해야 하는 부담도 커질 수 있다. 기존 library들이 capture-aware하게 설계되어야 제대로 효과를 볼 수 있는 영역도 있다.

그럼에도 capture checking이 던지는 질문은 흥미롭다.

함수가 무엇을 계산하는지만 타입으로 표현하는 것이 아니라, 그 계산을 하기 위해 무엇에 접근할 수 있는지까지 compiler가 알고 있다면 어떤 프로그램을 만들 수 있을까.

Scala 3의 tracked capabilities는 그 가능성을 실제 타입 시스템 안에서 실험하고 있다.