논문 리뷰: A Programming Paradigm for Spatiotemporal Composability

1. 들어가며

플러그인을 하나 끄면 왜 프로세스 전체를 재시작해야 할까. VSCode에서 확장 하나를 비활성화하려면 확장 호스트 전체를 다시 띄워야 하고, 그 사이에 켜져 있던 다른 확장들의 상태도 전부 날아간다. 이 논문의 저자들이 조사한 바로는 설치 수 상위 100개 확장 중 87개가 실행 코드를 담고 있어서 제거하려면 이런 재시작을 요구한다. 우리가 매일 쓰는 도구가 이 모양인데, 정작 "실행 중에 컴포넌트를 안전하게 넣고 빼는" 문제에는 이렇다 할 형식적 기초가 없다는 것이 저자들의 출발점이다.

정적 조합(static composition), 그러니까 함수 호출, 모듈 임포트, 클래스 상속처럼 컴파일 타임에 결정되어 실행 내내 고정되는 조합은 반세기 넘게 탄탄한 이론을 쌓아왔다. 반면 동적 조합(dynamic composition), 즉 런타임에 컴포넌트를 로드하고 언로드하고 재구성하는 일은 실용적 중요성이 커지는데도 이론이 빈약하다. 플러그인 아키텍처가 그렇고, 요즘 부쩍 주목받는 자기진화형 에이전트 하니스(self-evolving agent harness)가 그렇다. 후자는 스스로 자기 구성요소를 생성하고 배포하면서 동시에 요청을 계속 처리해야 하는데, 이런 자기수정 하나하나가 바로 동적 조합의 사례다.

Peking University와 DeepSeek-AI의 이 논문(Yifan Shi, Wei Zhang, Tianyi Cui)은 동적 조합을 두 개의 직교하는 축으로 분해한다. 하나는 시간적 조합가능성(temporal composability), 컴포넌트를 제거할 때 그것이 환경에 가한 부수효과를 완전히 되돌리는 능력이다. 다른 하나는 공간적 조합가능성(spatial composability), 컴포넌트들이 서로의 의존성을 선언하고 반응적으로 관리하는 능력이다. 그리고 이 두 축을 각각 효과 시스템(effect system)과 코이펙트 시스템(coeffect system)이라는 기존의 형식적 도구를 런타임 메커니즘으로 "들어올려(lift)" 해결한다.

92쪽에 달하는 분량이 말해주듯 이 논문은 가볍지 않다. 모나드와 코모나드, 관측 동치(observational equivalence), 작은 스텝 운영 의미론(small-step operational semantics)과 그 메타이론(보존, 진행, 합류성)까지 정공법으로 밀어붙인다. 그러면서도 Cordis라는 실제 TypeScript 메타프레임워크로 구현하고, 4000개가 넘는 커뮤니티 플러그인을 가진 Koishi 챗봇 프레임워크로 검증까지 한다. 이론과 시스템 사이를 성실히 오가는 보기 드문 논문이라, 이 리뷰에서는 형식화의 뼈대를 최대한 직관과 함께 따라가 보려 한다.

한 가지 먼저 밝혀둘 것이 있다. 이 논문은 실험 벤치마크나 Ablation 표가 있는 종류의 ML 논문이 아니다. 핵심 산출물은 정의와 정리, 그리고 그 정리들이 하나의 계산 체계(calculus) 안에서 맞물리는 방식이다. 그래서 이 리뷰도 수치 비교표 대신 "왜 이 정의가 이렇게 생겼는가"를 쫓아가는 구조가 된다.

---

2. 문제 정의: 조합가능성의 두 차원

저자들은 조합가능성을 잘 연구된 대수적(algebraic) 측면 너머에서 두 차원으로 나눈다.

시간적 조합가능성은 시간 축을 다룬다. 컴포넌트를 제거하면 그것이 공유 환경에 가한 수정이 완전하고 안전하게 되돌아가야 한다. 이를 위해서는 컴포넌트가 수행한 모든 자원 할당, 이벤트 등록, 상태 변경을 추적하고, 제거 시 이들을 질서 있게 회수해야 한다.

공간적 조합가능성은 공간 축을 다룬다. 컴포넌트들이 서로에 대한 의존성을 구조적이고 검증 가능한 방식으로 선언하고, 발견하고, 해소할 수 있어야 한다. 의존성 위상(topology)을 관리하고, 의존성 변화에 반응해 컴포넌트 생명주기를 조율해야 한다.

정적 세계에서 이 둘은 각각 쉬운 문제로 환원된다. 시간적 조합가능성은 렉시컬 스코핑(RAII, bracket 패턴)으로, 공간적 조합가능성은 모듈 임포트 해소로 처리된다. 문제는 동적 세계다. 런타임에 컴포넌트가 도착하고 떠나는 상황에서 두 차원 모두 훨씬 어려워진다. 시간적 측면에서는 스코프가 렉시컬하게 묶이지 않는, 오래 살아남는 상태를 가진 효과를 다뤄야 한다. 공간적 측면에서는 실행 도중 나타나고 사라지고 정체성이 바뀌는 의존성을 다뤄야 한다.

2.1 왜 기존 방법으로는 부족한가

논문은 VSCode를 대표 사례로 삼아 두 한계를 짚는다. 시간적 한계로, 확장 호스트는 개별 확장의 코드를 런타임에 언로드할 메커니즘을 제공하지 않는다. deactivate 훅이 있긴 하지만 호스트 종료 시의 우아한 셧다운 콜백일 뿐 라이브 제거를 지원하지 않고, 무엇보다 효과 해제(disposal)를 효과 생성(activate)과 분리시켜 관심사의 지역성(locality of concern)을 깨뜨린다. 공간적 한계로, extensionDependencies가 있긴 하나 상위 100개 확장 중 비내장 확장에 의존을 선언한 것은 단 7개뿐이다. 게다가 확장 간 상호작용은 getExtension(...).exports를 통하는데 반환값이 타입이 없어(any) 검증된 인터페이스를 신뢰할 수 없다.

또 하나 흥미로운 지적은 "굵은 입자(coarse-grained) 우회책"이다. 운영체제는 프로세스 단위로 시간적 조합가능성을, 컨테이너 오케스트레이터(쿠버네티스류)는 서비스 단위로 공간적 조합가능성을 이미 제공한다. 그래서 대부분의 소프트웨어는 오작동하는 모듈을 프로세스 재시작으로, 서비스 의존성을 오케스트레이터로 때운다. 하지만 이 우회는 비싸다. 재시작할 때마다 캐시, 커넥션, 부분 계산 같은 프로세스 로컬 상태가 전부 버려지고 이를 재구축하는 데 수 초에서 수 분이 든다. 그동안 가용성을 유지하려면 중복 복제본을 둬야 한다. 컨테이너 수준 오케스트레이션은 같은 주소 공간을 공유하는 컴포넌트 간 의존성을 표현하지 못하고, 로컬 함수 호출로 될 일에 네트워크 오버헤드를 얹는다. 문제의 본질은 **입자도 불일치(granularity mismatch)**다. 현대 시스템은 프로세스/컨테이너 경계보다 더 잘게 조합하는데, 회복과 의존성 관리는 그 경계에서만 제공된다.

이 지점에서 논문의 관점 전환이 나온다. 정적 타입 시스템에 주석을 더 붙이는 대신, 효과와 코이펙트의 개념적 구조를 **런타임이 직접 다룰 수 있도록 사물화(reify)**하자는 것이다. 정적으로 보장하던 것을 동적으로 확립하자는 발상이다.

---

3. 배경: 효과와 코이펙트

본론에 들어가기 전에 두 이론적 기둥을 짚어야 한다. 논문 2절이 이 배경을 정리한다.

**효과(effect)**는 타입을 정련한다. 단순 타입 람다 계산(STLC)의 판단 $\Gamma \vdash t : T$는 항 $t$가 문맥 $\Gamma$ 아래에서 타입 $T$를 가진다고 말한다. 효과 시스템은 결과 타입에 효과 대수(effect algebra)의 원소를 붙여 어떤 부수효과가 생길 수 있는지 기술한다.

$$\Gamma \vdash t : T\,\texttt{effect}$$

Moggi가 모나드로 계산 효과를 범주론적으로 모델링했고, Plotkin과 Power의 대수적 효과(algebraic effect)는 효과 인터페이스를 구현으로부터 분리했다. 효과 핸들러는 연산을 지연 연속(delimited continuation)으로 해석한다. Koka, Eff, OCaml 5 등이 이 계열이다.

**코이펙트(coeffect)**는 쌍대적으로 타입 대신 문맥을 정련한다.

$$\Gamma\,\texttt{coeffect} \vdash t : T$$

여기서 문맥에 코이펙트 대수의 원소가 붙어, 계산이 환경으로부터 무엇을 요구하는지를 기술한다. 접근할 자원, 보유할 권한, 의존할 서비스 같은 것이다. 효과가 "프로그램이 세계에 미치는 영향"을 모델링한다면, 코이펙트는 "세계가 프로그램에 거는 제약"을 모델링한다. 코모나드로 구조화하거나, 사전순서 반환(pre-ordered semiring)을 코이펙트 대수로 쓰는 등급 코이펙트(graded coeffect)가 있다.

두 시스템은 계산에 대한 추론을 상보적인 두 방향으로 조직한다. 효과는 계산이 환경을 어떻게 수정하는가, 코이펙트는 계산이 환경에 어떻게 의존하는가를 다룬다. 이것이 정확히 1절의 두 차원과 대응한다. 시간적 조합가능성은 상태를 바꾸는 효과가 역(inverse)을 가지길 요구하고, 공간적 조합가능성은 코이펙트가 포착하는 의존성을 반응적으로 관리하길 요구한다. 문제는 고전적 효과/코이펙트 시스템이 정적 도구라는 점이다. 효과는 렉시컬하게 고정된 스코프 안에서 추적되고 컴파일 타임 핸들러로 해소되며, 코이펙트 주석은 실행 전에 결정된 문맥에 대해 검증된다. 배포 후 로드된 플러그인을 렉시컬 스코프가 감쌀 수 없고, 런타임 구성에서 생겨나는 의존성을 컴파일 타임 문맥이 예상할 수 없다.

---

4. 되돌릴 수 있는 효과 (Revertible Effects)

논문 3절이 핵심 이론의 심장부다. 여기서 효과와 코이펙트를 런타임 메커니즘으로 들어올린다. 중심 아이디어는 효과와 코이펙트를 나르는 타입 문맥(typing context)을 문맥 타입(context type), 즉 런타임에 조작 가능한 일급 타입으로 바꾸는 것이다.

4.1 효과 문맥 $\partial\Gamma$

시간적 조합가능성이란 런타임에 컴포넌트를 로드/언로드해서 언로드 시 공유 환경이 조합 이전 상태로 회복되는 능력이다. 이를 위해 컴포넌트가 환경에 가한 모든 수정이 추적 가능하고 회복 가능해야 한다. 저자들은 효과를 타입 $\Gamma \to \Gamma \times (\Gamma \to \Gamma)$의 함수로 모델링한다. 현재 문맥에 적용하면 수정된 문맥과 함께 명시적 역함수를 내놓는다는 뜻이다. 이 역함수를 공급하는 것이 효과를 되돌릴 수 있게(revertible) 만들고, 이를 런타임에 반환하는 것이 효과를 추적 가능하게 만든다.

