모나드의 전파·순서를 넘어서, 효과의 생성과 처리에 대한 일반 이론을 제시한다. 자유/프리어 모나드와 상호작용 트리를 통해 의미 중간결과를 표준화하고, 상태·비결정성 등 구체 효과에 대한 법칙, 의미적 효과 핸들러와 언어 차원의 핸들러 구문 및 의미론을 소개한다.
URL: https://xavierleroy.org/control-structures/book/main014.html
Title: Chapter 12 Algebraic effects
모나드 이론(제11장)은 효과의 전파와 순서를 일반적으로 설명한다. 그러나 효과가 어떻게 생성되고 구현되는지는 말해주지 않는다. 각 모나드는 그에 특화된 연산과 구현을 개별적으로 제공할 뿐이다.
이 장에서 다루는 알제브라적 효과 이론은 특정 모나드의 세부에 독립적으로 효과의 생성과 처리에 대한 일반 이론을 제공함으로써 모나드 이론을 확장한다. 이 이론은 제10장에서 설명한 제어 연산자인 효과 핸들러의 영감과 형식적 토대를 제공한다.
모나딕 언어.이 절의 실행 예로, 제11.2의 계산 람다-미적분에 상태 모나드의 get과 set, 비결정성 모나드의 choose와 fail 연산을 장착해 보자.
Values: v::=c ∣ x ∣ λ x . M Computations: M, N::=v 1 v 2 ∣ if v then M else N ∣val v ∣ do x ⇐ M in N ∣get ℓ ∣ set ℓ v mutable state ∣choose M N ∣ fail nondeterminism
이 시점에서는 상태와 비결정성 모나드의 결합 의미론을 정하지 않았다. 실패 시 상태를 되돌릴 수도 있고, 반대로 상태를 보존한 채 선택 지점들 사이로 전달할 수도 있다. 효과적 연산을 해석하지 않은 채로도, do 바인딩, 함수 호출, 조건식 등을 평가할 수 있을까?
중간 결과. 위 질문에 긍정적으로 답하기 위해, 중간 결과 타입 R X를 정의한다. 이는 결국 X 타입의 값을 반환하는 get, set, choose, fail 연산의 모든 가능한 순서를 기술한다.
R X::=Pure: X → R X ∣Get: Loc → (Val → R X) → R X ∣Set: Loc → Val → R X → R X ∣Choose: R X → R X → R X ∣Fail: R X
이 타입은 연산마다 하나의 생성자와, 즉시 X 값을 반환하는 사소한 계산을 위한 Pure 생성자를 갖는다. 각 생성자의 R X 타입 인자 개수는 프로그램을 이어갈 수 있는 방법의 수와 같다. choose M N에는 두 가지(M 쪽, N 쪽), fail에는 0개(실행 중단), set에는 1개, get에는 읽는 위치의 가능한 값 개수만큼인데 이를 Val → R X 함수로 표현한다.
가능한 효과의 트리. 중간 결과는 프로그램이 수행할 수 있는 모든 효과를 트리 형태로 나타낸 것으로 볼 수 있다. 예를 들어 다음 프로그램을 보자:
choose(do _ ⇐ set ℓ 0 in do x ⇐ get ℓ in val(x+1)) (choose(val 0)fail)
그 중간 결과는 다음과 같은 트리이며, 노드에는 R 타입의 생성자가 들어 있다:
set과 get을 해석하지 않았으므로, set ℓ 0 이후에 get ℓ이 0만을 반환한다는 사실을 알 수 없다. 대신 get ℓ의 모든 가능한 값 x를 Get 노드의 서브트리로 고려하고, 각 x 값에 대해 val(x+1)을 특화한다.
중간 결과의 모나드. 중간 결과 타입 T X는 다음과 같이 정의되는 ret와 bind를 갖는 모나드다.
ret x= x bind(Pure v)f= f v bind(Get ℓ k)f= Get ℓ(λ v.bind(k ℓ)f) bind(Set ℓ v R)f= Set ℓ v(bind R f) bind(Choose R 1 R 2)f= Choose(bind R 1 f)(bind R 2 f) bind Fail f= Fail
즉, bind R f는 트리 R의 모든 잎 Pure x를 f x로 치환한다. 세 모나드 법칙이 성립함을 확인하기는 쉽다.
지시적 의미론.중간 결과를 이용해 모나딕 언어에 지시적(denotational) 의미론을 줄 수 있다. 타입 T X의 모나딕 계산 M의 의미 ⟦ M ⟧은 타입 R X의 중간 결과이다.
⟦ v 1 v 2 ⟧= v 1v 2 ⟦ if v then M 1 else M 2 ⟧= if vthen⟦ M 1 ⟧else⟦ M 2 ⟧ ⟦ val v ⟧= Pure v ⟦ do x ⇐ M 1 in M 2 ⟧= bind⟦ M 1 ⟧(λ x.⟦ M 2 ⟧) ⟦ get ℓ ⟧= Get ℓ(λ v.Pure v) ⟦ set ℓ v ⟧= Set ℓ v*(Pure()) ⟦ choose M 1 M 2 ⟧= Choose⟦ M 1 ⟧⟦ M 2 ⟧ ⟦ fail ⟧= Fail
여기서 값 v의 의미 v*는 다음과 같이 정의된다.
c* = c x* = x (λ x . M)* = λ x . ⟦ M ⟧
효과적 연산의 해석.지시적 의미론 ⟦ M ⟧은 get, set, choose, fail 연산의 의미에 독립적이다. 이 의미는 사후적으로 중간 결과를 “폴드” 순회하는 방식으로 정의될 수 있으며, 아래 run으로 표기한다.
선택 지점에서 스토어를 백트래킹하기로 한다면, run의 타입은 R X → Store → 𝒫(X)이며 다음과 같이 정의된다.
run(Pure v)s= {v} run(Get ℓ k)s= run(k(s ℓ))s run(Set ℓ v R)s= run R(s [ℓ ↦ v]) run Fail s= ∅ run(Choose R 1 R 2)s= run R 1 s ⋃ run R 2 s
하지만 선택 지점들 사이에 보존되는 단일 스토어를 선택할 수도 있다. 이 경우 run의 타입은 R A → Store → 𝒫(A) × Store이고, 다음과 같이 둔다.
run(Pure v)s= ({v}, s) run(Get ℓ k)s= run(k(s ℓ))s run(Set ℓ v R)s= run R(s [ℓ ↦ v]) run Fail s= (∅, s) run(Choose R 1 R 2)s= (V 1 ⋃ V 2, s 2) with run R 1 s = (V 1, s 1) and run R 2 s 1 = (V 2, s 2)
자유 모나드.제12.1절에서 사용한 중간 결과 타입 R X는 범주론의 보다 일반적인 구성인 자유 모나드(free monad)의 한 인스턴스다. 이는 다음 타입 R X로 서술할 수 있다.
R X::=Pure: X → R X ∣Op: F(R X) → R X
우리는 관심 있는 모든 연산을 묘사하기 위해 F(R X) 타입의 단일 인자를 받는 생성자 Op 하나만 둔다. 타입 생성자 F: Type → Type은 함자(functor)로서, 다음의 함자적 map 연산을 갖는다.
fmap: ∀ A, B,(A → B) → (F A → F B)
이는 임의의 함수 A → B를 F A → F B로 승격한다.
제12.1절의 R 타입을 다음과 같이 취해 복원할 수 있다.
F X=Get: Loc → (Val → X) → F X ∣Set: Loc → Val → X → F X ∣Choose: X → X → F X ∣Fail: F X
이에 대응하는 fmap 연산은 예상대로 다음과 같다.
fmap f(Get ℓ g)= Get ℓ(λ x . fmap f(g x)) fmap f(Set ℓ a)= Set ℓ(f a) fmap f(Choose a 1 a 2)= Choose(f a 1)(f a 2) fmap f Fail= Fail
함자 F 관점에서의 자유 모나드 제시는 fmap을 이용해 일반적으로 ret와 bind를 정의할 수 있게 한다.
ret v= Pure v bind(Pure v)f= f v bind(Op ϕ)f= Op(fmap(λ x.bind x f)ϕ)
프리어 모나드.Kiselyov and Ishii (2015)의 프리어 모나드는 모나딕 프로그램을 위한 중간 실행 결과 타입의 또 다른 일반적 구성이다.
R X=Pure: X → R X ∣Op: ∀ B, Eff B → (B → R X) → R X
여기서 Eff B는 결과 타입이 B인 효과들의 타입이다. 각 효과는 Eff 타입의 생성자에 해당한다. 새로운 효과를 추가하는 것은 OCaml의 사용자 정의 효과 표현(제10장)에서와 같이 Eff 타입에 새 생성자를 확장하는 것이다.
ϕ의 타입이 Eff B이면, Op ϕ k의 서브트리는 각 b : B에 대해 k b이다. B의 원소 수만큼 서브트리가 존재한다. 인자 k는 효과 ϕ의 연속체(continuation)로서, 효과의 반환 값을 인자로 받아 실행의 나머지를 묘사하는 서브트리를 생산한다.
예를 들어, 가변 상태와 비결정성을 위한 효과 생성자는 다음과 같다.
Get:Loc → Eff Val(가능한 값마다 하나의 서브트리) Set:Loc → Val → Eff unit(서브트리 하나) Fail:Eff empty(서브트리 없음) Flip:Eff bool(두 개의 서브트리)
choose 연산은 Flip 효과로 인코딩할 수 있다.
choose R 1 R 2≜Op Flip(λ b . if b then R 1 else R 2)
Eff 타입 생성자 관점의 프리어 모나드 제시는 ret와 bind도 일반적으로 정의할 수 있게 한다.
ret v= Pure v bind(Pure v)f= f v bind(Op ϕ k)f= Op ϕ(λ x.bind(k x)f)
bind를 정의하기 위해 더 이상 함자와 fmap이 필요 없음을 주목하라.
프리어 모나드에서의 효과 해석.프리어 모나드 항(term)이 기술하는 효과는 다음의 일반 “폴드”를 이용해 해석할 수 있다.
fold : (A → B)→ (∀ C, Eff C → (C → B) → B) → R A → B fold f g(Pure v)= f v fold f g(Op ϕ k)= g ϕ(λ x.fold f g(k x))
fold 해석은 순수 계산을 다루는 f와 효과를 다루는 g 두 함수를 인자로 받는다.
가변 상태와 비결정성의 경우, 선택 지점에서 상태를 백트래킹하는 해석은 다음을 취함으로써 얻어진다.
f: A → Store → 𝒫(A) f x s= {x} g: Eff B → (B → Store → 𝒫(A)) → Store → 𝒫(A) g(Get ℓ)k s= k(s ℓ)s g(Set ℓ v)k s= k()s [ℓ ↦ v] g Flip k s= k false s ⋃ k true s g Fail k s= ∅
다른 해석(선택 지점에서 상태를 보존하는 경우)은 연습으로 남긴다.
fold 정의에 드러난 _제어의 역전_에 주목하라. 구문상으로는 프로그램이 모나드의 연산들(get, set 등)을 호출하는 것처럼 보이지만, 실행상으로는 이 연산들의 구현(함수 g)이 필요할 때 프로그램을 평가하며, 연속체 k를 사용해 평가를 재시작한다.
상호작용 트리.상호작용 트리(Xia et al., 2020)는 프리어 모나드의 타입 R X를 공유도적(coinductive)으로 만든 버전이다. 상호작용 트리는 무한 가지를 가질 수 있으므로, 발산(종료하지 않는 계산)을 기술할 수 있다. 이는 다음 타입 정의를 유도적(유한 고정점) 대신 _공유도적(최대 고정점)_으로 해석함으로써 얻어진다.
R A=Pure: A → R A ∣Op: ∀ B, Eff B → (B → R A) → R A ∣Tau: R A → R A
생성자 Tau는 어떠한 효과도 수행하지 않는 한 걸음의 계산을 나타낸다. 조용한 발산(예: 무한 루프)은 무한한 Tau 단계 열로 표현된다.
⊥ = Tau⊥ 즉, ⊥ = Tau(Tau(Tau(⋯)))
무한 상호작용 트리는 무한히 많은 효과를 포함할 수도 있다. 다음 비결정적 프로그램을 보자.
let rec f() = if flip()then 0 else f()
그 상호작용 트리는 다음과 같다.
X = Op Flip(λ b . if b then Pure 0 else Tau X)
flip이 항상 false를 반환하는 경우에 해당하는 무한 가지가 하나 있다.
조용한 계산 단계를 나타내는 Tau는 조용한 발산을 포착하는 데 필요하지만, 수행된 조용한 단계 수만 다른 프로그램들이 서로 다른 상호작용 트리를 갖게 만든다. 이는 보통 바람직하지 않다. 따라서 상호작용 트리는 약한 비시밀러리티(weak bisimilarity) 까지 같다고 본다. 즉 유한 개의 Tau 단계를 제거한 것과 같다. 약한 비시밀러리티를 ≈로 쓰면,
Pure v ≈ Tau(Pure v) ≈ Tau(Tau(Pure v)) ≈ ⋯
하지만 Pure v ≉⊥ 이다. 왜냐하면 ⊥는 무한한 Tau 단계 열이기 때문이다.
이하에서는 “상호작용 트리”를 “프리어 모나드의 항(유도적으로 정의됨)” 또는 “Xia et al. (2020) 스타일의 상호작용 트리(공유도적으로 정의됨)”의 의미로 혼용한다.
이제 왜 자유 모나드가 ‘자유’이고, 알제브라적 효과가 ‘대수적’인지 이해하는 데 도움이 되는 몇몇 대수학 개념을 상기하자. 더 자세한 설명은 Bauer (2018)을 보라.
대수적 구조.군, 환, 모노이드 등과 같은 대수적 구조는 다음으로 서술된다.
예를 들어, 모노이드(또는 반군)는 (T, ε, ·)이며, 여기서
ε: T 항등 원소 ·: T → T → T 합성 연산자
그리고 다음 세 방정식이 성립한다.
ε · x= x left identity x · ε= x right identity (x · y) · z= x · (y · z)associativity
0: T 항등 원소 +: T → T → T 합성 −: T → T 역원 0 + x= x + 0 = x left and right identity (x + y) + z= x + (y + z)associativity (−x) + x= x + (−x) = 0 left and right inverse
이론과 모형.대수적 구조를 논할 때, 이론과 그 모형을 구분하는 것이 유용하다. _이론_은 단지 연산자의 시그니처(이름과 타입)와 그들이 만족해야 하는 방정식을 말한다. _모형_은 담지체와 방정식을 만족하는 연산들의 구체 정의다.
예컨대 모노이드의 이론은 다음과 같다.
ε: T ε · x= x · ε = x ·: T → T → T(x · y) · z= x · (y · z)
다음 구조들은 “모노이드이다.” 더욱 정확히는 모노이드 이론의 모형들이다.
(ℕ, 0, +)자연수와 덧셈 (ℝ, 1, ×)실수와 곱셈 (T → T, id, ∘)엔도함수와 합성
자유 모노이드.집합(“알파벳”) A가 주어졌을 때, A 위의 _자유 모노이드_는 (A*, ε, ·)이며
A = {1,2,3}이라면, “12”, “333”, “2”는 단어이며 다음이 성립한다.
12 · (333 · 2) = (12 · 333) · 2 = 123332
A를 포함하는 담지체를 가진 다른 모노이드들도 있다. 예컨대 위의 (ℕ, 0, +). 그러나 A 위의 자유 모노이드는 A를 포함하는 모든 모노이드 중 “가장 단순”하거나 “가장 제약이 약한” 것이다. 이 직관은 수학적으로 정밀화될 수 있다. A ⊆ B인 임의의 모노이드 (B, 0, +)에 대해, 자유 모노이드 (A*, ε, ·)를 (B, 0, +)로 사상하는 모노이드 준동형 Φ가 존재한다. Φ : A* → B는 다음과 같이 정의된다.
Φ(ε) = 0 Φ (a 1 a 2 … a n) = a 1 + a 2 + ⋯ + a n
이는 0을 시작값으로 리스트 a 1 a 2 … a n 위에 + 연산을 “폴드”한 것이다. Φ는 모노이드 준동형인데, 두 모노이드 연산과 교환하기 때문이다. Φ(ε) = 0은 정의로부터, Φ(w 1 · w 2) = Φ(w 1) + Φ(w 2)는 +의 결합법칙으로부터 따른다.
자유 모형.자유 모노이드와 그것의 모노이드 준동형에 의한 특징은 대수적 이론들에 대한 자유 모형의 일반 개념의 특수한 경우다.
이론 𝒯와 관심 원소들의 집합 X를 생각하자. X가 생성하는 𝒯의 _자유 모형_은 𝒯-모형 M과 함수 η : X → carrier(M)로서 다음을 만족한다:
임의의 다른 𝒯-모형 M′과 함수 η′ : X→ carrier(M′)에 대해, η′ = Φ ∘ η가 되도록 하는 유일한 준동형 Φ : M→ M′가 존재한다.
앞선 A가 생성하는 자유 모노이드의 예에서, 다른 모노이드는 A ⊆ B인 (B, 0, +)이고, η는 자명한 포함 A → A*, η′는 자명한 포함 A → B이다.
익숙한 대수적 구조에 대해 자유 모형을 구성해 보는 것은 유익하다. 예컨대 집합 X가 생성하는 자유 군은 X의 원소 x i ∈ X에 정수 계수 c i ∈ ℤ를 붙인 선형 결합 c 1 x 1 + ⋯ + c n x n의 집합, 달리 말해 각 x의 계수 c(x)를 돌려주는 함수의 타입 X → ℤ이며, 점별 연산으로 장착된다.
0≜λ x . 0 c 1 + c 2≜λ x . c 1(x) + c 2(x) − c≜λ x . −c(x) η(x)≜λ y . if y = x then 1 else 0
모나드의 대수 이론.제12.3절의 대수 이론 스타일로 모나드의 이론을 정의할 수 있다. 연산은 모나드에 특화된 각 효과 F(예: 상태 모나드의 get과 set)에 대해 ret, bind, F이다. 이들의 시그니처는 다음과 같다.
ret: X → T X bind: T X → (X → T Y) → T Y F: A → (B → T X) → T X if F: A → B
F의 경우, A는 효과 F의 인자 타입, B는 그 결과 타입이다. 따라서 F 연산은 효과의 인자(A 타입)와 결과를 받는 연속체(B → T X 타입)를 인자로 받는다.
위 시그니처는 대수 이론 개념을 다소 확장한다. 담지체가 단순 타입이 아니라 매개변수화 타입 T X이며, 연산이 함수들을 인자로 받기 때문이다. 그럼에도 제12.3절의 기본 개념들, 특히 구조들 사이의 준동형 개념은 여전히 적용된다.
모나드 이론의 방정식은 세 가지 모나드 법칙에 더해 F와 bind 사이의 교환 법칙이다. (특정 효과를 특징짓기 위해 더 많은 방정식을 추가할 수 있다. 제12.5절 참조.)
bind(ret v)f= f v bind M ret= M bind(bind M f)g= bind M(λ x. bind(f x)g) bind(F x k)g=F x(λ y . bind(k y)g)
자유 모나드는 ‘자유’이다.제12.2절의 자유 모나드와 프리어 모나드는 위 모나드 이론의 모형임을 쉽게 볼 수 있다. 이하에서는 프리어 모나드에 집중한다. 담지체 T는 다음의 상호작용 트리에 대한 유도적 타입이다.
T A=Pure: A → T A ∣Op: ∀ B,Eff B → (B → T A) → T A
특정 연산 F는 Eff 타입의 생성자들이다. ret, bind, F 연산은 다음과 같이 정의된다.
ret v= Pure v bind(Pure v)f= f v bind(Op(F x)k)f= Op(F x, λ y. bind(k y)f) F x k= Op(F x, k)
네 개의 이론 방정식은 bind 정의에서 쉽게 따른다. 따라서 프리어 모나드는 모나드 이론의 모형이다.
이제 프리어 모나드가 관심 효과 집합 F에 의해 생성되는 자유 모형임을 보이자. 동일한 효과 집합 F에 대해 다른 모형 M = (T′, ret′, bind′, F′)를 생각하자. 프리어 모나드에서 M으로의 준동형 Φ를 다음과 같이 정의한다.
Φ: T X → T′X Φ(Pure v)= ret′v Φ(Op(F x)k)=F′x Φ(k) where Φ(k) = λ y . Φ(k y)
이 준동형은 모나드 연산들과 교환한다. ret와 F의 경우 정의로부터 즉시 따른다.
Φ(ret v)= Φ(Pure v) = ret′v Φ(F x k)= Φ(Op(F x, k)) =F′x Φ(k)
bind의 경우, 상호작용 트리에 대한 귀납 및 케이스 분석으로 보인다.
Φ(bind(Pure v)f)= Φ(f v)(def.) = bind′(Φ(Pure v))Φ(f)(1st law) Φ(bind(Op(F x)k)f)= Φ(Op(F x, λ y. bind(k y)f))(def.) =F′x(λ y. Φ(bind(k y)f)))(def.) =F′x(λ y. bind′(Φ(k y))Φ(f))(ind.hyp.) = bind′(F′x Φ(k))Φ(f)(4th law) = bind′Φ(Op(F x)k)Φ(f)(def)
모나드의 대수적 제시에 기초하여, 이제 Moggi의 계산 람다-미적분처럼 효과의 전파만이 아니라 효과의 생성까지 설명하는 작은 언어를 정의한다.
언어는 효과를 수행하는 하나의 구문을 덧붙여 계산 람다-미적분을 확장한다.
Values: v::=x ∣ c ∣ λ x.M Computations: M, N::=v v′application ∣if v then M else N conditional ∣val v trivial computation ∣do x ⇐ M in N sequencing ∣F(v; y . M)performing an effect
계산 F(v; y . M)은 인자 v(0개 이상)의 효과 F를 수행한다. 효과는 결과 값을 만들어내며, 이는 연속체 M에서 y에 바인딩된다.
F(v )를 F(v; y . val(y))의 약기호로 쓴다. 즉, 효과의 값을 즉시 반환하는 사소한 연속체와 함께하는 효과 F이다.
일반 법칙들.제11.2절과 같은 접근으로, 대수적 효과의 언어에 두 계산의 동등성을 보이기 위한 _등식 이론_을 부여한다. 이 이론은 다음과 같은 일반 법칙들을 포함한다.
(λ x . M)v≡ M x := v if true then M else N≡ M if false then M else N≡ N do x ⇐ val v in M≡ M x := v do x ⇐ M in val x≡ M(M2) do x ⇐ (do y ⇐ M in N) in P≡ do y ⇐ M in(do x ⇐ N in P)(M3) do x ⇐ F(v; y . M) in N≡ F(v; y . do x ⇐ M in N)(M4)
처음 여섯 법칙은 계산 람다-미적분의 것이며, (M1), (M2), (M3)는 익숙한 모나드의 세 법칙을 반영한다. 마지막 (M4)는 제12.4절의 대수적 모나드 제시에서 오며, 효과 F를 수행한 뒤 그 결과를 바인딩하는 두 가지 방법을 동일시한다. 특히 (M4)와 (M1)에서 다음이 따른다.
F(v; y . M) ≡ do y ⇐ F(v ) in M
일부 효과 계열에서는 위 법칙들이 완전하다. 즉, 다른 등가성은 성립하지 않는다. 이는 입출력 효과(출력과 입력)처럼 서로 결합하거나 소거되지 않는 경우가 해당된다. Plotkin and Power (2003)의 깊은 통찰은, 가변 상태나 비결정성 같은 다른 효과들은 등식 이론에 특정 법칙을 추가함으로써 특징지을 수 있다는 점이다.
가변 상태의 법칙들.가변 상태를 구현하는 get과 set 효과는 풍부한 등식 이론을 갖는다. 먼저 위치 ℓ에 값 v를 쓴 뒤에는 ℓ에는 v가 담기고 ℓ′ ≠ ℓ인 다른 위치는 변하지 않는다. 이른바 “좋은 변수 성질”은 다음 두 법칙으로 포착된다.
set(ℓ, v; _ . get(ℓ; z . M))≡ set(ℓ, v;_. M [z := v]) set(ℓ, v; _ . get(ℓ′; z . M))≡ get(ℓ′; z . set(ℓ,v; _ . M)) if ℓ′ ≠ ℓ
이 두 법칙만으로도 상태 있는 프로그램을 실행하여 최종 값을 결정할 수 있다. 예컨대 ℓ′ ≠ ℓ라고 가정하면,
do _ ⇐ set(ℓ, 0) in do _ ⇐ set(ℓ′, 1) in get(ℓ) ≡do _ ⇐ set(ℓ, 0) in get(ℓ; x . do _ ⇐ set(ℓ′, 1) in val x)) ≡do _ ⇐ set(ℓ, 0) in do _ ⇐ set(ℓ′, 1) in val 0
가변 상태를 완전히 특징짓기 위해서는 다음 법칙들을 추가해야 한다.
get(ℓ; y . get(ℓ′; z . M))≡ get(ℓ′; z . get(ℓ; y . M)) set(ℓ, v; y . set(ℓ′, v′; z . M))≡ set(ℓ′, v′; z . set(ℓ, v; y . M)) if ℓ′ ≠ ℓ get(ℓ; y . get(ℓ; z . M))≡ get(ℓ; y . M [z := y])(double read) get(ℓ; y . set(ℓ, y; _ . M))≡ M(read then rewrite) set(ℓ, v 1; _ . set(ℓ, v 2; _ . M))≡ set(ℓ, v 2; _ . M)(double write)
비결정성의 법칙들.비결정성 모나드의 fail과 choose 연산 역시 풍부한 등식 이론을 가진다. 첫째, fail은 그 연속체를 무시하므로 흡수적이다.
fail( ; y . M) = fail( ) for all M
둘째, fail은 choose의 항등원이다.
choose M fail( ) = choose fail( )M = M(identity)
셋째, choose는 멱등, 교환, 결합이 성립한다.
choose M M= M(idempotent) choose M N= choose N M(commutative) choose(choose M N)P= choose M(choose N P)(associative)
우리 언어에서 choose M N은 flip(, y . if y then M else N)으로 인코딩되며, flip은 true나 false를 비결정적으로 반환하는 효과다. 그러므로 위 법칙들은 flip에 대한 법칙으로 읽혀야 하지만, 그 경우 읽기 훨씬 어렵다.
위 법칙들은 choose가 합(조인) 연산, fail이 항등원인 _반격자(semilattice)_의 법칙이다. 이들은 비결정성 모나드를 결과 집합들로 구현하는 것에 대응한다. 반면 Haskell의 리스트 모나드처럼 결과 리스트를 사용할 때에는 결과의 순서와 중복이 중요해진다. 따라서 “멱등”과 “교환” 법칙은 제거해야 한다. 남는 법칙들은 choose를 합성 연산, fail을 항등원으로 하는 _모노이드_의 법칙이다.
지시적 의미론.각 계산 M에 상호작용 트리 ⟦ M ⟧을 대응시킨다.
⟦ v 1 v 2 ⟧= v 1v 2 or Tau(v 1v 2) ⟦ if v then M 1 else M 2 ⟧= if vthen⟦ M 1 ⟧else⟦ M 2 ⟧ ⟦ val v ⟧= Pure v ⟦ do x ⇐ M 1 in M 2 ⟧= bind⟦ M 1 ⟧(λ x.⟦ M 2 ⟧) ⟦ F(v; y . M) ⟧= Op(F v)(λ y.⟦ M ⟧)
일반 재귀와 부분성을 지원하려면, 함수 적용처럼 발산이 일어날 수 있는 곳에 Tau 단계를 추가하고 공유도적 상호작용 트리를 사용해야 한다. 그렇지 않다면 유도적 상호작용 트리로 충분하다.
계산 M의 실행 결과를 얻기 위해, 제12.2절의 트리에 대한 “폴드” 연산을 사용해 트리 ⟦ M ⟧을 적절한 모나드에서 해석한다.
run M ≜ fold f g⟦ M ⟧
여기서 f와 g는 상호작용 트리의 생성자 Pure와 Op에 대한 해석을 제공한다.
이 의미론이 등식 이론의 법칙들을 만족함을 확인하기는 쉽다. 즉, M ≡ N이면 run M = run N이다. 일곱 개의 일반 법칙에 대해서는 더 강한 결과가 있다. M ≡ N이면 ⟦ M ⟧ = ⟦ N ⟧이다. 이는 ⟦ · ⟧의 정의와 상호작용 트리 위의 bind 정의로부터 따른다.
특정 효과에 특화된 법칙의 경우, fold와 해석 함수 f, g의 정의도 함께 사용한다. 예컨대 비결정성의 경우 다음과 같이 정의한다.
f x= {x} g fail k= ∅ g flip k= k false ⋃ k true
그러면 약간의 단순화 후, 위의 비결정성 법칙들은 합집합의 기초적 성질들로부터 따른다.
X ⋃ ∅= ∅ ⋃ X = X(identity) X ⋃ X= X(idempotent) X ⋃ Y= Y ⋃ X(commutative) X ⋃ (Y ⋃ Z)= (X ⋃ Y) ⋃ Z(associative)
마찬가지로, 가변 스토어에 대한 법칙들은 스토어 전달 구현에서의 표준적인 스토어 갱신 성질들로부터 따른다.
제12.2절과 제12.5절에서, 계산 M이 수행하는 효과를 나타내는 상호작용 트리 ⟦ M ⟧은 다음의 해석 함수 f, g를 트리 위로 “폴드”하여 선택한 모나드에서 해석되었다.
fold : (A → B)→ (∀ C, Eff C → (C → B) → B) → R A → B fold f g(Pure v)= f v fold f g(Op ϕ k)= g ϕ(λ x.fold f g(k x))
지금까지는 모든 효과를 한 번에 처리하여 프로그램의 최종 의미를 직접 산출하는 단일 “폴드”를 택했다. 그러나 그러한 “폴드”는 결과로 단순화된 상호작용 트리를 만들어낼 수도 있다. 상호작용 트리를 상호작용 트리로 변환하는 이러한 변환을 의미적 효과 핸들러(semantic effect handler), 줄여서 _효과 핸들러_라 부르자.
효과 핸들러는 합성될 수 있다. 이를 통해 핸들러가 효과의 부분집합만 처리하고, 나머지 효과는 결과에서 그대로 남겨둘 수 있다. 핸들러가 어떤 효과를 다른 효과들로 번역하여 구현하기로 선택할 수도 있다. 두 경우 모두, 남은 효과들을 해석할 수 있는 다른 핸들러와의 합성을 기대한다.
예를 들어, 가변 상태를 구현하는 get과 set 효과를 위한 핸들러는 다음과 같다.
state: R A → Store → R A = fold f state g state f state v= λ σ . Pure v g state(get ℓ)k= λ σ . k σ(ℓ)σ g state(set ℓ v)k= λ σ . k()σ [ℓ ↦ v] g state ϕ k= λ σ . Op ϕ(λ x.k x σ) for all other effects ϕ
이 핸들러는 스토어 σ를 매개변수로 추가하고, 이를 사용해 get을 스토어 접근으로, set을 스토어 갱신으로 해석한다. 결과 상호작용 트리에는 따라서 get이나 set 효과가 남지 않는다. 다른 모든 효과 ϕ는 결과 트리에서 재발행되며 스토어는 변경되지 않는다.
또 다른 예로, 비결정성을 구현하는 fail과 flip 효과를 위한 핸들러는 다음과 같다.
nondet: R A → R(𝒫(A)) = fold f nondet g nondet f nondet v= Pure{v} g nondet fail k= Pure∅ g nondet flip k=bind(k true)(λ x 1 . bind(k false)(λ x 2 . Pure(x 1 ⋃ x 2))) g nondet ϕ k= Op ϕ k for all other effects ϕ
상태와 nondet 핸들러를 합성하는 방법은 두 가지가 있다.
run 1 t σ = nondet(store t σ) run 2 t σ = store(nondet t)σ
타입 R A의 트리 t가 주어졌을 때, 두 합성 모두 타입 R(𝒫(A))의 트리를 반환한다. 더구나 t가 get, set, fail, flip 외의 효과를 포함하지 않는다면, 두 합성 모두 최종 결과 집합 s를 산출하는 사소한 트리 Pure s를 반환한다. 그러나 두 합성은 비결정성 하에서 상태의 의미론을 서로 다르게 구현한다. run 1은 fail 때문에 flip이 재실행될 때 스토어를 백트래킹하고, run 2는 실행 전체에 걸쳐 단일 스토어를 스레딩한다.
효과 핸들러를 제어 연산자로 발견하게 한 두 번째 깊은 통찰은 Plotkin and Pretnar (2013)의 것이다. 그들은 상호작용 트리 변환기로서의 효과 핸들러 아이디어를 제시했을 뿐 아니라, 제12.5절의 대수적 효과 언어에 소규모 확장을 가해 이 효과 핸들러들을 프로그램 안에서 정의할 수 있음을 보였다.
Values: v::=x ∣ c ∣ λ x.M Computations: M, N::=v v′ ∣if v then M else N ∣val v ∣do x ⇐ M in N ∣F(v; y . M) ∣with H handle M(effect handler) Handlers: H::={val(x) → M val; F 1(x; k) → M 1; ⋮ F n(x; k) → M n }
새 구문 with H handle M은 계산 M이 수행하는 일부 효과를 핸들러 H가 서술한 대로 처리한다. 표12.1은 M이 정상 종료하는지, 효과 F i를 수행하는지, 다른 효과를 수행하는지에 따라, 그리고 얕은(shallow) 의미론과 깊은(deep) 의미론 중 무엇을 쓰는지에 따라 이 구성의 비공식 의미를 보여준다.
M의 동작 Shallow handling Deep handling 정상값 v로 종료 M val을 평가. 단,
x = v M val을 평가. 단,
x = v 효과 F i(v; y . N) 수행 M i를 평가. 단,
x = v 그리고
k = λ y . N M i를 평가. 단,
x = v 그리고
k = λ y . with H handle N 효과 F(v; y . N) 수행, 단 F ∉ {F 1, …, F n} 동일 효과를 수행 동일 효과 F(v; y . with H handle N) 수행
표 12.1: with H handle M의 동작. 여기서 H = { val(x) → M val; …; F i(x; k) → M i; … } .
효과 핸들러의 지시적 의미론.효과 핸들러의 의미 ⟦ H ⟧는 상호작용 트리 변환기이므로, with 구성의 지시적 의미론은 이 변환기의 적용이 된다.
⟦ with H handle M ⟧ = ⟦ H ⟧⟦ M ⟧
이 변환기는 깊은 처리의 경우 트리 위의 “폴드” 순회이고, 얕은 처리의 경우 트리 꼭대기에서의 “케이스” 분석이다.
⟦ H ⟧ =⎧ ⎨ ⎩fold⟦ H ⟧ret⟦ H ⟧eff(deep handler) case⟦ H ⟧ret⟦ H ⟧eff(shallow handler)
“폴드”와 “케이스”의 차이는 정의와 타입 양쪽에 분명히 드러난다.
fold : (A → B)→ (∀ C,Eff C → (C → B) → B) → R A → B case : (A → B)→ (∀ C,Eff C → (C → A) → B) → R A → B fold f g(Pure v)= case f g(Pure v) = f v fold f g(Op ϕ k)= g ϕ(λ x.fold f g(k x)) case f g(Op ϕ k)= g ϕ k
핸들러 H = { val(x) → M val; F 1(x; k) → M 1; …; F n(x; k) → M n }에 대해, 정상 종료에 대한 의미 ⟦ H ⟧ret와 처리되지 않은 효과에 대한 의미 ⟦ H ⟧eff는 다음과 같다.
⟦ H ⟧ret x= ⟦ M val ⟧ ⟦ H ⟧eff(F i x )k= ⟦ M i ⟧for i = 1, …, n ⟦ H ⟧eff(F x )k= Op(F x )k if F ∉ {F 1, …, F n}
Bauer (2018)의 강의 노트는 이 장에서 다룬 것보다 더 자세히 알제브라적 효과와 핸들러의 대수적 성격을 설명한다.
Plotkin and Power (2008)가 보였고 Bauer (2018)의 4절에서 다시 설명된 바와 같이, 효과의 공대수적(coalgebraic) 해석은 프로그램 밖에서 수행되어 프로그램이 롤백할 수 없는 I/O 같은 “하드웨어/현실 세계” 효과를 설명하는 데 쓰일 수 있다. 이때 계산의 완전한 의미는 “소프트웨어” 효과의 모형과 “하드웨어” 효과의 코모형 사이의 텐서곱으로 기술된다.
알제브라적 효과 이론은 본성상 “1계”로, 인자에 계산(값만이 아니라)을 받는 효과적 연산을 다루지 않는다. 비결정성 모나드의 choose M N은 if flip then M else N으로 인코딩해 다룰 수 있다. 그러나 예외 모나드의 trywith 연산은 1계 효과로 표현할 수 없다. 이러한 고계 효과를 다루기 위한 여러 이론이 제안되었는데, Yang et al. (2022)의 스코프드 효과(scoped effects) 등이 그 예다.
