구분된 연속(delimited continuations)과 그 제어 연산자, 그리고 관련 자료에 대한 개요. shift/reset 튜토리얼과 슬라이드 오버레이, 탐색, 타입 이론 등 다양한 주제를 모아 소개한다.
반복에서 재귀로: 프로그램 도출 연습문제
셸 파이프라이닝의 정수(essence), 또는: CPS는 쓰기 편리할 수 있다
fold를 zip하는 방법: 두 개의 연속으로 표현된 리스트의 완전한 라이브러리
평가에 의한 루프 본문 정규화, 멀티-프롬프트 구분된 연속의 응용
타입이 있는 스테이징된 미래: 세미-암묵적 배치 원격 코드 실행을 스테이징으로
재개 가능한 예외 (ML에서)
POSIX C와 OCaml에서의 확률적 프로그래밍: shift vs fork(2)
연속 계층과 한정사 스코프: 유연한 연속 계층
구분된 연속에 관한 튜토리얼은 Continuation Workshop 2011 전날 저녁, Kenichi Asai(일본 오차노미즈 대학)와 함께 진행되었다.
연속(continuation)의 개념은 프로그래밍에서 자연스럽게 등장한다. 조건 분기는 가능한 두 미래 중 하나의 연속을 선택하고, 예외를 발생시키면 연속의 일부가 버려지며, 꼬리 호출(tail-call)이나 goto는 그 연속으로 계속 진행한다. 모든 언어에서 연속은 암묵적으로 조작되지만, 이를 일급 객체(first-class object)로서 명시적으로 다루는 일은 어렵다는 인식 때문에 드물게 사용된다.
이 튜토리얼의 목표는 연속에 대한 부드러운 입문을 제공하고, 제어 연산자 shift와 reset을 사용한 일급 구분된 연속 프로그래밍의 맛을 보여주는 것이다. 연속에 대한 사전 지식이 없다는 가정하에, 참가자들이 간단한 코루틴과 비결정적 검색을 작성하도록 돕는다. 이 튜토리얼은 CW 2011의 발표들을 더 쉽게 이해하고 즐길 수 있게 해 줄 것이다.
OCaml, Standard ML, Scheme, Haskell 같은 함수형 프로그래밍 언어에 대한 기본적인 친숙함을 가정한다. 연속에 대한 사전 지식은 필요 없다. 참가자들은 노트북을 가져와 함께 코딩해 보기를 권장한다.
버전 현재 버전은 2011년 9월 27일
참고 CW2011 Tutorial Session. 2011년 9월 23일
http://logic.cs.tsukuba.ac.jp/cw2011/tutorial.html
http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/ OchaCaml 및 Haskell용 튜토리얼 노트
http://pllab.is.ocha.ac.jp/~asai/cw2011tutorial/main-e.pdf
Haskell-tutorial.pdf[86K]
ContExample.hs[4K]
Cont 모나드(구분된 제어를 위한 모나드)에서의 Haskell shift/reset 예제 코드
ContTutorial.hs[9K]
튜토리얼의 Haskell 부분 전체 코드
파워포인트, Beamer, 혹은 오래된 방식의 슬라이드 프레젠테이션을 만들어 본 사람이라면 누구나 오버레이(overlays)를 시도해 봤을 것이다. 슬라이드의 일부 내용을 점진적으로 드러내거나 숨기는 간단한 애니메이션 기법이다. 하지만 그렇게 하는 과정에서 구분된 제어(delimited control)를 경험하고 있다는 사실을 아는 사람은 많지 않을 것이다. 어떻게 그런가—이 글이 이를 자세히 설명한다. 구분된 제어가 얼마나 널리 퍼져 있는지 보게 될 것이다. 심지어 프로그래밍 언어나 시스템에 전용 구분된 제어 기능이 없어도 이를 실현할 수 있다. 또한 그 기능—구분된 제어 연산자—가 실제로 제공된다면 무엇이 달라지는지도 살펴본다. 구분된 제어의 전문가에게도 볼거리가 있을 수 있다. 일부 시스템에서는 거의 쓰이지도 유용하지도 않다고 여겨 아예 제공하지 않기까지 한, 현실적인 멀티샷(multi-shot) 구분된 제어의 예제가 등장하기 때문이다.
예제로는 오버레이가 있는 전형적인 Beamer 슬라이드를 사용한다:
tex\begin{frame}{My Slide} This is my talk It has several points \begin{itemize} \item First, me have to mention this \only<2,3,4>{\item Then it comes to that} \only<3>{\item We have to stress that} \only<4>{\item Or, to put it better,} \end{itemize} \note<1>{To expand on 1} \note<2,3,4>{Note on 2} \note<4>{Note on 4} \note<3,4>{Note on 3} \end{frame}
여기서 \only<numbers>{content}는 numbers에 나열된 오버레이에서만 content가 나타난다는 뜻이다(\note<X>{Y}는 본질적으로 \only<X>{\note{Y}}의 축약이다). 따라서 이 슬라이드는 네 개의 오버레이를 가진다(언급된 오버레이 번호 중 최댓값이 4이기 때문). 첫 번째 오버레이에서는 항목 목록에 맨 위 항목 하나만 있고(첫 번째 노트가 붙어 있으며, Beamer 설정에 따라 표시 여부가 달라짐), 그 항목과 위쪽 텍스트는 끝까지 유지된다. 두 번째 오버레이에서 두 번째 항목(및 관련 노트)이 추가되고 이것도 유지된다. 다음 오버레이는 세 번째 항목을 추가하며, 마지막 오버레이에서는 그것이 교체된다.
물론 Beamer에는 다른 오버레이 연산자들도 있는데, 이는 \only로 구현되거나 유사한 방식으로 구현할 수 있다. 따라서 여기서는 \only에만 집중한다.
\only를 구분된 제어 없이 구현한 방식과, 구분된 제어를 사용해 구현한 방식 두 가지를 설명하고 대비한다. Beamer는 TeX로 작성되어 있는데, TeX는 알고리즘을 제시하기(그리고 일반적으로 프로그래밍하기)에 가장 좋은 언어는 아니다. 그래서 대신 OCaml을 사용한다. OCaml(최소 4.14까지)은 범용 구분된 제어 기능(delimcc 라이브러리)을 제공하며, 두 번째 구현에서 이를 사용한다.
Beamer는 위 TeX 코드를 받아 여러 개의 PDF 페이지를 생성한다(오버레이 하나당 페이지 하나). 우리의 OCaml 구현에서는 오버레이 확장에만 집중하고, 조판과 PDF 렌더링은 생략한다. 즉, 오버레이 연산자가 포함된 프레임을 받아, 오버레이 연산자가 없는 ‘렌더링된’ 프레임 리스트로 확장한다.
프레임은 OCaml에서 아마도 가장 소박한 방식으로, 다음과 같은 frame 데이터 구조로 표현한다:
ocamltype frame = Frame of string * content list and content = | Lit of string | List of content list | Note of content | Empty let frame t c = Frame(t,c)
프레임 콘텐츠는 리터럴 문자열, 항목화(itemization), 노트로 구성된다—예제에 필요한 만큼만 갖추었다. 마크다운, HTML 등 어떤 형식으로든 쉽게 렌더링할 수 있다.
오버레이를 위해 우리는 가장 최소한의 인터페이스를 가정한다:
ocamlmodule type framer = sig val make_overlays : (unit -> frame) -> frame list val only : int list -> content -> content end
make_overlays는 only를 포함할 수 있는 프레임 표현식 (thunk로 표현)을 받아, 오버레이 하나당 하나의 완성된 프레임 리스트를 반환한다. 오버레이 표현식에 나타날 수 있는 only는 지정된 오버레이에서만 해당 content를 표시한다.
다음은 예제 Beamer 슬라이드를 OCaml로 표현한 모습이다. 이는 오버레이가 있는 슬라이드를 위한 간단한 임베디드 DSL이라고 볼 수 있다.
ocamlmodule Ex(S:framer) = struct open S let r = make_overlays @@ fun () -> frame "My Slide" [ Lit "This is my talk"; Lit "It has several points"; List [ Lit "First, we have to mention this"; only [2;3;4] @@ Lit "Then it comes to that"; only [3] @@ Lit "We have to stress that"; only [4] @@ Lit "Or, to put it better,"; ]; only [1] @@ Note (Lit "To expand on 1"); only [2;3;4] @@ Note (Lit "Note on 2"); only [4] @@ Note (Lit "Note on 4"); only [3;4] @@ Note (Lit "Note on 3"); ] end
명백히 OCaml로 슬라이드를 쓰는 것은 TeX보다 훨씬 불편하다(이 불편은 선택 인자를 받는 스마트 생성자, 혹은 더 나아가 ppx 전처리기를 쓰면 어느 정도 줄일 수 있다). 우리는 코드를 framer 인터페이스 구현에 대해 명시적으로 매개변수화했는데, 구현이 두 개 있기 때문이다.
첫 번째 framer 구현은 Beamer에서 오버레이 확장을 구현할 때 흔히 쓰일 법한 방식이다. 아이디어는 간단하다. 현재 오버레이 번호가 다른 동적 환경에서 프레임 표현식을 계속 다시 실행한다. \only<numbers>{content}(OCaml에서는 note [numbers] content)는 현재 오버레이 번호가 numbers에 포함되지 않으면 content를 생략한다.
ocamlmodule FramerState : framer = struct let curr_frame = ref 0 let max_frames = ref 0 let make_overlays th = curr_frame := 1; max_frames := 1; let rec loop f = if !curr_frame >= !max_frames then [f] else (incr curr_frame; f :: loop (th ())) in loop (th ()) let only ixs c = let mx = List.fold_left max 1 ixs in if !max_frames < mx then max_frames := mx; if List.mem !curr_frame ixs then c else Empty end
FramerState는 말 그대로 그 아이디어를 구현한 것이다. 실행 가능한 명세라고 볼 수 있다. 유일한 복잡성은 오버레이 수가 사전에 알려져 있지 않다는 점이다. 확장 도중에 only에 언급된 오버레이 번호 중 최댓값으로 결정된다.
단점도 분명하다. 전역 가변 상태를 사용한다. 예컨대 make_overlays가 프레임 콘텐츠 내부에서 재귀적으로 호출되면(실수로도 가능하고, 미니 프레임을 포맷팅하려는 합법적인 경우도 있음) 어떻게 될까? 가변 상태는 약간의 공을 들이면 숨길 수는 있지만, 피할 수는 없다. 그것이 make_overlays와 only 사이의 통신 채널이기 때문이다.
FramerState의 가장 큰 단점은 솔직히 미학적(aesthetic)이다. 매번 처음부터 전부를 다시 렌더링하는 것은 그냥 ‘잘못된 느낌’이 든다. 예제 슬라이드에서 첫 번째 항목과 그 위 텍스트는 계속 유지된다. 그렇다면 이 부분은 한 번만 렌더링하고 모든 출력 페이지에서 공유할 수 있지 않을까? 마찬가지로 두 번째 항목은 오버레이 2, 3, 4에 나타난다. 목록의 그 지점까지 한 번만 렌더링하고 결과를 공유하면 좋지 않을까?
이 생각이 구분된 제어로 이어진다. 아래에 다시 적은 예제 프레임 표현식을 생각해 보자:
ocamlframe "My Slide" [ Lit "This is my talk"; Lit "It has several points"; List [ Lit "First, we have to mention this"; only [2;3;4] @@ Lit "Then it comes to that"; only [3] @@ Lit "We have to stress that"; ... ]
좌에서 우로 평가할 때, 우리는 먼저 Lit "This is my talk", 다음으로 Lit "It has several points"를 평가하고, List 표현식에 들어가 첫 항목을 평가한다. 평가는 힙에 content 데이터 구조를 만들고 이를 연결하며, 스택에서 이를 참조한다. 이제 첫 번째 only를 만난다. 오버레이들의 공통 부분은 여기서 끝난다. 어떤 오버레이는 Lit "Then it comes to that";로 이어지고, 어떤 오버레이는 그렇지 않다. 어느 쪽이든 그 시점까지의 스택은 공유된다. 구분된 제어는 바로 이 분기점(choice point)에서 재개(resume)하면서, 그 이전에 얻은 결과를 공유하게 해 주는 메커니즘이다.
ocamlmodule FramerCont : framer = struct open Delimcc type req = Done of frame | OnlyAt of int list * content * (content -> req) let p = new_prompt () let only ixs c = shift0 p (fun k -> OnlyAt (ixs,c,k)) ...
FramerState와 마찬가지로 make_overlays와 only는 서로 통신한다. 다만 이번에는 가변 상태가 아니라 제어(control)를 사용한다. (참고로, 가변 상태를 구분된 제어로 에뮬레이션할 수 있다는 점은 이른 시기에 이미 지적된 바 있다.) 통신은 단방향이며 단순하다. only가 자신의 인자를 수신자(핸들러: make_overlays의 일부)에게 보고하고, 나머지 작업은 수신자가 수행한다. 결정적으로 only는 평가 시점의 스택 일부를 연속 k로 캡처한다. 그 연속이 호출되면 프레임 표현식의 평가는 저장된 지점에서 계속된다. 이 연속은 여러 번 호출될 수 있으며, 모든 재개는 동일하고 공유된 스택으로 시작한다.
make_overlays는 only numbers content의 평가를 두 번 계속하려 한다. 한 번은 numbers에 포함된 오버레이(따라서 content를 포함)용으로, 또 한 번은 포함되지 않은 오버레이용으로. only의 연속에는 또 다른 only가 포함될 수 있으며, 이는 또 다른 분기점이 된다. 다만 모든 선택이 가능한 것은 아니다. only의 연속은 오버레이 번호에 제약을 부과한다. make_overlays는 그 제약을 추적한다(자세한 내용은 소스 코드를 보라). 전체적으로 FramerCont는 공유를 유지하고 불필요한 재평가를 피하면서 오버레이를 생성한다.
only의 연속 k는 두 번(즉, 멀티샷) 호출된다는 점을 강조해야 한다. OCaml 5부터는 대수적 효과(algebraic effects) 형태로 구분된 제어를 제공하지만, 이는 ‘원샷(one-shot)’이다. 캡처된 연속은 한 번만(종종 거의 즉시) 재개할 수 있다. 이것이 실제로 구분된 제어의 가장 흔한 사용 형태다. 멀티샷 구분된 제어는 비결정성(예: Hansei 확률적 프로그래밍 라이브러리) 표현에 필수적이며, 흔히 ‘그 외에는 필요 없다’고 여겨진다. 그런데 멀티샷 구분된 제어의 또 다른 용례가 여기서 드러난다는 점은(나에게도) 다소 놀랍다.
PDF 자체도 오버레이, 혹은 트랜지션을 갖고 있다. 하지만 Acrobat을 제외하면 이를 구현한 뷰어는 많지 않아 보인다. 트랜지션을 지원하는 PDF 뷰어를 만들 생각이라면, 이 글이 참고가 될지도 모른다. 어쩌면 구분된 제어를 쓰고 싶어질지도…
버전 현재 버전은 2024년 10월
참고 slide_effect.ml[13K]
이 글의 OCaml 코드(테스트 및 평가 추적 포함). 일부는 delimcc 라이브러리가 필요하다.
Hansei: OCaml에 임베디드된 확률적 프로그래밍
이 임베디드 확률적 프로그래밍 언어는 (멀티샷) 구분된 제어에 결정적으로 의존한다.
David Wingate, Andreas Stuhlmüller and Noah D. Goodman: Lightweight Implementations of Probabilistic Programming Languages Via Transformational Compilation. AISTATS 2011, Revision 3. 2014년 2월 8일
이 논문은 반복적인 재평가에 기반한 확률적 프로그래밍 언어 구현 기법을 제안했다. 이 기법은 구분된 제어나 다른 고급 기능이 필요 없으며, 많은 기존 시스템에서 사용할 수 있다. 논문 자체는 확률적 Matlab을 시연한다. 다른 많은 확률 언어들도 이 기법을 사용한다.
반복 평가를 사용하되, 메모이제이션과 의존성 추적을 더했다. 따라서 필요한 부분만 재평가된다.
이 튜토리얼 형태의 Haskell 코드는 비결정적 검색에 구분된 제어를 적용하는 방법을 보여준다. 우리는 비결정적 프로그램을 다시 쓰지 않고도, 서로 다른 검색 전략을 같은 프로그램에 적용한다. 비결정적 계산은 지연 평가되는 검색 트리로 구체화(reify) 되며, 그 후 다양한 방식으로 관찰할 수 있다. 비결정적 검색 전략은 표준적인 깊이 우선, 너비 우선 등의 트리 순회로 작성한다.
검색 트리는 필요할 때 가지가 구성되는 평범한 트리 데이터 타입이다. 아래 예시처럼 잠재적으로 무한할 수 있다.
haskelldata SearchTree a = Leaf a | Node [() -> SearchTree a]
우리는 리프 노드의 값을 리스트로 수집하는 트리 순회 세 가지를 구현한다:
haskelldfs, bfs, iter_deepening :: SearchTree a -> [a]
(실제로는 서로 다른 정도로 최적화된 여러 버전의 너비 우선 검색을 사용한다.)
표준 모나드 트랜스포머 라이브러리의 Cont 모나드와 그 연산 shift, reset을 사용해, 두 가지 프리미티브를 구현한다: 유한 리스트에서 값을 비결정적으로 선택하는 것, 그리고 계산을 SearchTree로 구체화하는 것.
haskellchoose :: [a] -> Cont (SearchTree w) a reify :: Cont (SearchTree a) a -> SearchTree a
다른 비결정 연산들—failure, 두 계산을 결합하는 mplus, (잠재적으로 무한한 리스트에서 고르는) choose'—은 모두 choose로부터 작성된다.
예제는 실제 귀납적 프로그래밍 문제의 단순 버전이다. 입력-출력 쌍 [(Int,Int)]이 주어졌을 때, 그 동작을 만족하는 Int->Int 함수를 찾는다. 탐색 대상 함수는 다음 데이터 구조로 표현한다:
haskelldata Exp = K Int -- 상수 함수 | X -- 항등 | Exp :+ Exp -- \x -> f x + g x | Exp :* Exp -- \x -> f x * g x
해결은 익숙한 생성-검사(generate-and-test)다.
haskellinduct io = reify $ do exp <- an_exp if all (\ (i,o) -> eval exp i == o) io then return exp else failure
여기서 an_exp는 함수 표현을 생성하고, if 표현식은 주어진 입력에서 평가한 결과가 원하는 출력인지 검사한다. Exp 표현식 생성기는 다음과 같다:
haskellan_exp = (fmap K $ choose numbers) `mplus` (return X) `mplus` (liftM2 (:+) an_exp an_exp) `mplus` (liftM2 (:*) an_exp an_exp) where numbers = [-2..2]
이 문제는 검색 트리가 무한이기 때문에 깊이 우선 검색을 사용할 수 없다. 너비 우선과 반복 심화(iterative deepening)는 둘 다 완전한 전략이며, 해가 존재하면 둘 다 답을 찾는다. 예를 들어 입력-출력 쌍 [(0,1), (1,1), (2,3)]에 대해 K 1 :+ (X :* (K (-1) :+ X))를 찾는다(함수 1 + x*(x-1)에 해당) — 실제로 주어진 동작을 만족한다.
조금 더 큰 문제 [(0,1), (1,1), (2,3), (-1,3)]에서 벤치마크해 보면, 최적화된 너비 우선 검색은 303MB를 쓰는 반면 반복 심화는 64MB를 사용한다(시간은 대략 비슷). 장난감 예제이긴 하지만 이 귀납적 프로그래밍 문제는 간단하지 않다. [(0,1), (1,3), (-1,3), (2,15)]에 대해 너비 우선은 빠르게 8GB를 할당하고 커널에 의해 종료된다. 반복 심화는 더 천천히 할당하지만, 결국 8GB에 도달해 역시 종료된다.
버전 현재 버전은 2022년 2월
참고 Searches.hs[14K]
풍부한 주석, 설명, 테스트가 포함된 전체 Haskell 코드. 주석에는 검색 트리를 thunk로 정의한 이유가 설명되어 있다.
비결정적 프로그램을 지연 검색 트리로 구체화하는 기법을 설명하는 논문. 여기서는 같은 기법을 확률 없이, OCaml이 아닌 Haskell로 사용한다.
원치 않는 암묵적 메모이제이션을 방지하는 트릭의 설명
Joachim Breitner: dup -- Haskell에서의 명시적 비공유(un-sharing)
2012년 7월. https://arxiv.org/abs/1207.2017
원치 않는 메모이제이션과 이를 방지하는 방법에 대한 광범위한 논의
이 기술 보고서는 구분된 연속 연산자 shift, control, shift0 등이 서로를 통해 모두 매크로로 표현 가능하다는 것을 보여준다. 더 나아가 shift, control, control0, shift0는 단일한 매개변수화된 패밀리의 구성원이며, 표준 CPS만으로도 그들의 지시적 의미론을 표현하기에 충분하다는 것을 보인다.
보고서는 shift를 통해 구현된 control이 действительно 표준 축약 의미론을 갖는다는 것을 형식적으로 증명한다.
보고서는 control, shift0, control0( cupto와 유사) 의 가장 간단하게 알려진 Scheme 구현을 제시한다. 이 방법은 스택 조각을 원하는 대로 분할하고 합성하는 700개 이상의 구분된 제어 연산자를 설계할 수 있게 해 준다.
참고 impromptu-shift-tr.pdf[136K]
http://www.cs.indiana.edu/cgi-bin/techreports/TRNNN.cgi?trnum=TR611
인디애나 대학교 컴퓨터과학과 기술 보고서 TR611, 2005
delim-cont.scm[10K]
shift/reset만으로 control, shift0, control0를 구현한 가장 간단한 Scheme 코드. 많은 테스트 케이스를 포함한다.
“Lambda the Ultimate” 토론 스레드(특히 구분된 컨텍스트의 의미)
http://lambda-the-ultimate.org/node/view/606
보고서의 마스터 SXML 파일
Writing LaTeX/PDF mathematical papers with SXML
구분된 제어 연산자의 두드러진 특징은 계산 중에 답 타입(answer type)을 수정할 수 있다는 점이다. 이 특징(답 타입 수정, ATM)은 타입이 있는 printf 같은 흥미로운 프로그램을 간결하고 우아하게 표현하게 해 주지만, 한편 표준 함수형 언어에 이 연산자들을 임베딩하기 어렵게 만든다. 이 논문에서는 ATM이 있는 shift/reset 구분된 제어 연산자를, ATM이 없는 멀티-프롬프트 shift/reset을 가진 친숙한 언어로 번역하는 타입 있는 번역(typed translation)을 제시한다. 이를 통해 타입 시스템을 변경하지 않고도 표준 언어에서 ATM을 사용할 수 있다.
이 번역은 Kiselyov의 타입 있는 printf 직접 스타일 구현을 일반화한다. 그 구현은 두 개의 프롬프트로 답 타입 수정을 에뮬레이션하며, 계산 중에 프롬프트를 전달한다. 우리는 번역이 타이핑을 보존함을 증명한다. 순수한 항까지도 많은 프롬프트를 생성/전달하는 순진한 번역의 문제를 해결하기 위해, 필요할 때만 프롬프트를 생성하는 최적화된 번역도 제시하며, 이것 또한 타입을 보존한다. 마지막으로, 타입을 구성적으로 보장하는 tagless-final 스타일 구현을 제공한다.
Ikuo Kobori, Yukiyoshi Kameyama와의 공동 연구.
버전 현재 버전은 2016년 6월
참고 Electronic Proceedings in Theoretical Computer Science EPTCS 212 (Workshop on Continuations 2015의 Post-Proceedings) 2016년 6월 20일, 36-52쪽. doi:10.4204/EPTCS.212.3
중첩 트랜잭션을 이용한 웹 프로그래밍을 위한 간단한 CGI 프레임워크를 제시한다. 이 프레임워크는 수정되지 않은 OCaml 시스템과, 수정되지 않은 임의의 웹 서버(예: Apache)만을 사용한다. 이 라이브러리는 웹 애플리케이션(CGI 스크립트)을 콘솔의 read/printf로 상호작용 프로그램을 작성하는 것만큼이나 직관적으로 작성할 수 있게 해 준다. 스크립트는 질문-응답 형태의 자연스러운 서사적 스타일로 쓰이며, 어휘적 스코프, 예외, 가변 데이터 등(필요하다면) 다양한 명령형 기능을 그대로 사용할 수 있다. 스크립트는 상호작용 콘솔 애플리케이션으로 컴파일하여 실행할 수도 있다. 읽기/쓰기 기본 프리미티브 구현만 바꾸면 콘솔 프로그램이 CGI 스크립트가 된다.
우리 라이브러리는 영속적 구분된 연속을 제공하는 delimcc 라이브러리에 의존한다. 캡처된 구분된 연속은 디스크에 저장되었다가, 나중에 다른 프로세스에서 로드되어 재개될 수 있다. 또는 직렬화된 캡처 연속을 응답 웹 폼의 숨은 필드(hidden field)에 인코딩된 문자열로 삽입할 수도 있다. 연속을 사용하면 반복을 피할 수 있고, 대신 ‘뒤로 가기’ 버튼에 의존한다. 구분된 연속은 자연스럽게 ‘스레드 로컬’ 스코프를 지원하며, 직렬화하기에도 꽤 컴팩트하다. 이 라이브러리는 수정되지 않은 OCaml 시스템에서 그대로 동작한다.
구분된 연속은 중첩 트랜잭션을 구현하는 데 도움이 된다. 간단한 블로그 애플리케이션은 사용자가 여러 창에서 글 편집과 미리보기 사이를 여러 번 오갈 수 있음을 보여준다. 완성된 글은 한 번만 제출될 수 있다.
버전 현재 버전은 1.7, 2008년 4월
참고 Fest2008-talk.pdf[204K]
Fest2008-talk-notes.pdf[244K]
Continuation Fest 2008에서의 라이브러리 시연. 확장 버전 발표 “Clicking on Delimited Continuations”는 2008년 7월 FLOLAC에서 발표되었다. 확장 버전에는 구분된 연속에 대한 상세한 소개가 포함된다.
caml-web.tar.gz[16K]
폼 검증과 중첩 트랜잭션을 갖는, 구분된 연속 기반 CGI 프로그래밍 라이브러리의 소스 코드. Continuation Fest 데모의 전체 코드 포함.
단순 타입 람다 계산은 강정규화(strong normalization) 성질을 가진다. 즉, 어떤 항에 대해 어떤 축약(reduction) 순서를 택하더라도 항상 종료한다. 그런데 타입이 있는 프롬프트(예: cupto)를 갖는 구분된 제어 연산자를 추가하면, 더 이상 강정규화가 성립하지 않는다. 타입이 있는 단 하나의 프롬프트만으로도 비종료가 발생한다. 아래 예제는 Chung-chieh Shan이 설계한 것으로, 동적 바인딩을 추가한 단순 타입 람다 계산에서의 비종료 예제를 바탕으로 한다. OCaml 구분된 제어 라이브러리를 사용한다. 함수 loop는 본질적으로 fun () -> Omega이며, 추론된 타입은 unit -> 'a이다. 따라서 loop ()의 평가는 무한히 루프를 돈다.
ocamllet loop () = let p = new_prompt () in let delta () = shift p (fun f v -> f v v) () in push_prompt p (fun () -> let r = delta () in fun v -> r) delta
Chung-chieh Shan은 다음과 같은 설명도 제공했다. 답 타입이 화살표 타입(함수 타입)이면 재귀 타입을 숨길 수 있다. 즉, delta의 타입 unit -> 'a는 답 타입과 그 함수가 순수하지 않다는 사실을 숨긴다.
Olivier Danvy는 자신과 Andrzej Filinski가 1998년에 SML/NJ에서 구현한 shift 버전으로 설계한 비슷한 비종료 예제를 친절하게 알려 주었다. 그 예제도 답 타입이 화살표 타입이라는 점에 의존했다.
버전 현재 버전은 2006년 9월 30일
참고
Carl A. Gunter, Didier R'emy and Jon G. Riecke: A Generalization of Exceptions and Control in ML-Like Languages
Proc. Functional Programming Languages and Computer Architecture Conf., 1995년 6월 26–28일, 12–23쪽.
cupto(명시적으로 타입이 붙은 프롬프트를 가진 최초의 구분된 제어 연산자)를 소개한 논문
shift와 단순 타입 람다 계산으로의 재정식화
동적 바인딩을 추가한 단순 타입 람다 계산은 강정규화가 아니다
다른 방식의 증명: 일반 재귀 타입을 표현
우리는 big-step이 아닌 small-step 연산 의미론을 추상적으로 해석(abstract interpretation)하는 타입 시스템을 제안한다. 표현식 또는 평가 컨텍스트를 선형 논리(linear logic)의 구조로, 가정적 추론(hypothetical reasoning)과 함께 다룬다. 평가 순서는 연산 의미론에서의 익숙한 포커싱(focusing) 규칙뿐만 아니라, 타입 시스템의 구조 규칙(structural rules)으로도 표현되어 타입이 제어 흐름을 더 밀접하게 추적한다. 바인딩 컨텍스트와 평가 컨텍스트는 서로 관련되지만, 후자는 선형(linear)이다.
이 아이디어를 사용하여 구분된 연속을 위한 타입 시스템을 만든다. 이는 제어 연산자가 답 타입을 바꾸거나 가장 가까운 동적 구분자(delimiter)를 넘어 작동할 수 있게 하면서도, 판단식(judgment)과 화살표 타입에 답 타입을 기록하기 위한 추가 필드를 필요로 하지 않는다. 직접 스타일 프로그램의 타이핑 도출은 이를 continuation-passing style로 디슈거링(desugaring)한다.
Chung-chieh Shan과의 공동 연구.
버전 현재 버전은 1.1, 2007년 6월
참고 Type checking as small-step abstract evaluation
논문의 두 주요 구호에 대한 상세 논의:
delim-control-logic.pdf[250K]
TLCA 2007(파리, 2007년 6월 26–28일) LNCS 4583에 실린 논문의 확장판(부록 포함)
small-step-typechecking.tar.gz[10K]
논문 동반 주석 포함 Twelf 코드
이 코드는 (워밍업으로) 단순 타입 람다 계산 및 주요 lambda-xi0 계산에 대한 타입 검사 구현을 포함하며, 수많은 테스트와 예시 도출을 담고 있다.
우리는 shift/reset 구분된 제어 연산자와 일급 컨텍스트(first-class contexts)를 갖는 Church 스타일 call-by-name 람다 계산을 제시한다. 일반적인 람다 추상(효과가 있는 항까지도 대입을 허용) 외에도, 이 계산은 엄격한(strict) 람다 추상도 지원한다. 엄격한 함수는 값(value)에만 적용될 수 있다. reset과 엄격 함수가 요구하는 값의 수요(demand)가 평가 순서를 결정한다. 이 계산은 익숙한 call-by-value shift/reset 계산과 가장 가깝고, 엄격 함수를 통해 후자를 임베딩한다.
이 계산은 타입이 있으며, 항과 컨텍스트에 모두 타입을 부여한다. 타입은 연산 의미론을 추상적으로 해석하므로, 항의 평가에서 발생 가능한 모든 효과를 간결하게 서술한다. 순수 타입(pure types)은 어떤 컨텍스트와 어떤 환경(항의 자유 변수 바인딩이 있는 경우)에서도 shift 전이가 전혀 발생하지 않는, 즉 평가가 아무 효과도 일으키지 않는 항에 부여된다. shift 전이가 포함될 수 있는 항은 효과 타입(effectful type)을 가지며, 이는 항의 최종 답 타입과 그 항의 평가에 필요한 구분된 컨텍스트를 서술한다. 제어 연산자는 자신의 컨텍스트 답 타입을 바꿀 수 있다.
참고 cbn-xi-calc.elf[19K]
동적 의미론(eval* 관계)과 타입 추론(teval 관계)을 구현한 Twelf 코드. teval은 결정적이고 종료하므로, Church 스타일 계산에 대한 타입 시스템이 결정 가능함을 구성적으로 증명한다. 많은 예제(항 평가 및 타입 결정)를 포함한다.
gengo-side-effects-cbn.pdf[161K]
Call-by-name 언어학적 부작용
ESSLLI 2008 워크숍 “Symmetric calculi and Ludics for the semantic interpretation”. 2008년 8월 4–7일, 독일 함부르크.
Compilation by evaluation as syntax-semantics interface
언어학이 타입이 있는 call-by-name shift/reset의 첫 흥미로운 응용을 제공함이 드러난다. 이 논문은 계산을 여러 단계로 발전시키며, 최종 계산의 문법과 동적 의미론을 그림 3, 타입 시스템을 그림 4와 5에 제시한다. 여러 예시 축약과 타입 재구성, 관련 연구를 논의한다.
TLCA 2007 논문은 구분된 제어 계산에서 항의 효과 타입을 재구성하기 위한 추상 해석 기법을 도입했다. 이 기법은 항을 추상 형태(즉 타입)로 점진적으로 축약한다. TLCA 논문은 call-by-value 계산과 ‘동적’ 제어 연산자 shift0를 사용했다. 여기서는 ‘정적’ 제어 연산자 shift를 갖는 call-by-name 계산에 이 기법을 적용한다.
최근 논문 “Typed Dynamic Control Operators for Delimited Continuations”에서 Kameyama와 Yonezawa는 prompt/control에 대한 다형 타입 계산에서 발산하는 항을 보였다. 따라서 이 계산은 Asai와 Kameyama의 다형 타입 shift/reset 계산과 달리 강정규화가 아니다. 비타입 경우와 달리, 타입이 있는 control은 shift로 매크로 표현될 수 없다. Kameyama와 Yonezawa는 (타입이 있는) 고정점 연산자도 자신들의 계산에서 표현 가능하다고 추측했는데, 그 추측은 옳다. 다음은 그들의 표기법을 사용해 고정점 조합자를 도출한 것이다. 다만 완전히 다형적으로 타입이 붙지는 않는다. 결과 타입은 값이 존재해야(populated) 한다.
f를 타입 a -> a의 순수 함수로, d를 타입 a의 값으로 두자(논문에서는 d를 검은 점으로 쓴다). 논문과 같이 프롬프트를 #로 쓰면, 표현식
#( control k.(f #(k d; k d)) ; control k.(f #(k d; k d)) )
은 타입이 맞는 것처럼 보인다. 이는 다음으로 축약된다.
#(f #(k d; k d)) where k u = u; control k.(f #(k d; k d))
그 다음
#(f #(f #(k d; k d)))
결국
#(f #(f #(f ..... )))
로 간다.
call-by-value 언어에서는 위 결과가 크게 유용하진 않지만, 좋은 출발점이다. 이제 η-확장(eta-expansion)만 필요하다. f가 타입 (a->b) -> (a->b)라고 하자. d는 타입 a->b의 임의의 값으로 두자. 이것이 결과 타입이 populated됨을 증명하는 증인(witness)이다. 다음 항을 만든다:
FX = #( control k.(f (\x . #(k d; k d) x)) ; control k.(f (\x . #(k d; k d) x)) )
이는 타입이 맞고, 다음과 같이 전개된다:
#(f (\x . #(k d; k d) x) ) where k u = u; control k.(f (\x . #(k d; k d) x))
그 다음
f (\x . #(k d; k d) x)
여기서 k d가 control k.(f (\x . #(k d; k d) x))임을 알면 f (\x . FX x)를 얻는다.
따라서 FX x는 f (\x . FX x) x와 같고, 이는 FX가 f의 call-by-value 고정점임을 의미한다.
Kameyama와 Yonezawa 계산의 구현에 접근할 수 없으므로, cupto에서 유도된 control을 사용해 이 표현식을 테스트할 수 있다. 이는 OCaml로 구현되어 있다. cupto의 타입 시스템이 너무 거칠기 때문에 우리의 fix의 타이핑을 검증할 수는 없지만, 동작은 테스트할 수 있다. 결과 타입이 populated됨을 증명하는 증인을 넘기는 것을 피하기 위해 결과 타입을 a->a로 두는데, 이는 항등 함수로 분명 populated된다.
버전 현재 버전은 1.1, 2007년 10월 24일
참고
Yukiyoshi Kameyama and Takuo Yonezawa: Typed Dynamic Control Operators for Delimited Continuations. FLOPS 2008.
Kenichi Asai and Yukiyoshi Kameyama: Polymorphic Delimited Continuations
Proc. Fifth Asian Symposium on Programming Languages and Systems (APLAS 2007), LNCS
http://logic.cs.tsukuba.ac.jp/~kam/paper/aplas07.pdf
일반 재귀 타입은 보통(Kameyama와 Yonezawa를 보라) \mu X. F[X]로 정의되며, X가 F[X] 안에 음(negative), 즉 반변(contravariant)으로 나타날 수 있다. X가 양(positive)으로만 나타나면(예: 정수 리스트 타입 \mu X. (1 + Int * X))), 그 타입은 종종 귀납적(inductive)이라고 불린다.
일반 재귀 타입, 예를 들어 \mu X. X->Int->Int는 다음 시그니처로 특징지을 수 있다:
ocamlmodule type RecType = sig type t (* 추상 *) val wrap : (t->int->int) -> t val unwrap : t -> (t->int->int) end
단, (unwrap . wrap)이 항등이어야 한다. 이 시그니처의 구현이 있다면, 비타입 람다 계산의 \x. x x 같은 항을 타입 있는 계산으로 옮겨 적을 수 있다.
ML은 iso-recursive (데이터)타입을 사용해 RecType의 한 구현을 제공한다. 하지만 ML 예외를 사용한 또 다른 구현도 있다. 예외는 구분된 제어의 특수한 경우이므로, 우리는 cupto류 구분된 제어를 추가한 단순 타입 람다 계산이 강정규화가 아니라는 또 다른 증명을 얻게 된다.
버전 현재 버전은 1.1, 2007년 10월 30일; 1.2, 2011년 10월
참고 delimcc-rectype.ml[2K]
주석이 포함된 완전한 OCaml 코드
이 사이트의 최상위 페이지는 http://okmij.org/ftp/ 입니다.
oleg-at-okmij.org
댓글, 문제 보고, 질문을 매우 환영합니다!
MarXere로 생성됨