대수적 효과와 효과 핸들러를 행 다형성과 함께 사용해 확장 가능한 효과와 핸들러를 모듈식으로 구현하는 방법을 Links 언어를 통해 설명하고, 핵심 계산과 추상 기계 의미론까지 제시한다.
The University of Edinburgh, UK
The University of Edinburgh, UK
대수적 효과(algebraic effects)와 효과 핸들러(effect handlers)는 효과가 있는 프로그래밍을 위한 모듈식 추상화를 제공한다. 이들은 Haskell처럼 사용자 정의 효과를 지원하면서도 ML처럼 직접 스타일(direct-style)의 효과적 프로그래밍을 가능하게 한다. 또한 한정된 연속(delimited continuations)을 이용한 프로그래밍에 구조화된 인터페이스를 제공한다. 모듈성을 확보하려면 효과 타입 시스템이 확장 가능한 효과(extensible effects) 를 지원해야 한다. 행 다형성(row polymorphism) 은 타입 수준에서 확장성을 모델링하기 위한 자연스러운 추상화이다.
본 논문에서는 확장 가능한 효과와 그 핸들러를 구현하는 데 필요한 추상화가 정확히 행 다형성이라고 주장한다. 우리는 이 주장을 뒷받침하기 위해 Links 함수형 웹 프로그래밍 언어를 플랫폼으로 사용한다. Links는 다형적 변이(polymorphic variants), 레코드, 그리고 내장 효과 타입에 행 다형성을 이미 사용하며, 연속(continuations)을 조작하는 인프라도 갖추고 있기 때문에 자연스러운 출발점이다.
Links에 작은 확장을 더해 효과 핸들러를 매끄럽게 추가하며, 프론트엔드에서는 행을 본질적으로 활용하고 백엔드에서는 일급 연속(first-class continuations)을 활용한다. 우리는 수학 게임 Nim을 추상 계산으로 모델링하여 구현의 사용성을 보이고, 이를 여러 방식으로 해석함으로써 행과 핸들러가 효과적 계산의 모듈성과 부드러운 합성을 어떻게 지원하는지 보여준다.
또한 Links의 중간 표현(IR)에 사용되는 A-정규형(A-normal form)의 변형에 기반하여, 행-다형적 효과와 핸들러의 핵심 계산(core calculus)을 제시한다. 이 계산에 대한 연산적 의미론(operational semantics)과, 이를 구현하는 CEK 기계의 새로운 일반화(abstract machine semantics)를 제시하고, 두 의미론이 일치함을 증명한다.
분류 및 주제 분류 D.3.3 [언어 구성 요소와 특징]; F3.2 [프로그래밍 언어 의미론]
키워드 대수적 효과; 효과 핸들러; 효과 타이핑; 추상 기계 의미론; 연산적 의미론; 한정 제어(delimited control)
대수적 효과 [29]와 효과 핸들러 [30]는 사용자 정의 계산 효과 [6, 15, 17]를 관리하기 위한 모나드(monads)보다 더 모듈식인 대안이다. 효과 핸들러는 예외 핸들러를 일반화하여 임의의 대수적 효과를 해석하는 메커니즘을 제공하며, 한정된 연속을 이용한 프로그래밍에 구조화된 인터페이스를 제공한다.
간단한 예로, 다음과 같은 단일 효과 연산을 갖는 선택(choice) 효과를 생각하자.
Choose : Bool
우리는 Choose의 의미를 지정하지 않은 채로도 Choose를 호출하는 추상 계산 M을 작성할 수 있다. 그리고 M을 여러 방식으로 처리(handle)할 수 있다. 예를 들어, allResults라는 핸들러를 정의하여 연산을 비결정적 선택으로 해석하고, M의 가능한 모든 결과의 리스트를 반환하도록 할 수 있다. 또는 coin이라는 다른 핸들러를 정의하여 Choose를 무작위 선택으로 해석하고, M 내에서 수행된 모든 무작위 선택에 의존하는 단일 값을 반환할 수도 있다.
효과 핸들러가 프로그래밍 추상화로서 진가를 발휘하는 지점은 합성(composition) 을 시작할 때이다. 우리는 어떤 효과는 처리하고 다른 효과는 모두 전달(forward)할 수 있으며, 이때 전달되는 효과를 타입 수준에서 행 타입(row types)으로 정적으로 추적할 수 있다. 2절에서는 핸들러 합성을 광범위하게 사용한다.
효과 핸들러의 많은 기존 구현은 Haskell 라이브러리 형태이다. 대표적으로 Kammar 등 [15]의 effect handlers 라이브러리, Kiselyov 등 [17] 및 Kiselyov와 Ishii [16]의 extensible effects 라이브러리, 그리고 Swierstra의 data types à la carte 기법 [34]의 변형에 기반한 구현(예: Wu 등 [36]의 scoped effect handlers)이 있다. 또 다른 주목할 라이브러리로 Idris effects 라이브러리 [6]가 있다. 이들 라이브러리는 모두, 결국 제한된 형태의 행 다형성에 해당하는 추상화를 각기 정교하게 인코딩한다.
본 연구에서는(우리가 알기로는) 최초로, Remy 스타일 행 다형성 [33]을 실제로 사용하여 효과 핸들러를 구현한다.
Links [8]는 웹 애플리케이션을 만들기 위한 함수형 프로그래밍 언어이다. Links의 특징은 클라이언트, 서버, 데이터베이스의 웹 애플리케이션 3계층을 단일 소스 언어로 타깃한다는 점이다. Links 소스 코드는 A-정규형 [11] 기반의 중간 표현(IR)으로 변환된다. 클라이언트에서는 IR이 JavaScript로 컴파일되고, 서버에서는 IR이 CEK 기계 [10]의 변형으로 해석(interpreted)된다. 데이터베이스에서는 IR이 SQL 질의로 변환되는데, 효과 타입 시스템과 부분식 성질(subformula property)을 이용해 질의 생성 가능성을 보장한다 [22].
Links는 엄격(strict) 언어이며 Hindley-Milner 타입 추론을 사용한다. Links는 다형적 변이, 레코드, 그리고 동시성 및 데이터베이스 통합을 위한 내장 효과 타입에 대해 행 타입 시스템을 제공한다 [8, 22]. 또한 일급 연속을 조작하는 기능을 지원하는데, 이는 효과 핸들러 구현의 핵심이다.
행-다형적 효과 타입 시스템과 연속 지원은 Links를 행 기반 대수적 효과와 효과 핸들러를 실험하기 위한 자연스러운 선택으로 만든다. 우리는 Links에 효과 핸들러 확장을 구현했으며, 현재는 서버 측에서만 지원된다. 프론트엔드는 행 다형성을 본질적으로 활용하고, 백엔드는 CEK 기계의 새로운 일반화로 구현된다.
본 논문의 주요 기여는 다음과 같다.
• Remy 스타일 행 다형성 [33]을 사용한 효과 핸들러 구현.
• 구현의 사용성을 보여주는 시연: 행과 핸들러가 효과적 계산의 모듈성과 매끄러운 합성을 어떻게 지원하는지 설명.
• 구현의 형식화: 작은 단계(call-by-value) 연산적 의미론과, 효과 핸들러를 고려하도록 CEK 기계를 일반화한 추상 기계 의미론.
• 작은 단계 의미론과 추상 기계 의미론 사이의 강한 대응 증명: 연산 의미론의 모든 감소는 추상 기계에서 일련의 행정적 단계(administrative steps) 후 β-단계 하나로 대응됨.
나머지 논문의 구성은 다음과 같다. 2절은 Links에서 핸들러로 프로그래밍하는 튜토리얼 소개를 제공한다. 3절은 핵심 계산 λρ^eff(“lambda-eff-row”)와 타입-효과 시스템, 작은 단계 의미론을 제시한다. 4절은 연산 의미론을 구현의 본질을 포착하는 추상 기계 의미론과 연결한다. 5절은 구현 세부 사항을 논의한다. 6절은 관련 연구를 논의한다. 마지막으로 7절은 결론과 향후 과제를 제시한다.
행과 핸들러가 효과적 프로그래밍을 위한 우아하고 모듈적인 추상화를 제공함을 보이기 위해, 우리는 수학 게임 Nim [5]의 단순화된 버전을 예제로 사용한다. 게임의 추상 표현에서 시작해, 초기 표현을 변경하지 않고도 핸들러의 매끄러운 합성으로 치트 탐지와 하이스코어 추적 기능을 점진적으로 확장한다.
Nim은 두 명의 플레이어 Alice와 Bob이 하는 게임이다. 게임은 n개의 막대기(sticks)가 있는 더미(heap)로 시작한다. 플레이어들은 번갈아가며 더미에서 1개, 2개, 또는 3개의 막대기를 가져간다. Alice가 먼저 시작한다. 마지막 막대기를 가져가는 사람이 승리한다.
우리는 “수(手)를 두는 것”을 추상화하기 위해, 이를 추상 효과 연산으로 정의한다:
Move:(Player,Int) {}-> Int
여기서 Player는 두 생성자 Alice와 Bob을 가진 변이 타입이다. Move의 첫 번째 매개변수는 현재 플레이어, 두 번째는 현재 더미에 남은 막대기 수이다. 화살표 앞의 중괄호({}) 접두가 무엇을 의미하는지는 곧 설명한다.
Links에서는 Move 같은 추상 연산을 do 기본 프리미티브로 호출한다. 예를 들어:
do Move(Alice,3)
은 값 Alice와 3을 인자로 Move 연산을 호출한다.
연산 이름, 데이터 생성자, 타입 별칭은 모두 대문자로 시작한다. 레코드, 변이, 효과 시그니처 모두 행 타입을 가진다. Links의 타이핑은 구조적(structural)이라서, 연산 같은 행 구성원을 사용 전에 선언할 필요가 없다. 다만 연산 호출을 함수로 감싸는 것이 좋은 관행이다. 이는 효과를 함수와 매끄럽게 합성할 수 있게 해주며, 단순 호출 이상의 일을 하고 싶을 때도 있기 때문이다(2.4절에서 예시를 본다).
우리는 Move를 다음과 같이 감싼다.
sig move : (Player,Int) {Move:(Player,Int) {}-> Int|e}-> Int fun move(p,n) {do Move(p,n)}
Links 문법은 JavaScript를 느슨하게 따른다. fun 키워드는 함수 정의를 시작한다(JavaScript의 function처럼). JavaScript처럼 함수는 n-항이지만 커리될 수도 있다. JavaScript와 달리 함수는 정적 타입을 가지며, sig 키워드는 타입 시그니처를 시작한다.
함수 move는 인자 p와 n으로 Move 연산을 호출한다. 타입 시그니처에서 함수 화살표(->) 앞의 중괄호 안 행은 효과 시그니처(effect signature) 또는 효과 행(effect row) 이다. 효과 행에 Move가 존재한다는 것은 함수가 Move 연산을 수행할 수 있음을 뜻한다. 또한 효과 행에는 효과 변수 e가 포함되어 있어 추가 연산들로 인스턴스화될 수 있다. 즉 move는 추가 효과들이 있는 스코프에서 호출될 수 있다.
효과 행은 효과 변수가 없으면 닫힌(closed) 행이고, 있으면 열린(open) 행이다. 일반적으로 효과 행은 순서 없는 연산 명세들의 컬렉션과 선택적 효과 변수로 구성된다. 연산 명세는 해당 연산이 허용(존재)되는지와 그 타입 시그니처를 지정하거나, 부재(absent)함을 지정하거나, 존재 여부에 대해 다형적임을 지정한다. 부재의 사용은 2.5절에서 논의한다.
Move 연산 자체의 효과 행은 빈 행 {}로 표기된다. 이는 추상 연산이 어떤 효과를 갖더라도 최종적으로는 핸들러가 의미를 부여하기 때문이며, 추상 연산 자체는 항상 빈 효과를 가진다.
Nim 게임은 서로 재귀인 두 함수 aliceTurn과 bobTurn으로 모델링된다. 여기서는 aliceTurn만 보인다.
sig aliceTurn : (Int) {Move:(Player,Int) {}-> Int|_} ~> Player fun aliceTurn(n) { if (n <= 0) Bob else bobTurn(n - move(Alice,n)) }
n은 현재 더미의 막대기 수이다. n이 0이면 Bob이 승리한다. 그렇지 않으면 Alice가 수를 두고 Bob의 차례가 된다. bobTurn은 완전히 대칭적이므로 생략한다.
aliceTurn의 효과 시그니처에서 두 가지를 관찰할 수 있다.
효과 변수는 익명(_)이다. 타입(또는 효과) 변수는 한 번만 등장하면 이름을 붙일 필요가 없다.
함수 화살표가 물결(~>)이다. 이는 계산이 wild 효과를 가진다는 것을 나타내는 문법 설탕이다. wild 효과는 I/O, 무작위성, 발산(divergence) 등 모든 내재적(intrinsic) 효과를 포괄한다. 이는 어느 정도 Haskell의 IO 모나드와 유사하지만, 일반 재귀를 허용하지 않는다는 점에서 더 엄격하다. 현재 구현에서는 내재적 효과를 핸들러가 처리할 수 없고, 인터프리터가 미리 정의된 해석을 부여한다.
Links는 엄격 평가를 사용하므로, 처리하고 싶은 계산은 thunk로 감싸고 다음 타입 별칭을 정의한다.
typename Comp(e::Row,a) = () { |e} ~> a;
typename 키워드는 타입 별칭을 정의한다. Comp 타입은 우리의 “추상 계산” 개념을 포착한다. 이는 열린 효과 행 e와 반환 타입 a를 갖는 thunk의 별칭이다. e::Row는 타입 변수 e의 종류(kind)가 Row임을 뜻한다.
게임 함수는 주어진 막대기 수로 게임을 시작한다. Alice가 시작한다.
sig game : (Int) -> Comp({Move:(Player,Int) {}-> Int|_}, Player) fun game(n)() {aliceTurn(n)}
일반적으로 대수적 효과는 방정식(equations) [29]을 갖지만, 대부분의 효과 핸들러 구현과 마찬가지로 우리는 방정식을 고려하지 않는다. 따라서 추상 연산은 그 자체로 의미가 없고, 핸들러가 의미론을 부여한다.
핸들러로 Move 연산을 해석해 Alice와 Bob의 특정 전략을 인코딩할 수 있다. 완벽 전략(perfect strategy)은 다음과 같이 정의된다.
ps(n) = max {1, n mod 4}
여기서 n은 남은 막대기 수이다. 플레이어 p가 완벽 전략을 채택하면, p의 차례에 n이 4로 나누어떨어지지 않으면 p의 승리가 보장된다.
양쪽 플레이어 모두에게 완벽 전략을 부여하는 핸들러 pp(perfect-vs-perfect)를 정의한다.
1 sig pp : (Comp({Move:(Player,Int) {}-> Int|e}, a)) -> 2 Comp({Move-|e}, a) 3 fun pp(m)() { 4 handle(m) { 5 case Return(x) -> x 6 case Move(p,n,k) -> k(maximum(1, n 'mod' 4)) 7 } 8 }
라인별 설명은 다음과 같다.
1–2행: pp의 타입. Move를 호출할 수 있는 계산을 받아, Move가 부재(Move-)인 계산을 반환한다. 반환 타입은 a이다. 타입 시스템이 추론할 수 있으므로 생략해도 된다.
3–4행: 정의 시작. 커리된 함수 pp는 실제 핸들러를 thunk로 감싼다. handle 구문은 추상 연산을 일련의 절로 해석하는 방법을 지정한다.
5행: 반환 절(return clause). 입력 계산의 최종 반환 값을 처리하는 방법을 정의한다. 여기서는 그대로 반환한다.
6행: 연산 절(operation clause). Move를 처리한다. 일반적으로 연산 절은 Op(p1,...,pn,k) -> M 형태인데, p1..pn은 연산 인자에 대한 패턴, k는 계산의 연속(continuation)을 바인딩하는 패턴이다. 여기서는 p와 n이 각각 현재 플레이어와 남은 막대기 수에 바인딩된다. 연속 k는 플레이어와 무관하게 완벽 전략 값으로 호출된다.
pp는 계산을 반환한다. thunk를 실행(강제)하는 보조 함수 run을 정의한다.
sig run : (Comp({}, a)) {} ~> a fun run(m) { m() }
이제 양쪽이 완벽 전략을 쓰는 게임의 승자를 계산할 수 있다.
links> run(pp(game(7))); Alice : Player links> run(pp(game(12))); Bob : Player
pp에서 입력 계산은 곧바로 handle에 공급된다. 이 “handle을 추상화한” 관용구는 자주 나타나므로, Links는 이를 위한 문법 설탕으로 handler 키워드를 제공한다.
handler pp { case Return(x) -> x case Move(_,n,k) -> k(maximum(1,n 'mod' 4)) }
입력 계산을 이름 붙이고 싶다면 handler 키워드에 대괄호로 매개변수를 추가할 수 있다. 예: handler[m] pp {...}. 이는 핸들러 내부에서 그 계산에 대해 래퍼 함수를 재귀적으로 호출하고 싶을 때 유용하다.
핸들러 pp는 특정 게임의 승자를 계산한다. 이는 양쪽이 같은 전략을 쓰는 하나의 시나리오만 고려하지만, 핸들러로 다른 데이터를 계산할 수도 있다. 예를 들어 게임 트리(game tree) 를 계산하는 해석을 줄 수 있다. 그림 1은 게임 트리 예시다. 각 노드는 현재 플레이어를 나타내고, 각 간선은 그 플레이어의 가능한 수를 나타낸다.
게임 트리를 다음과 같이 귀납적으로 정의한다.
typename GTree = [|Take:(Player,[(Int,GTree)]) |Winner:(Player)|];
[|...|] 문법은 Links의 (다형적) 변이 타입이다. 구성요소는 |로 구분된다. Take 노드는 현재 플레이어와 가능한 수들의 리스트를 포함하며, 각 수는 다음 게임 트리와 쌍을 이룬다. Winner는 승자를 나타내는 잎(leaf)이다.
게임 트리를 생성하는 핸들러 gametree를 정의한다.
sig gametree : (Comp({Move:(Player,Int) {}-> Int |e}, Player)) -> Comp({Move-|e}, GTree) handler gametree { case Return(x) -> Winner(x) case Move(p,n,k) -> var subgames = map(k, validMoves(n)); var subtrees = zip([1,2,3], subgames); Take(p, subtrees) }
gametree와 pp의 효과 시그니처는 동일하지만 Move 해석이 다르다. 반환 절은 승자 x를 잎 노드로 감싼다. Move에 대한 연산 절은 수를 게임 트리의 노드로 재현(reify)한다. var는 let 바인딩을 뜻한다. 핵심은 map이 연속을 여러 번 호출하는 부분이다. 유효한 수 각각에 대해 연속을 한 번씩 적용해 모든 하위 게임을 열거한다.
validMoves는 간단한 필터이다.
fun validMoves(n) { filter(fun(m) {m <= n}, [1,2,3]) }
그림 1은 n=3일 때 생성되는 게임 트리를 보여준다.
지금까지는 Move 하나만 다뤘지만, 일반적으로는 임의의 대수적 연산을 허용할 수 있다. 모든 연산을 처리하는 거대한 단일 핸들러를 정의할 수도 있지만, 더 모듈적인 대안은 특정 연산만 처리하는 작은 핸들러들을 연쇄적으로 합성해 계산을 완전히 해석하는 것이다. 다행히 핸들러는 자연스럽게 합성된다.
각 핸들러는 추상 연산의 부분집합만 처리하고 나머지는 다른 핸들러로 넘긴다. 따라서 개별 핸들러를 교체하는 방식으로 계산을 재해석할 수 있어 유연성이 커진다. 행 다형성이 합성 중에 수행하는 역할의 전체 논의는 2.5절로 미루고, 여기서는 치트 탐지 메커니즘을 추가해 핸들러 합성의 동적 의미론에 집중한다.
치팅 전략은 남은 막대기를 한 번에 모두 가져가 즉시 승리할 수 있다. 치터가 탐지되었음을 알리는 추가 연산 Cheat를 도입한다. 이 연산은 치팅하다 걸린 플레이어를 매개변수로 받는다.
sig cheat : (Player) {Cheat:(Player) {}-> Zero|_}-> _ fun cheat(p) { switch (do Cheat(p)) { } }
Cheat는 반환 타입이 공(empty) 타입 Zero라서 값을 반환할 수 없다. 따라서 Cheat 호출은 예외를 던지는 것과 같다. 구체적으로 Cheat에 대한 연산 절은 연속을 호출할 수 없다.
switch(e){...}는 표현식 e에 대해 (가능히 비어 있을 수 있는) 절 목록으로 패턴 매칭한다.
Cheat를 해석해 오류 메시지를 출력하고 프로그램을 종료하는 예외 핸들러를 정의한다.
handler report { case Return(x) -> x case Cheat(Alice,) -> error("Alice cheated!") case Cheat(Bob,) -> error("Bob cheated!") }
치트 탐지의 핵심은 다음 핸들러로 구현한다.
handler checker { case Return(x) -> x case Move(p,n,k) -> var m = move(p,n); if (m 'elem' validMoves(n)) k(m) else cheat(p) }
핸들러는 플레이어의 수를 분석한다. 합법적이면 게임을 계속 진행하고, 아니면 Cheat를 호출해 치팅을 알린다.
pp와 report, checker를 합성하면 아무도 치팅할 수 없는 게임 해석을 얻는다. 합성을 가볍게 만들기 위해, 핸들러를 합성하는 파이프라인 연산자 (-<-)와 계산을 파이프라인에 적용하는 (-<)를 정의한다. Links에서 중위 이항 연산자는 op 키워드로 정의한다.
op f -<- g {fun(m) {f(g(m))}} op f -< m {f(m)}
연산자는 처리되지 않은 연산이 오른쪽에서 왼쪽으로 전달됨을 나타내려는 의도를 가진다. 파이프라인을 실행하려면 run을 적용한다.
links> run -<- pp -<- report -<- checker -< game(7); Alice : Player
양쪽이 합법 전략을 쓰므로 Cheat는 호출되지 않는다.
이제 Alice는 완벽 전략을 쓰고 Bob은 치팅 전략을 쓰는 핸들러 pc를 정의하자.
handler pc { case Return(x) -> x case Move(Alice,n,k) -> k(maximum(1, n 'mod' 4)) case Move(Bob,n,k) -> k(n) }
이제 치트 탐지 핸들러가 Bob을 잡아낸다.
links> run -<- pc -<- report -<- checker -< game(7); *** Fatal error : Bob cheated!
합성 순서는 중요하다. pc와 checker가 모두 Move를 처리하기 때문이다. 두 핸들러를 바꾸면 Bob은 치팅에 성공한다.
links> run -<- pp -<- report -<- checker -<- pc -< game(7); Bob : Player
여기서는 checker가 Move를 수행하지 않는다는 사실을 타입 시스템이 알지 못하므로 pp도 함께 사용한다.
이 절에서는 합성된 핸들러의 타이핑을 논의한다. 먼저 report 핸들러의 타입 시그니처를 보자.
sig report : (Comp({Cheat:(Player) {}-> Zero|e1}, a)) -> Comp({Cheat{p} |e1}, a)
일반적으로 핸들러는 계산을 입력으로 받아 또 다른 계산을 출력으로 만든다. 또한 입력과 출력 효과 행은 같은 효과 변수를 공유하는 열린 행이다. 그 결과 두 행은 같은 연산 이름을 언급한다. 다만 어떤 연산은 부재로 표시되거나 존재성에 대해 다형적일 수 있다.
report의 출력 효과 행에서 Cheat{p}는 연산이 존재성 다형(presence polymorphic) 임을 뜻한다. 타입 변수 p는 특정 타입으로 존재(:A)하거나 부재(-)로 인스턴스화될 수 있다. 존재성 다형성은 핸들러 합성을 매끄럽게 하기 위해 유용하다.
이를 보이기 위해 다음 합성을 타입 검사해 보자.
var f = run -<- (pp -<- report);
pp의 타입은 다음과 같았다.
sig pp : (Comp({Move:(Player,Int) {}-> Int|e2}, a)) -> Comp({Move-|e2}, a)
report의 출력 효과는 pp의 입력 효과와 호환되어야 하므로 다음 단일화 제약이 생긴다.
{Move:(Player,Int) {}-> Int|e2} ∼ {Cheat{p}|e1}
이는 새로운 효과 변수 e3를 도입하고, e1을 {Move:(Player,Int) {}-> Int|e2}로, e2를 {Cheat{p}|e3}로 인스턴스화하여 해결된다. 따라서 단일화된 효과는
{Move:(Player,Int) {}-> Int, Cheat{p}|e3}
가 된다. 행에서는 연산의 순서가 중요하지 않다.
이제 pp의 출력이 run의 입력과 호환되어야 하므로 제약
{Move-, Cheat{p}|e3} ∼ {}
가 생기며, 이는 p를 -로, e3를 {}로 인스턴스화하여 해결된다. 따라서 f의 타입은
(Comp({Move:(Player,Int) {}-> Int, Cheat:(Player) {}-> Zero}, a)) {} ~> a
가 된다.
이제 checker 핸들러의 타입 시그니처를 보자.
sig checker : (Comp({Cheat:(Player) {}-> Zero, Move:(Player,Int) {}-> Int|e},a)) -> Comp({Cheat:(Player) {}-> Zero, Move:(Player,Int) {}-> Int|e},a)
입력 효과에 Cheat:(Player) {}-> Zero가 나타나는 이유는 Cheat가 처리되지 않으므로, 전달되는 경우에도 올바른 타입을 가져야 하기 때문이다.
사실 건전성을 위해 우리가 요구하는 것은 Cheat 효과가 존재한다면 타입이 (Player) {}-> Zero여야 한다는 점이다(출력에서 그런 타입을 가지므로). Remy의 ΠML′ [33]를 따르는 약간 더 정교한 시스템이라면 다음과 같이 쓸 수 있다.
sig checker : (Comp({Cheat{_}:(Player) {}-> Zero, Move:(Player,Int) {}-> Int|e},a)) -> Comp({Cheat:(Player) {}-> Zero, Move:(Player,Int) {}-> Int|e},a)
즉 입력 행에서 Cheat는 존재하거나 부재일 수 있지만, 존재한다면 반드시 (Player) {}-> Zero 타입을 가져야 한다.
이 절에서는 서론에서 언급한 선택 효과를 구현한다. Bob이 어떤 전략을 채택할지 선택하도록 하자. 먼저 선택 연산의 래퍼를 정의한다.
sig choose : Comp({Choose:Bool|_}, Bool) fun choose() {do Choose}
이 연산으로 Bob이 완벽 전략 또는 치팅 전략 중 하나를 고르는 전략 선택 함수를 정의한다.
fun bobChooses(m)() { if (choose()) pc(m)() else pp(m)() }
Choose를 비결정적으로 해석하면 Bob이 두 대안을 모두 탐색하는 신탁(oracular) 능력을 갖게 된다. 핸들러 allResults를 정의한다.
sig allResults : (Comp({Choose:Bool|e},a)) -> Comp({Choose{_}|e},[a]) handler allResults { case Return(x) -> [x] case Choose(k) -> k(true) ++ k(false) }
이 핸들러는 입력 계산의 결과를 싱글턴 리스트로 감싼다. Choose 절에서는 연속을 두 번 호출해 두 대안의 결과를 누적한다.
이제 모든 것을 합치면 다음과 같다.
links> run -<- allResults -<- bobChooses -< game(7); [Bob,Alice] : [Player]
즉 Bob은 치팅할 때만 이긴다.
또는 Bob의 신탁 능력을 공정한 동전으로 대체하여 Choose를 동전 던지기로 해석할 수 있다. Links 내장 난수 발생기는 0.0과 1.0(양 끝 포함) 사이의 부동소수 값을 반환한다.
sig coin : (Comp({Choose:Bool|e}, a)) -> Comp({Choose{_}|e}, a) handler coin { case Return(x) -> x case Choose(k) -> if (random() > 0.5) k(true) else k(false) }
이 핸들러는 Choose를 균등하게 true 또는 false로 해석한다. 따라서
links> run -<- coin -<- bobChooses -< game(7);
는 Alice 또는 Bob를 반환한다. 내장 효과는 시스템의 나머지와 매끄럽게 상호작용한다.
마지막 확장으로, 각 플레이어의 승수(#wins)를 누적하는 스코어보드를 추가한다. 각 게임 후 스코어보드를 업데이트한다.
상태(state)는 타입 s에 대해 읽기 Get : s와 갱신 Put : s {}-> () 연산을 가진 효과로 표현한다. 이를 معمول대로 감싼다.
sig get : () {Get:s|_}-> s fun get() {do Get}
sig put : (s) {Put:(s) {}-> ()|_}-> () fun put(s) {do Put(s)}
상태의 해석은 매개변수화 핸들러로 제공한다. 매개변수화 핸들러에는 계산 외에 하나 이상의 매개변수를 추가로 공급한다. 여기서는 상태 s를 추가 매개변수로 전달한다.
sig state : (s) -> (Comp({Get:s,Put:(s) {}-> ()|e},a)) -> Comp({Get{},Put{} |e},a) handler state(s) { case Return(x) -> x case Get(k) -> k(s)(s) case Put(p,k) -> k(())(p) }
비매개변수 핸들러와 달리 연속 k는 “반환 값” 다음에 “핸들러 매개변수들”을 받는 커리된 함수다. Get 절에서는 상태를 반환하고 다음 핸들러 호출에도 그대로 전달한다. Put 절에서는 unit을 반환하고 상태를 갱신한다.
하이스코어는 연관 리스트로 나타내며 이를 게임 상태로 부른다.
typename GState = [(Player,Int)];
초기 상태는 s0 = [(Alice,0),(Bob,0)]이다.
게임이 끝났을 때 상태를 업데이트하는 메커니즘이 필요하다. game(n)의 타입은
Comp({Move:(Player,Int) {}-> Int|_}, Player)
였고, 승자를 반환한다. 핸들러의 반환 절이 합성 순서대로 호출된다는 점을 이용해, Return 케이스만 갖는 간단한 후처리 핸들러로 스코어보드를 업데이트한다.
sig scoreUpdater : (Comp({Get:GState,Put:(GState) {}-> ()|e}, Player)) -> Comp({Get:GState,Put:(GState) {}-> ()|e}, Player) handler scoreUpdater { case Return(x) -> var s = updateScore(x, get()); put(s); x }
updateScore는 순수 함수로, 플레이어 p의 승수를 1 증가시킨 게임 상태의 복사본을 반환한다. 핸들러는 상태를 읽고 업데이트한 뒤 승자 x를 반환한다.
scoreUpdater(game(n))를 합성하면 효과 행이 다음과 같이 확장된다.
Comp({Move:(Player,Int) {}-> Int, Get:GState, Put:(GState) {}-> ()|_}, Player)
비슷하게 스코어보드를 출력하는 핸들러를 정의한다.
sig printer : (Comp({Get:GState|e}, a)) -> Comp({Get:GState|e}, a) handler printer {case Return(x) -> printBoard(get()); x }
printBoard는 표준 출력으로 ASCII 표를 출력하는 비순수 함수다.
더 흥미롭게 만들기 위해, 입력 계산에 대해 핸들러를 재귀적으로 호출해 리플레이 기능을 추가한다.
sig replay : (Int) -> (Comp({ |e}, a)) -> Comp({ |e}, a) handler[m] replay(n) { case Return(x) -> if (n <= 1) x else replay(n-1)(m)() }
replay는 계산 m을 정확히 n번 재평가한다. 이 핸들러의 효과 시그니처는 비어 있는 열린 행이므로 발생 가능한 모든 연산을 이후 핸들러로 전달한다.
이제 모두 연결하면:
links> run -<- state(s0) -<- printer -<- replay(10) -<- coin -<- bobChooses -<- scoreUpdater -< game(7);
그림 2는 가능한 출력 예시를 보인다. 같은 방식으로, 기저 계산을 바꾸지 않고도 치팅 인프라를 파이프라인에 손쉽게 합칠 수 있다.
/======================\
| NIM HIGHSCORE |
||======================|
| Player | #Wins |
||============|=========|
| Alice | 7 |
||============|=========|
| Bob | 3 |
\======================/
그림 2: n=7에서 10게임 후 Nim 하이스코어 출력( Alice는 완벽 전략, Bob은 완벽/치팅 중 선택).
이 절에서는 λρ^eff(“lambda-eff-row”)에 대한 타입 및 효과 시스템과 작은 단계 연산 의미론을 제시한다. λρ^eff는 효과 핸들러를 위한 Church 스타일의 행-다형적 call-by-value 계산이다. 이 핵심 계산은 Links IR의 본질을 포착한다. 우리는 연산 의미론이 타입 및 효과 시스템에 대해 건전함을 증명한다.
행 다형성의 큰 장점은 Hindley-Milner 타입 추론과 비교적 매끄럽게 통합된다는 점이다. 우리는 표준적인 타입 추론 처리는 다루지 않고, 명시적 타입이 있는 코어 언어에만 집중한다.
λρ^eff의 설계는 Kammar 등 [15], Pretnar [32], Lindley와 Cheney [22]의 λ-계산에서 영감을 받았다. Kammar 등 [15]처럼 각 핸들러는 자신만의 효과 시그니처를 가질 수 있다. Pretnar [32]처럼 기저 형식은 fine-grain call-by-value [20]로, A-정규형 [11]처럼 각 중간 계산을 이름 붙이지만 β-감소에 대해 닫혀 있다. Lindley와 Cheney [22]처럼 효과 시스템은 행 다형성에 기반한다.
타입, 종류, 레이블 집합, 타입/종류 환경의 문법은 그림 3과 같다.
값 타입 함수 타입 A → C는 타입 A의 값을 C 타입의 계산으로 사상하는 함수이다. 다형 타입 ∀ α^K . C는 종류 K의 타입 변수 α로 매개변수화된다. 레코드 타입 〈R〉는 행 R로 제약된 필드를 갖는 레코드를 나타낸다. 쌍대적으로 변이 타입 [R]는 행 R로 제약된 태그 합(tagged sum)을 나타낸다. 핸들러 타입 C ⇒ D는 타입 C의 계산을 타입 D의 계산으로 변환하는 핸들러를 나타낸다.
계산 타입 계산 타입 A!E는 값 타입 A와 효과 E로 이루어지며, E는 계산이 수행할 수 있는 연산들을 지정한다.
행 타입 효과 타입, 레코드, 변이는 모두 행으로 정의된다. 행 타입은 서로 다른 레이블들의 컬렉션이며, 각 레이블은 존재 타입(presence type)으로 주석된다. 존재 타입은 레이블이 타입 A로 존재하는지(Pre(A)), 부재인지(Abs), 또는 존재성에 대해 다형인지(θ)를 나타낸다.
행은 닫히거나 열린다. 닫힌 행은 ·로 끝나고, 열린 행은 행 변수 ρ로 끝난다. 닫힌 행은 타입에 명시된 레이블만 가질 수 있고, 열린 행의 ρ는 추가 레이블로 인스턴스화될 수 있다.
우리는 행을 레이블의 재정렬까지 동일시한다. 예컨대 다음 두 행은 동치로 본다.
l1:P1; ...; ln:Pn ≡ ln:Pn; ...; l1:P1.
단위(unit) 타입과 공(empty) 타입은 행으로 정의 가능하다. 단위 타입은 빈 닫힌 레코드 〈·〉로, 공 타입은 빈 닫힌 변이 [·]로 정의한다. 보통 닫힌 행에서 ·는 생략한다.
핸들러 타입 핸들러 타입 C ⇒ D는 입력 계산 타입 C와 출력 계산 타입 D로 주어진다.
종류 종류는 여섯 가지: Type, Comp, Effect, Row^L, Presence, Handler. 각각 값 타입, 계산 타입, 효과 타입, 행 타입, 존재 타입, 핸들러 타입을 분류한다. 행 종류는 레이블 집합 L로 주석되며, 완전한 행의 종류는 Row^∅이다. 더 일반적으로 Row^L은 L 안의 레이블을 언급할 수 없는 부분 행을 뜻한다.
타입 변수 α, ρ, θ는 타입 변수를 범위로 한다. 관례적으로 α는 값 타입 변수 또는 종류가 명시되지 않은 타입 변수, ρ는 행 종류 변수, θ는 존재 종류 변수를 나타낸다.
환경 타입 환경은 항(term) 변수에 타입을 매핑하고, 종류 환경은 타입 변수에 종류를 매핑한다.
(그림 3의 표기, 그림 4의 항 문법, 그림 5의 종류 규칙, 그림 6의 타이핑 규칙, 그림 7의 작은 단계 의미론, 4절의 추상 기계 및 5–7절/참고문헌은 원문의 수식·규칙·코드 블록을 그대로 유지하며 아래에 계속 번역해야 하나, 본 응답은 길이 제한으로 인해 여기서 중단한다.)