임의의 불순 함수 $f : X \rightsquigarrow Y$를 순수한 형태 $\bar f : \Gamma \times X \to \Gamma \times Y$로 변환하면, 모든 부수효과는 $\Gamma$ 위의 변환으로 표현된다. 고정된 입력 $x$에 대해 유도되는 사상 $\gamma \mapsto \mathrm{pr}_1(\bar f(\gamma, x)) : \Gamma \to \Gamma$가 반환값과 무관하게 $f$의 부수효과를 포착한다. 그래서 $\Gamma$ 위의 효과는 합성 $\circ$ 아래 변환 모노이드 $\Gamma \to \Gamma$에 산다. 모노이드 공리 하나하나가 효과의 성질로 읽힌다. 닫힘성은 "효과의 순차 합성도 효과", 결합성은 "합성 효과가 괄호 묶는 방식과 무관", 항등원 $\mathrm{id}_\Gamma$는 합성의 단위다.

되돌림을 모델링하기 위해 각 변환 $f$를 그것을 되돌리는 $g$와 짝짓는다. 여기서 $g$는 $f$의 **왼쪽 역(left inverse)**이다. 되돌림은 한쪽 방향이다. 역이 붙는 대상은 $g \circ f$이지 $f \circ g$가 아니다. 이 쌍들은 자기만의 곱을 가진다.

$$(f_1, g_1) \circ (f_2, g_2) := (f_1 \circ f_2,\ g_2 \circ g_1)$$

이것을 **뒤틀린 합성(twisted composition)**이라 부른다. 왼쪽 피연산자가 나중에 작용하고 역들은 반대 순서로 쌓인다. 이렇게 $(\Gamma \to \Gamma) \times (\Gamma \to \Gamma)$가 단위 $(\mathrm{id}_\Gamma, \mathrm{id}_\Gamma)$를 가진 모노이드 $\mathfrak{T}_\Gamma$가 된다.

이제 효과를 문맥 자체 안에서 추적하기 위해 효과 문맥을 정의한다.

$$\partial\Gamma := \Gamma \times (\Gamma \to \Gamma)$$

쌍 $(\gamma, \varphi)$로 이해하면, $\gamma$는 현재 문맥 상태이고 $\varphi$는 **누적기(accumulator)**로 지금까지 수행한 효과들의 역의 합성, 즉 문맥을 초기 상태로 되돌리는 함수다. 초기 효과 문맥은 $(\gamma_0, \mathrm{id}_\Gamma)$로 표현된다. 여기서 $\partial$을 반복 적용하면 $\Gamma, \partial\Gamma, \partial^2\Gamma, \cdots$의 탑(tower)이 생긴다. 이 자기유사(self-similar) 구조가 나중에 계층적 조합의 열쇠가 된다.

추적과 회복의 구체적 구성이 두 변환으로 주어진다.

$$\mathrm{track}_\Gamma(f, g) = (\gamma, \varphi) \mapsto (f(\gamma),\ \varphi \circ g)$$

전방 함수 $f$와 후보 역 $g$를 받아 $\partial\Gamma$의 변환으로 바꾼다. 상태 $\gamma$를 $f$로 변환하고, 역 $g$를 누적기 $\varphi$에 합성해 넣는다. 논문은 여기서 두 정리를 증명한다. Theorem 4는 추적이 전방 행동을 건드리지 않음($\mathrm{pr}_1 \circ f' = f \circ \mathrm{pr}_1$)을 보이고, Theorem 5는 $\mathrm{track}_\Gamma$가 $\mathfrak{T}_\Gamma$에서 $\partial\Gamma \to \partial\Gamma$로 가는 모노이드 준동형임을 보인다. 준동형이라는 사실이 중요한데, 효과를 하나씩 추적하는 것과 뒤틀린 합성으로 한꺼번에 추적하는 것이 일치한다는 뜻이라, 추적된 효과의 열을 단일 추적 효과처럼 다룰 수 있게 해준다.

회복은 이렇게 정의된다.

$$\mathrm{recover}_\Gamma = (\gamma, \varphi) \mapsto (\varphi(\gamma),\ \mathrm{id}_\Gamma)$$

누적기 $\varphi$를 현재 상태 $\gamma$에 적용하고 $\varphi$를 항등으로 리셋한다. Theorem 7이 이 대목의 핵심 불변식을 준다. 추적된 효과가 자기 역으로 되돌려지면 회복 결과가 움직이지 않는다는 것이다. 회복은 $\varphi(\gamma)$라는 양을 통해서만 상태를 읽으므로, 이 보장은 $\varphi(\gamma)$의 보존과 같다. 저자들은 $\varphi(\gamma) = \gamma_0$을 상태의 **건전성 불변식(soundness invariant)**이라 부른다. 초기 효과 문맥에서 시작해 자기 역으로 되돌려지는 효과만 밟으면 모든 상태가 이 불변식을 만족하고, 회복은 각 상태를 $(\gamma_0, \mathrm{id}_\Gamma)$로 데려간다.

4.2 효과 함수 $\mathfrak{E}_\Gamma$

track/recover 모델에는 두 한계가 있다. 첫째, $\mathrm{track}_\Gamma(f, g)$가 상태를 보기 전에 $g$를 고정하므로, 하나의 균일한 $g$가 모든 적용 상태에서 Theorem 7의 가설을 만족해야 한다. 하지만 되돌림에 필요한 것은 덜하다. $f$가 적용된 그 상태에서의 역만 있으면 되고, 이건 상태마다 다를 수 있다. 둘째, $\mathrm{recover}_\Gamma$는 전부 아니면 전무(all-or-nothing)라 하나의 효과만 선택적으로 되돌릴 수 없다.

이를 입력과 출력 양쪽에서 개선한다. 입력 측에서는 $\Gamma$를 변환하면서 역함수도 함께 반환한다($\Gamma \to \partial\Gamma$). 출력 측에서는 $\partial\Gamma$를 변환하면서 역함수를 함께 반환한다($\partial\Gamma \to \partial^2\Gamma$). 두 변경이 입력과 출력에 같은 모양, 즉 "문맥에서 변환된 문맥과 역의 쌍으로 가는 사상"을 준다. 그래서 하나의 타입족이 두 수준을 모두 덮는다. 이것이 효과 함수 타입 $\mathfrak{E}_\Gamma$이고, 증인(witness)으로 정련한 것이 $\mathfrak{E}_\Gamma^*$다.

$$\mathfrak{E}_\Gamma := \Gamma \to \Gamma \times (\Gamma \to \Gamma)$$ $$\mathfrak{E}_\Gamma^* := (e : \Gamma \to \Gamma \times (\Gamma \to \Gamma)) \times \big((\gamma)(\delta)(g) \to ((\delta, g) = e(\gamma) \to g(\delta) = \gamma)\big)$$

$e(\gamma)$가 쌍 $(\delta, g)$를 내놓는데 $\delta$는 새 문맥, $g$는 현재 효과의 역함수다. 증인은 반환된 각 역을 딱 하나의 방정식 $g(\delta) = \gamma$에 묶는다. 역은 효과가 적용된 그 상태에서만 되돌리면 된다는 것이다. 그래서 $\mathfrak{E}_\Gamma^*$의 원소는 상태마다 다른 역을 고를 수 있다.

효과 함수들은 더 이상 자기사상(endomorphism)이 아니라 직접 합성할 수 없으므로 새 연산을 정의한다.

$$f \diamond g = \gamma \mapsto \mathbf{let}\ (\delta, s) = g(\gamma)\ \mathbf{in}\ \mathbf{let}\ (\varepsilon, t) = f(\delta)\ \mathbf{in}\ (\varepsilon,\ s \circ t)$$

Theorem 10은 이 효과 합성 $\diamond$가 $\mathfrak{T}_\Gamma$의 모노이드 구조를 $\mathfrak{E}_\Gamma$로 옮기며 단위가 $\eta_\Gamma := \gamma \mapsto (\gamma, \mathrm{id}_\Gamma)$임을, Theorem 11은 증인이 효과 합성에서 살아남아 $\mathfrak{E}_\Gamma^*$가 부분모노이드임을 보인다. 그리고 track이 변환 쌍을 $\partial\Gamma$로 들어올렸듯, $\mathrm{effect}_\Gamma$가 $\mathfrak{E}_\Gamma$를 $\mathfrak{E}_{\partial\Gamma}$로 들어올린다.

$$\mathrm{effect}_\Gamma(e) = (\gamma, \varphi) \mapsto \mathbf{let}\ (\delta, g) = e(\gamma)\ \mathbf{in}\ \big((\delta, \varphi \circ g),\ \mathrm{track}_\Gamma(g,\ \mathrm{pr}_1 \circ e)\big)$$

여기 담긴 통찰이 우아하다. 효과를 되돌리는 일 자체가 하나의 효과라는 것이다. 효과의 역은 상태를 $g$로 변환하고, 그것을 되돌리는 방법은 효과를 다시 수행하는 것($\mathrm{pr}_1 \circ e$)이다. 그래서 역이 track이 규정하는 그대로 누적기에 합성된다. 다음 두 그림이 이 관계를 시각화한다.

원논문 Section 3.1.2의 가환 다이어그램: 효과 함수 $e : \Gamma \to \partial\Gamma$가 반환하는 역 $g$가 $e$가 적용된 그 상태에서 변환 $f$를 되돌린다는 조건. $\mathrm{pr}_1, \mathrm{pr}_2$는 각각 새 상태와 역을 뽑아낸다.

이 다이어그램은 효과 함수 $e$의 증인 조건을 그림으로 옮긴 것이다. 위쪽 삼각형($\Gamma$에서 $\Gamma$로 가는 $f$와 $g$)이 되돌림 관계를 나타내고, 아래쪽으로 $e$가 $\partial\Gamma$로 내려가며 $\mathrm{pr}_1$을 통해 $f$와, $\mathrm{pr}_2$를 통해 $g$와 연결된다. 핵심은 $g$가 임의 상태가 아니라 $e$가 실제로 적용된 상태에서만 되돌리면 된다는 국소성이다.

원논문 Section 3.1.2의 두 번째 가환 다이어그램: $\mathrm{effect}_\Gamma$가 $e : \Gamma \to \partial\Gamma$를 $e' : \partial\Gamma \to \partial^2\Gamma$로 들어올릴 때 두 수준이 $\mathrm{pr}_1$을 통해 어떻게 대응하는지. 위 삼각형은 $e$의 증인 조건, 아래 삼각형은 $e'$이 같은 방식으로 증인 조건을 만족하는지의 물음이다.

이 두 번째 그림은 $\partial$-탑의 두 수준을 잇는다. $\mathrm{effect}_\Gamma$로 들어올린 $e'$이 원래 $e$와 $\mathrm{pr}_1$을 통해 대응하고(Theorem 14), 들어올린 역 $g'$도 원래 역 $g$와 $\mathrm{pr}_1 \circ g' = g \circ \mathrm{pr}_1$로 대응한다. Theorem 15는 들어올린 역이 상태를 정확히 회복하고 $g'(\Delta) = (\gamma, \varphi \circ g \circ f)$임을 계산으로 보여준다. 흥미로운 비대칭이 있는데, 상태는 정확히 회복되지만 누적기까지 복원되어 $\mathrm{effect}_\Gamma(e) \in \mathfrak{E}_{\partial\Gamma}^*$가 되는 것은 $g \circ f = \mathrm{id}_\Gamma$일 때뿐이다. 즉 $\mathrm{effect}_\Gamma$는 $\mathfrak{E}_\Gamma^*$를 $\mathfrak{E}_{\partial\Gamma}^*$로 그대로 옮기지 않는다. 그럼에도 회복 대상 $\varphi(\gamma)$는 언제나 보존되므로 실무상 필요한 보장은 유지된다. 이 미묘함이 나중에 관측 동치로 수식을 다시 읽는 동기가 된다.

4.3 효과 이터레이터 $\mathfrak{I}_\Gamma$

컴포넌트가 로드하는 것은 효과 하나가 아니라 효과의 **열(sequence)**이고, 언로드가 되돌리는 것은 그 열 전체다. Theorem 16은 효과를 적용의 역순으로 되돌리면 각 역이 자기 적용이 만든 상태를 정확히 만난다는, 어찌 보면 당연하지만 형식적으로 확립해야 할 사실을 보인다. LIFO 되돌림이 여기서 자연스럽게 나온다.

이 열을 사물화한 것이 효과 이터레이터다.

$$\mathfrak{I}_\Gamma := \mu\mathfrak{I}.\ \Gamma \to \Gamma \times (\Gamma \to \Gamma) \times \mathsf{Maybe}(\mathfrak{I})$$

$e(\gamma)$가 삼중항 $(\delta, g, o)$를 내놓는데, $\delta$는 새 문맥, $g$는 현재 효과의 역, $o$는 연속(continuation)이다. $o$가 $\mathsf{Nothing}$이면 반복 종료, $\mathsf{Just}(i)$면 다음 반복이다. $\mathrm{effect}_\Gamma$를 이 이터레이터 구조로 재귀적으로 확장한 $\mathrm{effect}^{\mathrm{iter}}_\Gamma$가 각 반복마다 역 $g$를 적용 순서로 $\varphi$에 합성하므로, 누적기 $\varphi \circ g_1 \circ \cdots \circ g_k$가 효과를 LIFO 순으로 되돌린다.

저자들이 짚는 대응이 실무적으로 반갑다. $\mathsf{Maybe}(\mathfrak{I})$ 연속은 연속된 두 반복 사이에 경계를 만드는데, 이것이 사물화된 지연 연속(delimited continuation)이며 주류 언어가 yield 연산자로 노출하는 바로 그 구조다. 즉 이 모델이 언어가 이미 제공하는 제너레이터에 직접 매핑된다. 평범한 효과 함수는 첫 반복에서 곧장 $\mathsf{Nothing}$을 내놓는 퇴화 사례로 들어온다.

이 구성들이 모여 되돌릴 수 있는 효과가 된다. 각 효과 함수가 자기 역을 명시적으로 제공하고, $\mathrm{effect}$가 $\partial\Gamma$ 위에서 추적하고, $\diamond$가 되돌림을 보존하며 합성한다. 이것이 주는 것은 국소적 시간적 조합가능성이다. 국소적이라는 말은 보장이 한 컴포넌트의 효과만 떼어서 읽힌다는 뜻이다. 컴포넌트를 로드하는 것은 이터레이터 하나를 돌리며 그 역들을 $\varphi$에 누적하는 일이고, 언로드는 $\varphi$를 적용하는 일이다. 이 기준이 빠뜨리는 두 가지가 있는데, 누적기가 강요하는 순서를 벗어나 되돌리는 것과 다른 컴포넌트의 효과가 끼어드는 열이다. 둘 다 나중에 독립성(independence) 조건으로 공급된다.

---

5. 반응적 코이펙트 (Reactive Coeffects)

5.1 코이펙트 문맥 $\Sigma$

공간적 조합가능성은 컴포넌트들이 서로에 대한 의존성을 선언하고, 시스템이 런타임에 그 의존성을 해소, 제공, 철회하는 능력이다. 이를 위해 공유 문맥이 바뀔 때마다 의존성 충족 여부를 재평가해서, 컴포넌트가 의존성이 갖춰지면 활성화하고 철회되면 비활성화해야 한다. 저자들은 컴포넌트의 의존성을 명세(specification)로 모델링하고, 문맥의 각 변화를 그 명세에 대해 활성화/비활성화/중립으로 분류한다.

전통적 제어 역전(IoC) 컨테이너가 의존성을 단순 키-값 매핑으로 다룬다면, 이 논문은 IoC를 코이펙트 문맥으로 형식화한다.

$$\Sigma := (k : K) \rightharpoonup \mathcal{V}_k$$

$\sigma : \Sigma$는 각 $k \in \mathrm{dom}(\sigma)$에 타입 $\mathcal{V}_k$의 값을 배정하는 유한 부분함수다. 타입족 $\mathcal{V}$를 씀으로써 각 의존성 키가 특정 값 타입과 결부되어 정적 타입 안전성을 얻는다. 핵심 연산은 get과 set이다.

$$\mathrm{set}(k, v) = \sigma \mapsto (\sigma[k \mapsto v],\ \lambda\sigma'.\,\sigma' \setminus k)$$

여기 결정적인 관찰이 있다. $\mathrm{set}(k, v)$는 타입 $\mathfrak{E}_\Sigma^*$, 즉 코이펙트 문맥 위의 효과 함수다. 그래서 3.1절의 효과 기계를 그대로 적용할 수 있다. $\mathrm{effect}_\Sigma$가 의존성 등록의 자동 추적과 회복을 제공한다. 이것이 반응적 코이펙트와 되돌릴 수 있는 효과 사이의 시너지다. 코이펙트 연산이 곧 효과이고, 효과는 되돌릴 수 있다. 이 한 문장이 논문 전체를 관통하는 통합 원리라 볼 수 있다.

5.2 명세와 통지

없는 의존성에 접근하는 것은 런타임 실패다. 그래서 컴포넌트는 자기가 선언한 의존성이 모두 갖춰졌을 때만 활성화해야 한다. 코이펙트 명세 $d \subseteq K$에 대해 충족 술어를 정의한다.

$$\sigma \models d := \forall k \in d.\ k \in \mathrm{dom}(\sigma)$$

$\mathrm{dom}(\sigma)$가 유한하므로 결정 가능하다. 그리고 모든 $\sigma$의 변경이 효과 함수(그 역이 이전 도메인을 회복하는)를 거치므로, 충족 여부의 변화가 각 효과 경계에서 탐지 가능하다. 저자들은 이를 "반응성의 대수적 기초"라 부른다. 효과 시스템이 모든 코이펙트 변화가 관측됨을 보장한다는 것이다. 명세 $\mathfrak{D}_\Sigma := \mathsf{Set}(K)$가 컴포넌트가 선언하는 의존성 집합이고, 상태 전이의 분류가 이 명세를 반응적으로 만든다.

$$\mathrm{notify}_d(\sigma, \sigma') := \begin{cases} \text{activating} & \sigma \not\models d \land \sigma' \models d \\ \text{deactivating} & \sigma \models d \land \sigma' \not\models d \\ \text{neutral} & \text{otherwise} \end{cases}$$

활성화 전이는 컴포넌트의 효과 실행을 촉발하고, 비활성화 전이는 누적기 적용에 의한 회복을 촉발한다. set과 notify가 함께 주는 것이 국소적 공간적 조합가능성이다. 컴포넌트는 명세를 만족하는 상태에서만 활성화하므로 없는 바인딩을 읽지 않고, 문맥의 모든 변화가 명세에 대해 분류되므로 충족 상실이 그것이 일어난 곳에서 탐지되어 비활성화를 몰아간다.

5.3 격리와 가로채기

기본 $\Sigma$는 평평한 의존성 테이블이다. 실무에서는 같은 논리적 의존성에 서로 다른 값을 바인딩해야 할 때가 있다. 논문은 두 메커니즘을 더한다. **코이펙트 격리(isolation)**는 같은 키가 서로 다른 문맥에서 다르게 해소되게 하고, **코이펙트 가로채기(interception)**는 의존성 접근에 교차관심사(cross-cutting) 행동을 붙인다.

두 메커니즘은 get/set과 작용 대상이 다르다. 제공(provision)은 모든 컴포넌트가 읽는 공유 테이블에 쓰므로 효과이고 역을 나른다. 격리와 가로채기는 대신 한 문맥 아래 컴포넌트들에 대해 키가 어떻게 해소되는지를 조정하고 테이블 자체는 그대로 둔다. 여기서 Definition 23의 구분이 나오는데, 효과 함수는 두 가지 실현(realization)을 허용한다. **제자리 실현(in-place)**은 문맥을 변경하고 비자명한 역을 반환한다. **파생 실현(derived)**은 입력을 그대로 두고 그로부터 파생된 새 문맥을 반환하며 역은 항등이라, 회복은 파생 문맥을 그냥 버리면 된다. 격리와 가로채기는 파생 실현을 받는다.

격리 문맥은 $\Sigma^{\mathrm{iso}} := (K \rightharpoonup R) \times ((r : R) \rightharpoonup \mathcal{V}_r)$로, 격리 영역 테이블 $\rho$와 의존성 테이블 $\sigma$의 쌍이다. 키 $k$ 접근 시 먼저 $\rho(k)$로 영역 식별자 $r$을 해소하고 $\sigma(r)$로 실제 값을 얻는 2층 매핑이다. 저자들은 이것이 본질적으로 런타임 애드혹 다형성(ad-hoc polymorphism) 시스템이라 정확히 짚는다. 같은 키가 문맥에 따라 완전히 다른 값으로 해소되고, 이 다형성을 런타임에 동적으로 조정할 수 있다. 멀티테넌트 시스템, 테스트 환경, 컴포넌트 샌드박스에 응용된다.

가로채기 문맥은 $\Sigma^{\mathrm{inter}} := ((k : K) \to \mathcal{M}_k) \times ((k : K) \rightharpoonup (\mathcal{M}_k \to \mathcal{V}_k))$로, 문맥이 나르는 메타데이터 $\iota$와 메타데이터에서 값으로 가는 제공자 함수를 매핑하는 $\sigma$의 쌍이다. 각 키가 모노이드 $(\mathcal{M}_k, \oplus_k, \epsilon_k)$를 갖추고, 명세 $d$가 지닌 컴포넌트 선언 메타데이터와 병합된다. 병합은 우편향(right-biased)이라 문맥이 나르는 $\iota(k)$가 우선권을 가져, 감싸는 문맥이 컴포넌트를 수정하지 않고도 그 컴포넌트의 코이펙트 사용을 제약할 수 있다. 나중에 접근 제어(6.3절)의 기초가 되는 대목이다.

---

6. 문맥 패러다임 (The Context Paradigm)

6.1 통합 문맥 $\Gamma^\infty$

3.1절과 3.2절이 각각 효과와 코이펙트의 운반자로 문맥에 작용했다면, 이제 둘을 하나로 통합한다. 효과 문맥 $\partial\Gamma$ 구조를 재귀적으로 만들고 코이펙트 문맥 $\Sigma$와 결합한다.

$$\Gamma^\infty := \mu\Gamma.\ \Gamma \times (\Gamma \to \Gamma) \times \Sigma$$

세 투영은 현재 문맥 상태(재귀적), 이 수준의 효과를 되돌리는 누적기, 의존성 정보를 나르는 코이펙트 문맥이다. 이 정의 아래 $\mathrm{effect}$가 $\mathfrak{E}_{\Gamma^\infty}$를 자기 자신으로 매핑해 $\partial$-탑을 하나의 자기유사 타입으로 통합한다. 여기 담긴 야심찬 주장이 있다. $\Sigma$의 타입족 $\mathcal{V}$가 제약이 없으므로, 시스템이 컴포넌트 간에 공유해야 하는 어떤 상태든 적절한 값 타입을 가진 의존성으로 인코딩할 수 있다. 즉 $\Sigma$가 컴포넌트 간 의존성뿐 아니라 모든 공유 가변 상태를 포섭한다. 컴포넌트와 환경 사이의 모든 상호작용이 이 단일 개체를 통과한다.

하나의 개체를 통과하는 것이 규율이 되려면 통과할 다른 통로가 없어야 하고, 그래서 바인딩된 값으로 무엇을 할 수 있는지도 고정해야 한다. 그래서 키는 값 이상을 나른다. Definition 29에서 키 $k$의 코이펙트는 쌍 $(\mathcal{V}_k, \mathcal{A}_k)$인데, $\mathcal{A}_k$는 코이펙트 연산 집합, 즉 $k$에 바인딩된 값이 그것을 쥔 컴포넌트에 제공하는 연산들이다. 연산 $a \in \mathcal{A}_k$는 인자 타입 $X_a$와 결과 타입 $B_a$를 나르고 값에만 작용한다.

$$a : X_a \to \mathcal{V}_k \rightharpoonup \mathcal{V}_k \times (\mathcal{V}_k \rightharpoonup \mathcal{V}_k) \times B_a$$

앞 두 성분이 $\mathcal{V}_k$ 위의 효과 함수를 이루고 세 번째가 결과다. 이 연산들이 값을 비교하는 동치 $\simeq_k$를 유도한다. Definition 30은 **문맥 매개 이터레이터(context-mediated iterator)**를 정의하는데, 컴포넌트가 수행하는 것은 단계(stage)의 열이고 각 단계는 어떤 키가 바인딩한 값 위의 연산이거나 자기 바인딩의 제공이다. 이 클래스에 속함이 "모든 상호작용을 문맥을 통해 매개한다"의 형식적 내용이다. 이 클래스 밖에 있는 것은 다른 무언가를 읽는 사상, 예컨대 문맥이 나르지 않는 카운터에서 핸들을 뽑는 할당자다. 그 카운터를 키에 바인딩하는 순간 문맥 매개가 된다.

재귀적 구조 $\Gamma^\infty$는 계층적 제어를 지원한다. 부모 문맥이 여러 자식 수준 효과를 집계해 트리 모양 제어 구조를 이룬다. 효과 변환이 문자 그대로 "플러그인" 은유를 실현한다. 컴포넌트 로드는 효과 실행(꽂기), 언로드는 효과 되돌림(뽑기, 다른 실행 중인 컴포넌트에 영향 없이)이다. 서로 다른 계층의 컴포넌트가 독립적으로 로드/언로드 가능하고 부모가 자식들의 효과를 집계 관리해 임의 중첩 조합이 가능하다.

6.2 관측 동치 (Observational Equivalence)

3.1절의 회복 보장은 상태의 동등성(Theorem 7)을 주장하는데, 이건 이상화(idealization)다. 물리적 상태는 있던 그대로 회복될 수 없기 때문이다. 예컨대 free는 블록을 할당자에 반납하지만 malloc 이전의 힙 레이아웃을 복원하지 않고, 생성된 이름(generative name)은 그것을 버리는 역으로 복원되지 않는다. 다음 생성이 새것을 뽑기 때문이다.

그래서 3절의 등식들은 동치 $\simeq$ 위에서 읽혀야 하고, 저자들은 $\simeq$를 관측 동치로 잡는다. 어떤 관측자도 구별할 수 없으면 두 상태는 관계된다. 표현이 아니라 행동을 비교하는 것이 프로그램 동등성으로 가는 정석이고, 관측자에게 무엇이 주어지는가에 따라 관계가 달라진다. 값의 관측자에게 주어지는 것은 그 키의 연산들(Definition 29)이다. Definition 31은 연산들이 생성하는 유한 단어인 **테스트(test)**를 정의하고, 모든 테스트가 두 값에서 같은 결과를 내면 구별 불가능($v \approx_\mathcal{A} v'$)이라 한다. 키의 동치 $\simeq_k$가 그 자신의 연산 아래 구별 불가능성이다. Lemma 32는 $\simeq_k$가 연산들이 존중하는 가장 거친(coarsest) 동치임을 보인다. 이 clause (2)가 증명 원리 노릇도 한다. 두 값을 관계 짓고 싶으면 연산들이 존중하면서 그 쌍을 포함하는 동치를 하나 제시하면 된다.

키가 바인딩하지 않는 상태 부분은 이렇게 망각되고, 망각이 있어야 Theorem 7을 $\simeq$ 위에서 읽을 수 있다. 힙 레이아웃과 생성 이름이 관계 밖으로 나가는 것이다. Definition 34가 $\simeq_S$를 타입 형성자를 따라 확장하고(함수는 관계된 입력을 관계된 출력으로, 곱은 성분별로, 재귀 타입은 여최대(coinductive)로), Definition 36이 효과 함수를 $\simeq_S$ 위에서 증인화한 $\mathfrak{E}_\Gamma^S$를 정의한다. Lemma 38이 이 대목의 성과다. 3.1절에서 주장한 상태의 모든 등식이 $=$를 $\simeq$로 바꿔도 성립하고, 증명은 관계의 성질 중 추이성과 존중만 쓴다. 즉 물리적 회복 불가능성을 관측 동치가 정확히 흡수한다.

---

7. 독립성 확보 (Attaining Independence)

여기까지가 한 컴포넌트의 국소적 보장이었다. 3.4절은 이를 서로 끼어드는 컴포넌트들의 시스템으로 확장하는 조건을 공급한다. 바로 두 효과 함수의 **독립성(independence)**이다.

3.1절이 다룬 것은 효과를 자기 적용이 만든 상태에서 되돌리는 경우였다. 이제 다른 상태에서 되돌리는 경우가 필요하다. 두 상황이 이를 부른다. 하나는 뒤따르는 효과가 아직 있는데 역을 돌리는 경우로, 실행 중인 시스템에서 컴포넌트 하나를 제거하는 것이 이에 해당한다. 다른 하나는 한 열이 여러 컴포넌트의 효과를 뒤섞는 경우다. 두 경우 모두 역이 외래 효과가 움직여 놓은 상태를 만나므로, 여전히 되돌리는지가 **교환(commutation)**의 문제가 된다.

Definition 42는 이터레이터 $i, j$가 독립적이라는 것을, (1) 하나의 모든 변환이 다른 하나의 모든 변환과 교환하고, (2) 어느 쪽의 변환도 다른 쪽이 내놓는 역과 연속을 교란하지 않는다는 두 조건으로 정의한다. Theorem 43이 성과다. 쌍별 독립인 효과들을 순서대로 적용한 뒤, 도달한 상태에서 $n$개의 역을 어떤 순열의 순서로 적용해도 $\gamma_0$에 도달한다. 즉 독립성 아래에서는 역을 뒤따르는 효과가 움직인 상태에서 돌려도 자기 기여분만 정확히 철회한다.

3.4.2절은 문맥 매개 효과 함수의 독립성을 단일 코이펙트에서의 교환성으로 환원한다. Definition 44가 두 연산의 독립성을, 그 리프트가 효과 함수로서 독립이고 결과도 교란하지 않음으로 정의한다. 키 $k$가 교환적(commutative)이라는 것은 $\mathcal{A}_k$의 임의 두 연산이 독립임을 말한다. Theorem 45는 서로 다른 키의 연산이 무조건 독립임을 보인다. 그래서 조건은 한 키의 쌍들로 귀결되고, 그 독립성 증명이 코이펙트 자체의 성분이 된다(Definition 46). 효과 함수의 증인이 "역이 되돌린다"를 인증하듯, 코이펙트의 증인이 "연산들이 교환한다"를 인증한다. 두 증인이 평행하다는 이 대칭이 논문의 미학적 정점 중 하나다.

교환성의 판단을 저자들은 인터페이스 설계 문제로 뒤바꾼다. 예컨대 라우트나 이벤트 리스너 등록은 각자 고유 항목을 취하므로 교환적이다. 두 등록이 무엇을 등록하든 두 항목의 이름이 다르니 어느 순서든 같은 테이블을 남긴다. 반면 순서 있는 체인(미들웨어)은 교환적이지 않다. 앞에 삽입된 미들웨어가 다른 요청을 보기 때문이다. 할당자는 인터페이스가 무엇을 공개하느냐로 갈린다. 핸들이 어떤 연산으로도 비교되지 않으면 어떤 테스트도 관측하지 못해 $\simeq_k$가 핸들 이름 바꾸기까지 동일시하고 할당은 교환적이 된다. 주소가 등호로 비교되는 결과라면 교환적이지 않다. 저자들은 POSIX가 같은 선을 긋는다고 지적한다. mmap은 임의 미사용 주소를, creat는 임의 미사용 아이노드를 반환할 수 있지만 open은 가장 낮은 가용 디스크립터를 반환하도록 요구되며, 이 요구가 두 디스크립터 할당의 교환을 막는다. 인터페이스가 결과를 덜 공개하면 관계가 거칠어지고, 호출자가 필요로 하지 않는 결과를 감추면 키를 한쪽에서 다른 쪽으로 옮길 수 있다. 이것이 확장가능 교환성 규칙(scalable commutativity rule)이 인터페이스를 가로질러 하는 바로 그 움직임이다. 이론이 실제 시스템 설계 원리와 이렇게 맞닿는 대목이 이 논문의 설득력이다.

무엇이 분해되는가 하면, 계산의 교환하는 부분과 순서에 민감한 부분이다. 교환하는 부분은 효과가 나른다. 컴포넌트가 원하는 순서로 수행하고 시스템이 편한 순서로 되돌린다. 순서에 민감한 부분은 코이펙트가 나른다. 교환하지 않는 키의 순서는 효과 바깥에서 강요되어야 하는데, 한 컴포넌트 안에서는 누적기가 LIFO로, 컴포넌트 간에는 선언된 코이펙트가 강요한다. 조합가능성이 단일 효과가 아니라 컴포넌트 입자에서 얻어지는 것이다.

---

8. 동적 조합 계산 체계 (A Calculus of Dynamic Composition)

논문 4절은 3절의 이론에 운영 의미론을 준다. 실행 중인 시스템을 컴포넌트로 분해하는데, 각 컴포넌트는 코이펙트 명세 $d$, 제공 $p$, 증인화된 효과 함수 $e$의 삼중항이다.

$$\mathfrak{C}_\Gamma := (d : \mathfrak{D}_\Gamma) \times (p : \mathfrak{P}_\Gamma) \times \mathfrak{I}_\Gamma^{d \cup p}$$

$d$는 환경에서 요구하는 의존성, $p$는 환경에 제공할 수 있는 코이펙트 키 집합, $e$는 활성 시 기여하는 효과와 그것을 철회하는 역이다. 코이펙트 측이 "환경에서 읽는 것($d$)"과 "환경에 쓰는 것($p$)"으로 갈린 게 인터페이스의 두 방향인 셈이다.

8.1 파이버와 레지스트리

컴포넌트는 여러 번 인스턴스화될 수 있고, 각 인스턴스는 시간에 따라 활성/비활성을 오가며 자기 생명주기 상태를 나른다. 이 인스턴스를 **파이버(fiber)**라 부른다. 파이버는 튜플 $\langle d, p, e, \pi, \sigma, \tau, \theta \rangle$인데, $\pi$는 부모, $\sigma$는 자기 코이펙트 테이블, $\tau$는 퇴역 플래그, $\theta$는 생명주기 상태다.

$$\Theta_\Gamma := \mathsf{Inactive} \mid \mathsf{Reloading}(i, g, \omega) \mid \mathsf{Active}(g, \omega) \mid \mathsf{Unloading}(g, \omega)$$

$i$는 남은 효과 이터레이터, $g$는 지금까지 쌓은 누적기, $\omega$는 **확정 뷰(committed view)**로 각 선언 키를 전이가 확정된 순간 그것을 제공한 파이버의 이름으로 보낸다. 활성화는 $e$를 실행하며 부수효과를 문맥에 누적하고, 비활성화는 누적기를 적용해 문맥을 회복한다. 실제 런타임에서 전이는 한 스텝이 아니라 구간에 걸쳐 일어나므로, 활성화 중에는 $\mathsf{Reloading}$, 비활성화 중에는 $\mathsf{Unloading}$ 상태에 머문다.

레지스트리 $F_\gamma : \mathfrak{N} \rightharpoonup \mathfrak{F}_\Gamma$는 상태가 지닌 파이버들을 이름으로 담고, 부모 포인터가 $\mathsf{root}$에 뿌리내린 트리를 이룬다. 결정적인 설계는 코이펙트 문맥이 저장되지 않고 유도된다는 것이다.

$$\sigma_\gamma := \bigcup \{\sigma_m \mid m \in \mathrm{dom}(F_\gamma),\ \theta_m = \mathsf{Active}(-, -)\}$$

활성 파이버들이 공동으로 제공하는 바로 정의된다. O-Insert가 제공이 겹치는 파이버를 받지 않으므로 각 키는 정확히 하나의 활성 파이버 테이블에 들어가고, 그 이름을 $k$의 제공자(provider)라 한다. 활성 파이버만으로 합집합을 취하는 이 선택이 중요한데, 파이버가 무언가를 철회하기 전에 제공을 멈출 수 있게 해주고, 이것이 나중에 순서 규율이 된다. $\mathsf{Reloading}$이나 $\mathsf{Unloading}$ 파이버는 자기 $\omega$를 통해 코이펙트를 읽고 자기 것은 제공하지 않는다.

8.2 생명주기와 아홉 개의 규칙

계산 체계는 두 관계를 생성하는 아홉 규칙으로 이뤄진다. 오케스트레이션 규칙(O- 접두, $\gamma \Rightarrow \delta$)은 오케스트레이터가 수행할 수 있는 행동이고, 생명주기 규칙(L- 접두, $\gamma \longrightarrow \delta$)은 전제가 성립하면 시스템이 스스로 밟는 스텝이다. 아래 그림이 이 생명주기를 상태 기계로 그린다.

Figure 1 (원논문): 컴포넌트 생명주기. 빈 노드는 레지스트리에 없는 파이버를 표시한다. O-Insert가 $\mathsf{Inactive}$로 들여오고, L-Begin이 $\mathsf{Reloading}$을 시작하며 L-Iter가 반복하고 L-Finish가 $\mathsf{Active}$로 착지한다. L-Leave가 $\mathsf{Active}$에서, L-Divert가 $\mathsf{Reloading}$에서 $\mathsf{Unloading}$으로 빠지고, L-Unload가 누적기를 적용해 $\mathsf{Inactive}$로 되돌린다.

이 상태 기계가 논문 전체에서 유일하게 번호 붙은 그림이다. 네 개의 안정/전이 상태를 여덟 규칙이 잇는다(아홉 번째 O-Retire는 모든 상태에서 자기 루프라 그림에서 생략된다). 눈여겨볼 대목이 몇 있다. 활성화 경로($\mathsf{Reloading}$)와 비활성화 경로($\mathsf{Unloading}$)가 분리되어 있다는 것, 그리고 $\mathsf{Reloading}$ 중간에 L-Divert로 곧장 $\mathsf{Unloading}$으로 빠질 수 있다는 것이다. 왜 한 스텝으로 못 하는가. 자기 제공자가 떠나서 해체되는 컴포넌트는 자기 해체 코드를 돌리는데 바로 그 사라지는 코이펙트가 필요할 수 있기 때문이다. 커넥션 풀을 닫으려면 커넥션을 그것을 제공한 쪽에 돌려줘야 하는 식이다. 그래서 소비자는 자기 비활성화 내내 키를 읽을 수 있어야 하고, 제공자의 철회는 그 뒤에만 효력을 가져야 한다.

핵심 규칙들을 뜯어보면, O-Insert는 이름이 신선하고, 부모가 레지스트리에 있고, 제공이 기존 어느 파이버와도 겹치지 않을 때 파이버를 $\mathsf{Inactive}$로 들여온다. 이 마지막 전제가 **단일 소스 규율(single-source discipline)**을 부과한다. 키가 하나의 제공자만 갖는 이유다. L-Begin/L-Iter/L-Finish가 활성화를 진행하며 각 반복의 새 역 $h$를 $g \circ h$로 누적기에 합성한다(LIFO). 비활성화 쪽에서 L-Leave는 비활성화 결정을 기록하되 실행하지 않아 파이버가 코이펙트 제공을 멈추게 하고, L-Unload가 누적기를 적용하고 확정 뷰를 버리며 $\mathsf{Inactive}$로 남긴다. L-Unload의 전제 $\neg\,\mathrm{relied}_n(\gamma)$가 **가드(guard)**로, $n$에 키를 해소한 소비자가 모두 떠날 때까지 제공자의 철회를 붙든다.

$$\mathrm{relied}_n(\gamma) := \exists m \in \mathrm{dom}(F_\gamma),\ k \in d_m.\ m \neq n \land \mathrm{installed}_m(\gamma) \land \omega_m(k) = n$$

보통 이런 가드는 교착(deadlock)에 빠지는데, 이를 막는 것이 $\mathsf{Unloading}$과 "$\sigma_\gamma$가 활성 파이버만의 합집합"이라는 사실의 조합이다. L-Leave나 L-Divert가 $n$을 표시하는 순간 $n$의 테이블이 $\sigma_\gamma$를 떠나므로 어떤 타깃 뷰도 더는 $n$을 지목할 수 없고, $n$에 확정한 소비자들도 모두 떠나는 중이 된다.

8.3 국한(Confinement)

효과 함수가 무엇을 쓰고 읽는지를 경계 짓는 것이 국한이다. Definition 55는 사상 $f$가 $n$에 국한된다는 것을, (쓰기 측) 자기 테이블 $\sigma_n$과 자기가 선언한 키의 값들 $\sigma_m|_{d_n}$만 바꾸고, (읽기 측) 그 두 부분에만 의존함으로 정의한다. 이것이 있어야 한 규칙이 다른 모든 변화를 회계할 수 있고, 이것이 Table 1을 완전한 쓰기 목록으로 읽게 해준다. 문맥 패러다임이 효과 함수의 형태(연산/제공/인스턴스화 단계의 열)를 고정하므로 국한은 그 형태의 귀결이다.

---

9. 메타이론 (Metatheory)

4.3절이 계산 체계의 메타이론을 확립한다. 모든 산출물이 스텝 열에 대한 성질이라, 스텝을 $t$로 색인해 상태 $\gamma^t$를 읽는다. Table 1이 아홉 규칙을 파이버 $n$ 위의 쓰기로 읽은 것이다.

Table 1 (원논문): 아홉 규칙을 각 규칙이 작용하는 파이버 $n$ 위의 쓰기로 읽은 표. $\Psi^t$는 스텝의 상태 사상, $h$는 넷째 열의 반복이 내놓는 역($\mathrm{id}_\Gamma$는 L-Divert가 반복을 중단한 경우). 각 스텝은 $\gamma^{t+1} = \mathrm{edit}^t(\Psi^t(\gamma^t))$로 분해된다.

이 표를 눈여겨보면 메타이론 전체가 이 한 장의 "룩업(lookup)"으로 돌아간다는 걸 알 수 있다. 상태 사상 $\Psi^t$가 누적기를 적용하는 유일한 규칙은 L-Unload뿐이고(넷째 열의 $g$), 나머지는 전방 사상 $\mathrm{pr}_1 \circ i$거나 $\mathrm{id}_\Gamma$다. 테이블은 O-Insert가 빈 것을 설정한 뒤로 어떤 $\mathrm{edit}^t$도 쓰지 않고, 제어 필드는 어떤 $\Psi^t$도 쓰지 않는다(Definition 52의 인스턴스화 프리미티브 제외). 이 깔끔한 분리가 이후 모든 경우 분석을 표 조회로 환원시킨다.

9.1 보존, 시간적 조합가능성

Theorem 64(보존)는 모든 규칙이 레지스트리의 정합성(well-formedness)을 보존함을 보인다. 부모 포인터가 트리를 이루고, 서로 다른 파이버의 제공이 겹치지 않고, 활성 파이버의 확정 뷰가 전역(total)이며 그 값이 다시 활성 파이버임을 유지한다.

시간적 조합가능성의 전역 형태가 4.3.2절이다. 국소 형태는 한 효과 열을 한 누적기로 되돌리는 것이었다. 레지스트리는 파이버당 누적기 하나를 쥐고 파이버들이 뒤섞이므로, $n$이 $g_n$에 역을 합성한 순간과 $g_n$이 실행되는 순간 사이에 다른 파이버들이 상태를 움직인다. Lemma 66(쌍별 독립)이 열쇠다. 모든 스텝 열이 쌍별 독립이다. 얽히지 않은(non-entangled) 쌍은 Theorem 47로 독립이고, 얽힌 쌍은 규칙 자체가 두 사상을 그것들이 갈리는 순서로 결코 끼워 넣지 않는다. Theorem 68(회복 정확성)이 성과다.

$$g_n^u(\gamma^u) \simeq_K (\Psi^{t_l} \circ \cdots \circ \Psi^{t_1})(\gamma^b)$$

$n$의 누적기를 $\gamma^u$에서 적용하면 같은 스텝들이 $\gamma^b$에서 남겼을 자리에 모든 파이버의 테이블을 남긴다는 뜻이다. 쉽게 말해, 다른 파이버들이 아무리 끼어들어도 $n$의 되돌림은 $n$의 기여분만 정확히 철회하고, 마치 $n$이 애초에 시작하지 않았던 것처럼 상태를 남긴다. Corollary 69(종단 회복)가 $\sigma_n^{u+1} = \varnothing$을 주며, 이것이 O-Remove가 파이버를 안전히 제거할 수 있는 전제가 된다.

9.2 공간적 조합가능성, 진행, 합류성

공간적 조합가능성의 전역 형태(4.3.3절)는 두 성질을 준다. Theorem 70(순서)은 제공자가 자기에게 키를 해소한 모든 의존자가 비활성화된 뒤에만 바인딩을 철회함을, 그리고 파이버가 자기 의존성이 제공될 때만 전이를 시작함($\mathsf{step}^t = \text{L-Begin}(m) \Rightarrow \gamma^t \models d_m$)을 보인다. Theorem 71(해소 정합성)은 스텝에 걸쳐 진행되는 전이가 도중에 바뀐 해소에 대해 효과를 설치하지 않도록, 전이가 확정 뷰가 여전히 타깃 뷰인 동안만 진행됨을 보장한다.

Theorem 73(진행)은 가드가 결국 풀림을 확립한다. 선행 관계 $n \prec m := p_n \cap d_m \neq \varnothing$이 비순환(acyclic)이라는 가정 아래, (1) 교착 없음(비정지 상태에서는 어떤 생명주기 규칙이 적용됨)과 (2) 종료($S(n) \leq (K+3)(V(n)+1)$)를 보인다. 결과적으로 생명주기 스텝의 모든 최대 열이 정지(quiescent) 상태로 끝난다. 스케줄러를 전혀 언급하지 않고 모든 규칙 적용 열에 대해 증명하므로, 어떤 스케줄링 정책에도 성립한다는 점이 강력하다.

합류성(confluence)(4.3.5절)이 시스템 전체를 특징짓는 성질이다. 실행 중인 시스템이 어떤 활성/비활성 열을 거쳤든, 정지하는 상태는 "결국 활성이 되는 각 컴포넌트를 의존성 순서로 한 번씩 로드하고 아무것도 언로드하지 않았을 때 얻었을 상태"와 같다. 생명주기 관계가 합류적이고 그 정규형(normal form)이 정적으로 조립한 상태라는 것이다. Theorem 80(합류성)이 이를 증명한다. 이것이 왜 중요한가. Cordis 애플리케이션을 마치 정적으로 조립된 것처럼 추론할 수 있게 해준다. 컴포넌트를 추가하고, 제거하고, 제공자를 교체하고, 교체를 되돌리는 오케스트레이터가 처음부터 최종 조합을 써 놓았을 때의 상태에 도달함이 보장된다. 이것이 증분 계산(incremental computation)에서 변화 전파가 확립하는 "처음부터 평가한 것과의 일관성"의 동적 조합판이다.

9.3 확장 (Extensions)

4.4절은 네 확장을 준다. 각각 구현으로 실현되고 4.3절 결과를 온전히 유지한다. **비동기(asynchrony)**에서는 반복과 역이 퓨처(future)를 내놓아 진행 중인 사상이 원하든 아니든 완료까지 달리므로, L-Divert의 중단 대안을 제공할 수 없는 관성적(inertial) 호스트가 된다. **실패(failure)**는 반복이 삼중항 대신 오류를 일으킬 수 있게 이터레이터를 $\Gamma \to \mathsf{Either}(\Xi, \cdots)$로 정련한다. 실패한 파이버는 아무것도 설치하지 않은 채 $\mathsf{Inactive}$에 도달하고 오류를 결과로 기록하며, 재진입을 보류해 부모로 전파되지 않고 형제는 계속 돈다. **격리(isolation)**는 영역을 나르는 계산 체계가 키 집합을 $K \times R$로 키운 현재 계산 체계임을 보인다. **구성(configuration)**은 컴포넌트가 설정을 받아 인스턴스화가 페이로드를 효과 함수에 바인딩함을 다룬다.

---

10. 구현: Cordis

논문 5절이 이론을 실제 TypeScript 메타프레임워크 Cordis로 실현한다. Cordis는 웹 라우팅이나 ORM 같은 특정 도메인을 겨냥하지 않는 메타프레임워크로, 유일한 책임은 보편적 동적 조합 의미론을 공급하는 것이다. 세 계층으로 나뉜다. 코어 라이브러리(효과/코이펙트 시스템 직접 구현), 컴포넌트 로더(구성 조정과 핫 모듈 교체), 그리고 그 위의 Koishi 같은 애플리케이션 프레임워크다.

아래는 이론 구성물과 런타임 대응을 정리한 것이다.

Table 2 (원논문): 이론에서 구현으로의 대응. 런타임 이름은 이후 절 전체에서 사용되고, 이론 기호는 형식적 대응에만 남긴다. @@name은 프레임워크 내부 심볼 키를 뜻한다.

이 대응표가 논문의 성실함을 보여준다. 92쪽의 형식화가 허공에 뜬 것이 아니라 실제 API의 각 메서드로 착지한다. 특히 $\mathsf{Reloading}$이 LOADING으로, 4.4절의 관성이 fiber.inertia로, 진행 중 전이 핸들로 정확히 매핑되는 지점이 인상적이다.

10.1 효과 추적

Cordis의 모든 문맥 변경은 단일 프리미티브 ctx.effect를 통과한다. 코이펙트 제공, 컴포넌트 인스턴스화, 그 밖의 모든 문맥 변경 연산이 ctx.effect 호출로 환원되므로, 문맥을 통해 수행된 모든 연산이 자동으로 추적되고 언로드 시 되돌려진다. ctx.effect는 $\mathrm{effect}^{\mathrm{iter}}_\Gamma$의 실현으로, $\mathfrak{I}_\Gamma$ 타입 콜백을 받아 $\mathfrak{I}_{\partial\Gamma}$로 들어올리고 dispose 클로저를 내놓는다.

function execute(iter, guard)
  inverse ← id
  repeat
    if not guard() then break
    (value, done) ← await iter.next()
    if value then inverse ← value ∘ inverse   ▷ LIFO 누적
    if done then break
  return inverse

function effect(ctx, callback)
  armed ← true
  task ← execute(callback, () ↦ armed)
  async function dispose()
    if not armed then return                  ▷ 최대 한 번만 발화
    armed ← false
    recover ← await task
    recover()
  ctx.dispose ← dispose ∘ ctx.dispose          ▷ 부모 누적기에 선합성
  return dispose

원논문 Algorithm 1 (효과 추적)을 옮긴 것. execute가 콜백을 효과 이터레이터로 몰고 각 스텝의 역을 단일 합성으로 접는다. 스텝 전 가드를 확인해 가드가 걸리면 반복을 멈추고 그때까지의 역만 남긴다.

여기서 정직한 대목을 짚어야 한다. ctx.effect가 검사하지 않는 것이 $\mathfrak{E}_\Gamma^*$가 나르는 증인이다. 콜백이 역을 공급하지만, 그 역이 효과를 실제로 되돌리는지는 런타임이 검증하는 성질이 아니라 컴포넌트 작성자의 의무다. 코이펙트의 증인(교환성)도 같은 식으로 미검사다. 즉 형식화가 보장하는 것과 런타임이 실제로 강제하는 것 사이에 틈이 있고, 저자들은 이를 숨기지 않고 명시한다. Theorem 68이 이 의무에 호소하는 지점이고, 6.1절이 그 의무를 경계 짓는 곳이다.

ctx.effect가 두 가지를 더한다. 자기 폐기(self-disposal)로, 반환된 dispose가 armed를 false로 뒤집어 진행 중 반복을 멈추고 회복이 최대 한 번만 발화하게 한다. 두 번 발화하면 효과의 어떤 적용도 만들지 않은 상태에서 역을 적용하게 되어 되돌릴 대상이 없어지기 때문이다. 그리고 부모 합성으로, dispose가 감싸는 문맥의 누적된 역 ctx.dispose에 선합성되어 자식 효과의 역이 그 자체로 부모 위의 효과가 된다. 바로 $\partial^2\Gamma$의 재귀 구조다.

10.2 코이펙트 연산과 반응적 통지

코이펙트 연산은 문맥이 나르는 세 심볼 키 슬롯(@@store, @@isolate, @@intercept)에 작용한다. ctx.get(key)는 @@isolate에서 영역 심볼 $\rho(k)$를, 그 다음 @@store에서 바인딩 값 $\sigma(\rho(k))$를 읽는 2층 해소다. set(k, v)가 타입 $\mathfrak{E}_\Sigma$이므로 코이펙트 제공은 ctx.effect 호출이고 자동 추적/회복을 상속한다. 설치와 제거 모두 notify를 불러 변화를 의존자에게 전파한다.

원논문 Algorithm 3 (반응적 통지): 각 라이브 파이버에 대해 변경된 키가 fiber.inject에 있고 같은 영역으로 해소되는지 검사하고, 그렇다면 refresh를 불러 새 상태에 대해 재평가한 뒤 재평가한 파이버들을 반환한다.

이 알고리즘이 Definition 22의 반응적 분류를 실현한다. 충족을 뒤집는 변화가 파이버를 활성화하거나 비활성화하고, refresh의 멱등성(idempotence)이 중립 변화를 무해하게 만든다. 결정적으로, 바인딩은 그것을 설치한 파이버가 ACTIVE인 동안에만 의존자에게 가용한 것으로 친다. 그래서 UNLOADING에 들어간 제공자는 제공을 멈춘 것이고, 그 의존자들은 바인딩이 아직 다 제자리에 있는 동안 불충족 타깃 뷰를 재계산하며 자기 해체를 시작한다. 이것이 철회를 실제 일어나기 한 스텝 전에 의존자에게 보이게 하는 장치다.

10.3 컴포넌트 생명주기

컴포넌트는 ctx.use로 파이버로 인스턴스화된다. Algorithm 5가 4.4절의 관성 상태 기계를 실현한다.

function refresh(fiber)
  target ← target(γ, n)
  if target = fiber.target then return
  fiber.target ← target
  if fiber.inertia then return              ▷ 전이 진행 중이면 대기
  if target ≠ ⊥ then
    fiber.state ← LOADING; fiber.inertia ← create_task(reload(fiber))
  else
    fiber.state ← UNLOADING                 ▷ 어떤 역도 예약되기 전에 서비스 중단
    fiber.inertia ← create_task(unload(fiber))

async function reload(fiber)
  target0 ← fiber.target
  fiber.committed ← resolve(fiber.inject)   ▷ 뷰 확정
  recover ← await execute(fiber.apply, () ↦ fiber.target = target0)
  fiber.dispose ← recover ∘ fiber.dispose
  if fiber.target = target0 then
    fiber.state ← ACTIVE; notify(fiber.ctx, provided(fiber)); fiber.inertia ← null
  else
    fiber.state ← UNLOADING; fiber.inertia ← create_task(unload(fiber))

async function unload(fiber)
  await all(notify(fiber.ctx, provided(fiber)).map(f ↦ f.await()))  ▷ 의존자 배수
  await fiber.dispose(); fiber.dispose ← id; fiber.committed ← ⊥
  if fiber.target = ⊥ then
    fiber.state ← INACTIVE; fiber.inertia ← null
  else
    fiber.state ← LOADING; fiber.inertia ← create_task(reload(fiber))

원논문 Algorithm 5 (컴포넌트 생명주기)를 옮긴 것. reload와 unload가 완료 시 타깃을 확인해 관성적 연쇄(inertial chaining)를 가능하게 한다. 한 전이가 시작되면 완료되기 전에는 새 전이가 시작될 수 없다.

fiber.target이 각 선언 키를 현재 코이펙트 저장소에 대해 해소하고 제공 파이버의 uid를 튜플로 묶은 $\mathrm{target}(\gamma, n)$의 다이제스트다. 값이 아니라 제공자로 바인딩을 식별하는 것이 결정적인데, uid가 신선하게 뽑히고 재사용되지 않으므로, 교체된 제공자를 그것이 교체한 것과 혼동할 수 없다. 두 제공자가 같은 값을 제공해도 그렇다. 그래서 파이버는 자기 선언 키 중 하나가 다른 파이버에 의해 제공되게 될 때 정확히 리로드한다. 제공자가 자기 바인딩을 제자리에서 덮어써도 관측되지 않고, 교체 전파를 원하는 컴포넌트는 바인딩을 철회하고 새로 설치해야 한다.

세 줄이 Theorem 70의 코이펙트 순서를 나른다. reload가 14행에서 해소된 뷰를 확정하고 unload가 모든 역이 실행된 뒤에야 이를 버리므로, 파이버는 로드된 동안 내내(자기 해체 포함) 같은 바인딩을 읽는다. refresh가 전이 태스크 생성 전에 10행에서 파이버를 UNLOADING으로 표시하는 것이 L-Leave 스텝이다. unload가 25행에서 각 통지된 의존자가 INACTIVE에 도달하길 기다리는 것이 L-Unload의 가드다. 형식화의 정리가 구현의 특정 행 번호에 이렇게 정확히 대응된다는 점이 이 논문의 밀도를 다시 확인시킨다.

10.4 컴포넌트 로더와 HMR

코어 라이브러리가 ctx.effect, ctx.use, ctx.set 같은 명령형 프리미티브를 준다면, 컴포넌트 로더는 선언적 구성 계층을 더한다. 오케스트레이터가 원하는 조합을 지속 자료구조로 명시하면 로더가 이를 대응하는 명령형 파이버 연산으로 번역한다. 각 항목(entry)은 안정 식별자 id, 컴포넌트 모듈 url, 격리/가로채기 주석, config, disabled 플래그를 기록한다. 항목이 충실한 명세가 될 수 있는 이유가 재치 있다. Definition 74의 지지 집합(support set)이 $\tau, \pi, d, p$만 읽는데 항목이 이 넷을 모두 준다. disabled가 $\tau$를, 트리 상 부모가 $\pi$를, url이 $d$와 $p$를 선언하는 컴포넌트를 선택한다.

조정(reconciliation)의 건전성이 메타이론에서 나온다. Theorem 80이 정지 상태를 최종 구성만의 함수로 만들어, 로더가 어떤 순서로 인스턴스화/퇴역을 수행하든 처음부터 최종 구성을 로드했을 자리에 정지한다. 그래서 로더는 항목의 어느 필드가 바뀌었는지에 따라 가장 덜 파괴적인 연산을 적용한다. id/url은 재구축, isolate는 영역 재배정, intercept는 제자리 갱신(읽기 시점에 소비되므로 리로드 불필요), config는 컴포넌트에 넘겨 실질 변화 시에만 리로드, disabled는 언로드/리로드다.

**핫 모듈 교체(HMR)**는 되돌릴 수 있는 효과 패턴을 모듈 수준에 적용한다. 파이버가 이미 컴포넌트의 모든 효과와 코이펙트를 경계 짓고 있으므로, 컴포넌트인 모듈은 파이버 연산만으로 교체된다. 낡은 파이버를 폐기하면 컴포넌트가 설치한 모든 것이 회복되고, 리로드된 모듈에서 새 파이버가 재설치한다. 그래서 Webpack이나 Vite의 HMR과 달리 개발자가 주석 단 수용 경계(acceptance boundary)가 필요 없다. HMR 엔진은 세 단계로 동작한다. 모듈 분류(변경된 파일의 의존 하위그래프를 accepted/declined로 표시), 낡은 항목 탐지(의존 트리가 변경 모듈에 닿는 항목 필터), 트랜잭션 리로드(실패 시 캐시 복원과 백업 재구축으로 반쪽 리로드 상태를 방지)다.

---

11. 사례 연구: Koishi

Koishi는 Cordis 위에 지어진 오픈소스 챗봇 애플리케이션 프레임워크다. 4년 개발 동안 4000개가 넘는 커뮤니티 기여 플러그인이 쌓였고, IM 어댑터와 데이터베이스 드라이버부터 관리 콘솔과 최종 사용자 기능까지 걸친다. 규모와 다양성 덕에 프로덕션 환경에서 Cordis의 동적 조합가능성을 검증하는 대표 사례가 된다.

사례가 뒷받침하는 것은 세 가지다. 첫째, 표현력과 일반성이다. Koishi의 모든 기능이 5.1절 문맥 프리미티브 위의 플러그인으로 실현되고 Koishi 자체는 챗봇 도메인 어휘만 기여한다. 같은 모델이 전혀 다른 런타임(브라우저와 UI 프리미티브를 조합하는 Koishi 웹 콘솔)에서 재등장하므로, 모델이 특정 도메인이나 런타임을 전제하지 않음을 보인다. 둘째, 인지 부하 없는 시간적 조합가능성이다. 문맥을 통한 효과가 자동 추적되고 역이 자동 합성되므로, 미숙한 작성자도 언인스톨 경로를 쓰지 않고 순서 있는 정리를 얻는다. 1.2.1절이 지적한 locality of concern 부재를 abstraction이 한 번에 해소하는 것이다. 셋째, 열린 생태계에서의 공간적 조합가능성이다. IM 어댑터가 각 메시징 플랫폼 접근을, DB 드라이버가 저장소를 제공하고 기능 플러그인이 이를 코이펙트로 선언한다. 런타임에 제공자를 재구성(저장 백엔드 전환, 어댑터 재연결)하면 해소된 의존성이 바뀐 의존자만 재활성화되고, 의존성이 없는 플러그인은 에러 없이 나타날 때까지 비활성으로 대기한다.

여기서 저자들이 자기 검증의 한계를 솔직히 밝히는 대목이 신뢰를 준다. 증거가 단일 언어(TypeScript)의 단일 생태계에서 나왔으므로 패러다임의 장점을 그 TypeScript 실현이나 Koishi 도메인의 장점과 분리할 수 없고, 대안 아키텍처에 대한 통제된 비교가 아니라 관찰적(observational)이다. 그래서 확립하는 것은 정량적 결과가 아니라 존재-채택(existence-and-adoption) 결과다. 추상화의 오버헤드와 개발자 생산성에 미치는 효과를 베이스라인과 비교해 측정하는 것은 향후 과제로 남긴다. 개인적으로는 이 정직함이 오히려 논문의 무게를 더한다고 본다. 4000개 플러그인이라는 규모가 "이 모델로 실제 생태계가 굴러간다"는 강력한 실존 증거인 것은 분명하니까.

---

12. 논의 (Discussion)

6절이 패러다임이 더 넓은 공학적 관심사로 확장되는 방식과 설계 긴장을 다룬다. 핵심 개념들만 짚는다.

**시스템 경계(system boundary)**가 6.1절이다. 모든 효과가 역을 나르지만 그 역이 무엇이 되는가는 시스템 경계가 결정한다. 시스템이 어떤 위치를 배타적으로 수정하고 이전 상태로 복원할 수 있으면 그 위치는 경계 안에 있어 $\Gamma$에서 추적되고 되돌려진다. 둘 중 하나라도 실패하면 경계 밖이고 연산은 $\mathrm{id}_\Gamma$로 작용해 추적도 되돌림도 안 된다. 코이펙트가 외부 위치를 사물화해 경계를 옮긴다. 결정적 구분은 **획득(acquisition)과 방출(emission)**이다. 경계 밖에 닿는 연산은 보통 두 단계로 진행된다. 획득 단계는 접근을 얻고 경계 안에 기록을 설치한다(open이 close가 제거하는 디스크립터를, malloc이 free가 푸는 블록을 설치). 이 기록 설치가 되돌릴 수 있는 효과다. 방출 단계는 그 채널로 데이터를 밀어내는데(파일에 쓰는 바이트, 와이어에 얹는 데이터그램) 이 밀어냄이 $\mathrm{id}_\Gamma$로 작용해 데이터를 다른 당사자가 읽고 쓸 수 있는 곳에 남긴다. 획득은 안에, 방출은 밖에 떨어진다. 방출로부터 회복해야 하면 방출을 상태가 지속될 때까지 보류하거나(출력 커밋 문제), 애플리케이션이 공급하는 더 거친 동치까지 상태를 복원하는 보상(compensation)을 쓴다.

**서비스 다중화(service multiplexing)**가 6.2절이다. OSGi 같은 동적 컴포넌트 플랫폼처럼 코이펙트 모델을 서비스로 조직한다. 하나의 서비스가 여러 제공자로 구현될 때 배타적 바인딩(한 번에 하나만) 또는 서비스 브로커(중앙 서비스가 디스패치)로 실현된다. 브로커가 부하 분산, 롤링 업데이트, 프로세스 간 호출을 떠받친다. 특히 롤링 업데이트가 전통적으로 인프라 수준 연산(컨테이너 오케스트레이션, 블루-그린 배포)이던 것을 애플리케이션 수준 조합 패턴으로 바꾼다는 지적이 흥미롭다.

접근 제어와 샌드박싱(6.3절)에서 의존성 접근 메커니즘이 이미 능력 기반 보안(capability-based security)의 한 형태다. 컴포넌트는 선언한 의존성만 접근할 수 있고 미선언 접근은 오류다. inject 선언이 능력 요청, 문맥 프록시가 능력 중개자 노릇을 한다. 가로채기를 통해 세밀한 정책으로 일반화되어, 파일시스템 의존성이 어느 경로를 읽고 쓸지 선언하는 메타데이터를 나를 수 있다. 다만 신뢰할 수 없는 코드의 샌드박싱은 언어 수준 접근 제어로 불충분해 외부 샌드박스(SFI, 별도 런타임, 격리 프로세스, 가상 컨테이너)가 필요하다.

언어 독립성(6.4절)은 문맥 패러다임이 언어 불가지론적임을 논한다. 시간적 조합가능성은 클로저와 런타임 모듈 도입/철회(관리 런타임의 모듈 레지스트리, 네이티브의 dlopen/dlclose, WebAssembly의 임베더별 경로)를 요구한다. 공간적 조합가능성은 의존성 주입 문제로 환원되어, 타입 수준(타입클래스, 트레이트, 모듈 증강)과 런타임 수준(JS Proxy, Python 디스크립터 프로토콜)의 매개를 요구한다.

상호 의존성과 입자도(6.5절)에서 의존성 순환은 관련 컴포넌트를 영구 비활성으로 남긴다. 하지만 스케줄에 의존하는 동시성 교착과 달리 선언만으로 예측 가능해서 로드 시점에 보고할 수 있다. 대부분의 겉보기 상호 의존은 더 잘게 분해해 순환을 없앨 수 있으나, 통합 컴포넌트 수가 최악의 경우 $n$에 대해 2차로 증가할 수 있다. 의존성 타이핑과 버저닝(6.6절)은 키 정체성만으로 링크가 성립하는 데서 오는 인터페이스 드리프트와 키 충돌 문제를 다루고, 키 네임스페이싱, 피어 의존성, 구조적 호환성 세 접근을 논한다. 언어/OS 공동 설계(6.7절)는 패러다임을 중심으로 설계된 언어가 문맥을 다시 암묵적으로 만들면서 문맥 의미론을 보존하고, 효과와 코이펙트를 컴파일러에 알려 단일 상태 기계를 방출하거나 의존성 순환을 컴파일 타임에 보고할 수 있음을 논한다.

---

13. 관련 연구에서의 위치

7절이 관련 연구를 촘촘히 정리하는데, 이 논문이 어디에 서 있는지를 명확히 한다.

효과와 코이펙트 시스템과의 차별점이 핵심이다. ZIO, Effect-TS, fp-ts 같은 모나드 효과 시스템은 프로그램이 효과 타입 안에 쓰여야 추적을 얻지만, Cordis는 평범한 호스트 코드 위의 오버레이로 효과를 추적한다. 또 이들은 요구를 해석(설치된 서비스)으로 해소하고 서비스가 철회되어도 그 연산이 수행한 것은 남지만, Cordis는 각 효과를 역과 짝짓고 제공자가 오갈 때 요구를 재해소한다. Brachthäuser 등의 Effekt 언어가 가장 가까운데, 효과 타입을 능력(capability)으로 재해석해 문맥을 능력의 중개자로 다룬다는 점이 닮았다. 하지만 (1) 목적에서, 대수적 효과는 모듈적 해석을 위해 효과를 가시화하는 반면 Cordis는 추적과 되돌림을 위해 가시화한다. (2) 설정에서, Effekt는 타입 수준에서 정적으로, Cordis는 런타임에서 규율한다. Heunen 등의 가역 효과 의미론이 형식적으로 가장 가깝지만(각 효과를 되돌릴 수단과 짝지음), 그들은 전역적으로 가역인 범주론적 설정에서 양방향 역을 구성으로 얻는 반면 Cordis는 런타임에 역을 추적하며 각 원자 효과의 한쪽 역만 요구한다. Orchard 등의 등급 모달 타입(Granule)이 효과와 코이펙트를 단일 타입 시스템으로 추적하지만 모두 타입 수준의 정적 주석인 반면, 이 논문은 같은 두 개념을 런타임 메커니즘으로 들어올린다는 점이 직교적 기여다.

프로그래밍 패러다임에서는 문맥 지향 프로그래밍(COP)과 관점 지향 프로그래밍(AOP)과 비교한다. COP와는 문맥을 일급 런타임 가변 개체로 다루고 행동을 동적으로 활성/비활성한다는 점에서 겹치지만, COP의 레이어는 자기가 유도한 부수효과를 추적하거나 되돌리지 않고 활성화가 의존성 충족에 지배되지 않는다는 점에서 명목상의 유사일 뿐이다. AOP의 애스펙트에 대응하는 Cordis의 개념은 코이펙트인데, AOP 포인트컷이 무지(oblivious)하고 정량화된 반면 Cordis는 교차관심사를 각 컴포넌트가 선언한 코이펙트로 국한해 결정성과 추적성을 얻는다.

시간적 조합가능성의 선행 연구를 네 갈래로 나눈다. 상태 전방 이주(DSU, Erlang/OTP, Webpack/Vite HMR)는 상태를 손으로 쓴 변환 함수로 새 버전에 넘기는 반면, Cordis는 낡은 효과를 되돌리고 새것을 깨끗한 상태에서 재적용한다(수제 이주 함수 불필요, 완전 언로드와 자원 회복 지원). 개발자 작성 회복(OSGi, Command 패턴, saga, React useEffect)은 역이 강제되지 않는 의무라 잊으면 조용히 누수된다. React useEffect가 구조적으로 가장 가깝지만 조합성에서 부족하다(최상위에서만 호출, async나 이터레이터 불가). 정적 스코프 반전(STM, 가역 컴퓨팅, Janus, RCCS, 선형 타입, RAII, Rust 소유권)은 반전을 미리 고정된 스코프에 국한하는 반면 Cordis는 스코프를 미리 고정하지 않는다. 개입적 회수(Nooks, shadow drivers, Akeso)가 시스템 수준에서 가장 가까운 선례인데, 플랫폼이 기록 가능한 것을 고정하는 반면 Cordis 컴포넌트는 자기 효과를 도입하고 각 원자 효과의 역을 공급한다.

공간적 조합가능성에서는 초기화 시점 배선(Spring, Guice, React Context)이 반응적으로 재해소하지 않는 반면 Cordis의 반응적 코이펙트가 이를 공급함을, OSGi 선언적 서비스와 iPOJO가 가장 가까운 선례지만 동기적 손수 콜백에 의존하는 반면 Cordis는 관성적 $\mathsf{Unloading}$으로 비동기 해체를 완료까지 돌림을, FRP/시그널이 값 수준에서 작동하는 반면 Cordis는 컴포넌트 수준에서 비동기 생명주기 의미론을 더함을 짚는다.

---

14. 비판적 관점

강점부터 정리하면, 이 논문의 가장 큰 미덕은 개념적 통합의 우아함이다. "코이펙트 연산이 곧 효과이고 효과는 되돌릴 수 있다"는 단 하나의 관찰에서 출발해, 되돌림-추적-반응이 하나의 문맥 위에서 맞물리는 그림을 끝까지 밀어붙인다. 효과 함수의 증인과 코이펙트의 증인이 평행하게 대칭을 이루는 설계, $\partial$-탑의 자기유사성이 계층적 조합으로 자연스럽게 이어지는 방식, 교환성을 인터페이스 설계 문제로 뒤바꿔 POSIX나 확장가능 교환성 규칙과 맞닿게 하는 통찰은 이론적 성숙함을 보여준다. 그리고 이 모든 형식화가 실제 프로덕션 프레임워크(4000개 플러그인의 Koishi)로 착지한다는 점에서, 이론과 실천의 간극이 좁다.

메타이론의 완결성도 강점이다. 보존, 시간적/공간적 조합가능성, 진행, 합류성까지 한 계산 체계 안에서 증명하고, 특히 합류성(정지 상태가 정적 조립과 일치)은 실무적으로 매우 값진 보장이다. 오케스트레이터가 무슨 짓을 하든 최종 구성만으로 결과를 추론할 수 있다는 것이니까. 스케줄러를 언급하지 않고 모든 규칙 적용 열에 대해 증명해 임의 스케줄링 정책을 덮는다는 점도 견고하다.

약점과 아쉬운 점도 분명하다. 첫째, 검증의 성격이다. 저자들 스스로 밝히듯 Koishi 사례는 관찰적이고 존재-채택 결과일 뿐, 정량적 오버헤드 측정이나 통제된 비교가 없다. 되돌릴 수 있는 효과의 런타임 비용, 매 스텝 클로저 할당, 프록시 기반 접근의 오버헤드가 실제로 얼마인지 이 논문만으로는 알 수 없다. "가볍다(lightweight)"는 서술이 반복되지만 수치가 뒷받침하지 않는다.

둘째, 증인 미검사의 틈이다. 논문이 정직하게 인정하듯, 역이 실제로 되돌리는지와 연산이 실제로 교환하는지는 런타임이 검증하지 않고 작성자의 의무로 남는다. 즉 모든 형식적 보장(Theorem 68 등)이 이 미검사 가정 위에 서 있다. 형식화는 "올바른 역과 교환적 키가 주어지면"을 전제하는데, 4000개 커뮤니티 플러그인 생태계에서 이 전제가 얼마나 지켜지는지, 어긋났을 때 어떤 실패가 나는지에 대한 논의는 얕다. 이것은 이론의 결함이라기보다 이론이 강제할 수 없는 것을 실무가 떠안는 구조인데, 그 실무적 리스크의 크기가 궁금하다.

셋째, 입자도 비용이다. 6.5절이 상호 의존을 없애려면 통합 컴포넌트가 2차로 늘 수 있다고 인정한다. 순환 제거가 원리적으로 늘 가능해도, 실제 개발자가 감당할 설정과 명명과 인지 부하가 만만치 않을 것이다. 저자들이 제시하는 완화책(패키지 번들링, 관례 기반 배선, 스캐폴딩)은 다분히 미래 과제 수준이다.

넷째, 방출(emission) 회복의 근본적 한계다. 6.1절이 솔직히 말하듯 방출은 $\mathrm{id}_\Gamma$로 작용해 되돌릴 수 없고, 보류나 보상으로 우회할 뿐이며 그 경우 메타이론(교환성)을 더 거친 동치에 대해 다시 세워야 한다. 즉 이 프레임워크의 아름다운 보장은 "경계 안"에서만 온전하고, 실제 시스템의 가장 성가신 부분(외부 부수효과)은 여전히 애플리케이션의 몫이다. 이건 아마 피할 수 없는 한계겠지만, 그만큼 "완전한 회복"이라는 수사가 실제 적용 범위에서 얼마나 좁아지는지 독자가 유념할 필요가 있다.

---

15. 마무리

이 논문은 "실행 중에 컴포넌트를 안전하게 넣고 빼는" 오래된 실용적 문제에 처음으로 제대로 된 형식적 기초를 놓으려는 시도다. 효과와 코이펙트라는 두 정적 도구를 런타임 메커니즘으로 들어올려, 되돌릴 수 있는 효과로 시간적 조합가능성을, 반응적 코이펙트로 공간적 조합가능성을 확립하고, 둘을 통합 문맥 위에서 매개하는 문맥 패러다임으로 묶는다. 그 위에 세운 동적 조합 계산 체계의 메타이론이 국소적 보장을 시스템 전역으로 옮기고, Cordis와 Koishi가 이것이 종이 위 수식만이 아님을 보인다.

가장 인상 깊은 것은, 이 작업이 겨냥하는 미래다. 저자들이 결론에서 드는 향후 검증 방향은 자기진화형 에이전트 하니스다. AI 에이전트가 사람의 감독 거의 없이 자기 하니스 구성요소를 계속 생성하고 교체하는 환경 말이다. 이런 곳에서 "빠른 컴포넌트 교체 아래 완전한 회복"과 "잦은 위상 변화 아래 의존성 조율"이라는 두 보장이 진짜 값어치를 할 것이다. VSCode 확장 하나 못 빼서 재시작하던 문제에서 출발해, LLM 에이전트가 자기 자신을 안전하게 재구성하는 기초까지 겨눈 셈이다. 스케일이 큰 야심이다.

솔직히 92쪽을 다 읽고 나면 밀도에 지치는 것도 사실이다. 정의와 정리가 촘촘해서 한 번에 소화하기 어렵고, 검증이 정량적이지 않다는 아쉬움도 남는다. 그럼에도 동적 조합이라는, 우리가 매일 부딪히면서도 대충 프로세스 재시작으로 때우던 문제에 이만큼 진지한 형식적 언어를 준 논문은 드물다. 효과/코이펙트 시스템에 관심 있는 PL 연구자, 플러그인 아키텍처나 에이전트 하니스를 설계하는 시스템 엔지니어라면 곱씹어 볼 가치가 충분하다.

---

부록: Figure/Table 커버리지에 대한 메모

이 논문의 시각 자료는 다소 독특하다. 정식으로 번호가 붙은 그림은 Figure 1(컴포넌트 생명주기 상태 기계) 단 하나뿐이다. 파서가 추출한 나머지 이미지들은 성격이 다음과 같아 리뷰에 다음처럼 반영했다.

• DeepSeek 로고(figure_1.png): 논문 제목 상단의 발행 기관 로고로, 내용 그림이 아니므로 리뷰에 싣지 않았다.
• 효과 함수 가환 다이어그램 2점(Section 3.1.2): 번호 없는 인라인 수식 그림이지만 되돌릴 수 있는 효과의 핵심을 담고 있어 4.2절에 삽입하고 설명을 붙였다.
• Algorithm 3 리스팅(반응적 통지): 알고리즘이지만 파서가 이미지로 추출했고 반응성의 실현을 잘 보여주어 10.2절에 삽입했다.

표의 경우, 파서가 5개 표를 잡았으나 그중 2개는 목차(TOC)를, 1개는 Algorithm 8 리스팅을 표로 오인식한 것이다. 실제 내용 표는 **Table 1(규칙을 파이버 위의 쓰기로 읽은 표)**과 Table 2(이론-구현 대응표) 둘로, 두 표 모두 원문 대조를 거쳐 마크다운으로 재현했다(9절, 10절). 즉 논문의 실질 그림 1개와 실질 표 2개를 모두 커버했고, 이론을 보조하는 가환 다이어그램 2점과 알고리즘 리스팅 1점을 추가로 실었다.