람다 계산과 Church/Böhm–Berarducci 인코딩을 통해 불리언, 자연수, 리스트 같은 데이터 타입을 순수 함수로 구현하는 방법을 `annah` 컴파일러 예제로 살펴본다.
이 글의 제목은 Lisp 격언인 “Code is Data(코드는 데이터다)”를 비튼 것이다. Lisp 세계에서는 모든 것이 데이터이며, 코드는 조작하고 변환할 수 있는 또 하나의 데이터 구조일 뿐이다.
하지만 정확히 반대 극단으로도 갈 수 있다. “Data is Code(데이터는 코드다)”! 모든 것을 코드로 만들고, 데이터 구조를 코드의 관점에서 구현할 수도 있다.
그게 대체 무슨 뜻인지 궁금할지도 모른다. 조작할 원시 데이터 구조가 하나도 없다면 어떻게 어떤 코드든 작성할 수 있을까? 흥미롭게도 Alonzo Church는 오래전에, 함수를 정의할 수만 있으면 완전한 프로그래밍 언어를 갖춘 것과 같다는 사실을 발견했다. “Church 인코딩”은 데이터 구조를 함수로 변환할 수 있다는 그의 통찰에서 이름을 딴 기법이다.
이 글은 부분적으로 Church 인코딩 튜토리얼이자, 내가 새로 출시한 annah 컴파일러(데이터 타입의 Church 인코딩을 구현)를 알리는 공지이기도 하다. 이 글의 많은 예제는 여러분이 직접 가지고 놀 수 있는 유효한 annah 코드다. 또한 아주 엄밀하게 말하면 annah는 Church 인코딩의 타입 있는 버전이라고 생각할 수 있는 Boehm-Berarducci 인코딩을 구현한다.
이 글은 람다 표현식에 대한 기본적인 친숙함을 가정한다. 그렇지 않다면, Haskell Programming from First Principles의 1장(무료로 제공됨)을 읽을 수 있는데, 람다 계산을 훌륭하게 가르쳐 준다.
이 예제들을 따라 해보고 싶다면, 다음 단계에 따라 annah를 다운로드하고 설치할 수 있다:
다음 stack.yaml 파일 생성
$ cat > stack.yaml
resolver: lts-5.13
packages: []
extra-deps:
- annah-1.0.0
- morte-1.6.0
<Ctrl-D>
stack setup 실행
stack install annah 실행
설치된 실행 파일을 $PATH에 추가
타입 없는 람다 계산(untyped lambda calculus)에서는 오직 람다 표현식만 사용할 수 있고 그 외에는 아무것도 없다. 예를 들어, 항등 함수를 인코딩하는 방법은 다음과 같다:
λx → x
이 함수는 인자를 하나 받아서 그 인자와 동일한 값을 결과로 반환한다.
그리스 문자 람다 기호를 사용해 변수를 도입할 때 이것을 “추상화(abstraction)”라고 부르며, 도입한 변수를 “바인딩 변수(bound variable)”라고 부른다. 그런 다음 람다 표현식의 “본문(body)” 어디에서든 그 바인딩 변수를 사용할 수 있다.
+-- Abstraction
|
|+-- Bound variable
||
vv
λx → x
^
|
+-- Body of lambda expression
람다로 시작하는 어떤 표현식이든 익명 함수이며, 이를 다른 표현식에 적용할 수 있다. 예를 들어, 항등 함수를 자기 자신에 적용하려면 다음과 같이 한다:
(λx → x) (λy → y)
-- β-reduction
= λy → y
익명 함수에 인자를 제공할 때 이를 “적용(application)”이라고 부른다.
여러 인자를 받는 함수는 중첩된 “추상화”로 정의할 수 있다:
λx → λy → x
위 코드는 익명 함수를 반환하는 익명 함수다. 예를 들어, 가장 바깥쪽 익명 함수에 값을 적용하면 새로운 함수를 얻게 된다:
(λx → λy → x) 1
-- β-reduce
λy → 1
… 그리고 람다 표현식을 두 값에 적용하면 첫 번째 값을 반환한다:
(λx → λy → x) 1 2
-- β-reduce
(λy → 1) 2
-- β-reduce
1
따라서 이 람다 표현식은 실제로는 인자 하나를 받아서 인자 하나짜리 새 함수를 반환하는 함수임에도, 두 인자를 받는 함수처럼 동작한다. 인자 하나짜리 함수로 여러 인자 함수를 흉내 내는 것을 “커리(currying)”라고 부른다. 우리는 인자 하나짜리 함수만 지원하는 람다 계산에서 프로그래밍할 것이기 때문에 이 트릭을 사용할 것이다.
타입 있는 람다 계산(typed lambda calculus)에서는 모든 함수 인자의 타입을 지정해야 하므로 다음처럼 작성해야 한다:
λ(x : a) → x
… 여기서 a는 x라는 바인딩 변수의 타입이다.
하지만 위 함수는 아직 유효하지 않다. 타입 a가 무엇인지 지정하지 않았기 때문이다. 이론적으로는 Int 같은 타입을 지정할 수 있다:
λ(x : Int) → x
… 하지만 이 글의 전제는 어떤 내장 데이터 타입에도 의존하지 않고 프로그래밍할 수 있다는 것이므로, 이 실험에서는 Int는 사용할 수 없다.
다행히도, 타입 있는 람다 계산의 일부 변형(특히 “System F”)에서는 a라는 타입 이름 자체를 또 다른 함수 인자로 도입할 수 있다:
λ(a : *) → λ(x : a) → x
이를 “타입 추상화(type abstraction)”라고 부른다. 여기서 *는 “타입들의 타입(type of types)”이며 항상 스코프 안에 있는 보편 상수이므로, 이런 방식으로 언제든 새 타입을 함수 인자로 도입할 수 있다.
위 함수는 “다형적 항등 함수(polymorphic identity function)”로, 어떤 타입에 대해서도 동작하는 능력을 보존하는 항등 함수의 타입 있는 버전이다.
Int 같은 내장 타입이 있다면, 다른 인자와 마찬가지로 다형 함수에 타입을 적용하여 특정 타입에 대한 항등 함수를 얻을 수 있다:
(λ(a : *) → λ(x : a) → x) Int
-- β-reduction
λ(x : Int) → x
이를 “타입 적용(type application)” 또는(더 흔히) “특수화(specialization)”라고 부른다. “다형(polymorphic)” 함수는 타입을 함수 인자로 받는 함수이며, 특정 타입 인자를 적용해 다형 함수를 “특수화”한다.
그런데 우리는 Int 같은 내장 타입을 포기했으니, 사용할 수 있는 다른 타입은 무엇이 있을까?
음, 모든 람다 표현식에는 그에 대응하는 타입이 있다. 예를 들어, 다형적 항등 함수의 타입은 다음과 같다:
∀(a : *) → ∀(x : a) → a
이 타입은 다음처럼 읽을 수 있다:
a이며 a는 타입이다x이며 x의 타입은 a다a의 값이어야 한다이 타입은 함수의 구현을 유일하게 결정한다. 아주 엄밀하게 말하면 함수의 외연적 동치(extensional equality of functions)까지 고려했을 때 정확히 하나의 구현만 존재한다. 이 함수는 가능한 모든 타입 a에 대해 동작해야 하므로 구현할 방법은 하나뿐이다. 타입 a의 값으로 이용 가능한 것은 x뿐이므로 결과로 x를 반환해야 한다.
대부분의 프로그래머에게 타입을 값이나 함수 인자로 전달하는 일은 다소 이상하게 느껴질 수 있는데, 대부분의 언어는 다음 중 하나이기 때문이다:
예: Javascript
// The polymorphic identity function in Javascript
function id(x) {
return x
}
// Example use of the function
id(true)
예: Haskell
-- The polymorphic identity function in Haskell
id x = x
-- Example use of the function
id True
예: Scala
-- The polymorphic identity function in Scala
def id[A](x : a)
-- Example use of the function
-- Note: Scala lets you omit the `[Boolean]` here thanks
-- to type inference but I'm making the type
-- application explicit just to illustrate that
-- the syntax is different from normal function
-- application
id[Boolean](true)
이 글의 목적을 위해, 어떤 마법이나 숨겨진 기계장치도 없이 명시적 타입 추상화와 타입 적용을 사용해 프로그래밍할 것이다.
예를 들어, 타입 있는 다형적 항등 함수를 자기 자신에 적용한다고 해보자. 타입 없는 버전은 다음과 같았다:
(λx → x) (λy → y)
… 그리고 타입 있는 버전은 다음과 같다:
(λ(a : *) → λ(x : a) → x)
(∀(b : *) → ∀(y : b) → b)
(λ(b : *) → λ(y : b) → y)
-- β-reduction
= (λ(x : ∀(b : *) → ∀(y : b) → b) → x)
(λ(b : *) → λ(y : b) → y)
-- β-reduction
= (λ(b : *) → λ(y : b) → y)
따라서 항등 함수를 자기 자신에 적용하는 일은 여전히 가능하지만, 훨씬 장황하다. 타입 추론이 있는 언어는 이런 지루한 작업을 자동화하면서도 타입이 주는 안전성 보장을 제공한다. 예를 들어, Haskell에서는 이렇게만 쓰면 된다:
(\x -> x) (\y -> y)
… 그러면 컴파일러가 모든 타입 추상화와 타입 적용을 알아서 추론해 준다.
연습문제: Haskell은 다음처럼 정의된 const 함수를 제공한다:
const :: a -> b -> a
const x y = x
System F(즉, 명시적 타입 추상화를 사용하는)에서 타입 있는 다형적 람다 표현식으로 const 함수를 번역하라.
람다 표현식이 “코드”이므로, 이제 “코드”로부터 “데이터”를 만들어야 한다.
가장 단순한 데이터 중 하나는 불리언 값이며, 이를 타입 있는 람다 표현식으로 인코딩할 수 있다. 예를 들어 값 True는 다음처럼 구현한다:
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
이름은 전혀 중요하지 않다는 점에 주목하라. 다음처럼 써도 똑같다:
λ(a : *) → λ(x : a) → λ(y : a) → x
… 이는 앞선 버전과 “α-동치(α-equivalent)”다(즉, 변수 이름 바꾸기까지 허용하면 동치).
위 표현식을 현재 디렉터리에 ./True라는 파일로 저장하자. 이유는 곧 알게 될 것이다.
유니코드 문자로 저장할 수도 있다:
$ cat > ./True
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
<Ctrl-D>
… 또는 ASCII로 저장할 수도 있는데, 각 람다(즉 λ)를 백슬래시(즉 \)로 바꾸고, 각 화살표(즉 →)를 ASCII 화살표(즉 ->)로 바꾸면 된다.
$ cat > ./True
\(Bool : *) -> \(True : Bool) -> \(False : Bool) -> True
<Ctrl-D>
… 취향대로 선택하면 된다. 이 튜토리얼의 나머지에서는 읽기 쉬우므로 유니코드를 사용하겠다.
마찬가지로, False는 두 번째 인자인 True가 아니라 세 번째 인자인 False를 반환하도록 바꾸기만 하면 인코딩할 수 있다. 이 파일 이름은 ./False로 하겠다:
$ cat > ./False
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
<Ctrl-D>
불리언 값의 타입은 무엇일까? ./True와 ./False 파일은 둘 다 같은 타입을 가지며, 이를 ./Bool이라고 부르자:
$ cat > ./Bool
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
… ASCII를 따라 하는 경우에는 각 forall 기호(즉 ∀)를 forall이라는 단어로 바꾸면 된다:
$ cat > ./Bool
forall (Bool : *) -> forall (True : Bool) -> forall (False : Bool) -> Bool
이 항(term)들과 타입을 파일에 저장하는 이유는, annah 컴파일러를 사용해 파일로 저장된 어떤 람다 표현식이나 타입도 다룰 수 있기 때문이다. 예를 들어 annah 컴파일러로 ./True 파일이 ./Bool 타입을 갖는지 검증할 수 있다:
$ annah
-- Read this as: "./True has type ./Bool"
./True : ./Bool
<Ctrl-D>
./True
$ echo $?
0
표현식이 타입 체크를 통과하면 annah는(이 경우에는 불필요한 타입 주석을 제거하여) 람다 계산으로 표현식을 컴파일한 뒤 종료 코드를 0으로 반환한다. 하지만 표현식이 타입 체크를 통과하지 못하면:
$ annah
./True : ./True
annah:
Expression: ∀(x : λ(Bool : *) → λ(True : Bool) → λ(False : Bool)
→ True) → λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
Error: Invalid input type
Type: λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
$ echo $?
1
… annah는 예외를 던지고 0이 아닌 종료 코드를 반환한다. 이 경우 annah는 타입 주석 오른쪽의 ./True가 유효한 타입이 아니라고 불평한다.
마지막으로 필요한 것은 ./Bool 타입의 값을 소비하는 함수인데, ./if 함수 같은 것이다:
$ cat > ./if
λ(x : ./Bool ) → x
-- ^
-- |
-- +-- Note the space. Filenames must end with a space
./if의 정의는 눈부시게 단순하다. ./if는 ./Bool에 대한 항등 함수일 뿐이다!
왜 이것이 동작하는지 보려면, ./if의 타입을 확인해 보자. 표준 입력으로 morte 컴파일러에 표현식을 전달하면 어떤 표현식이든 타입을 물을 수 있다:
$ morte < ./if
∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) →
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) → x
morte는 annah와 함께 설치되는 람다 계산 컴파일러이며, annah는 morte 언어에 대한 더 고수준 인터페이스다. 기본적으로 morte 컴파일러는:
이번에는 타입만 필요했으므로, morte 컴파일러에 표현식을 해석하고 타입을 추론/검증하도록 요청해도 된다:
$ morte resolve < ./Bool/if | morte typecheck
∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) →
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
위 타입은 다음과 같은 것과 같다:
∀(x : ./Bool ) → ./Bool
믿기 어렵다면, morte에 타입을 해석하도록 시켜 직접 확인할 수 있다:
$ echo "∀(x : ./Bool ) → ./Bool" | morte resolve
∀(x : ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool) →
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
하지만 이 타입은 두 번째 ./Bool만 펼치고 첫 번째 ./Bool은 그대로 두면 가장 이해하기 쉽다:
./Bool → ∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
이 타입은 ./if 함수가 네 개의 인자를 받는다는 뜻으로 읽을 수 있다:
./Bool(즉 ./True 또는 ./False)./if 표현식의 결과 타입./Bool이 ./True로 평가될 때 반환할 결과(즉 “then” 분기)./Bool이 ./False로 평가될 때 반환할 결과(즉 “else” 분기)예를 들어 다음 Haskell 코드:
if True
then False
else True
… 는 다음 Annah 코드로 번역된다:
$ annah
./if ./True
./Bool -- The type of the result
./False -- The `then` branch
./True -- The `else` branch
<Ctrl-D>
./if ./True ./Bool ./False ./True
annah는 표현식을 평가하지 않는다. annah는 표현식을 Morte 코드로 번역(그리고 그 표현식은 이미 유효한 Morte 코드다)하고 타입 체크만 한다. 표현식을 평가하려면 morte 컴파일러에도 통과시켜야 한다:
$ morte
./if ./True
./Bool -- The type of the result
./False -- The `then` branch
./True -- The `else` branch
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
morte는 이 표현식의 타입이 ./Bool임을 도출하고, 표현식이 ./False로 평가됨을 보여 준다.
morte는 모든 참조를 해석하고 β-축약을 반복 적용하여 표현식을 평가한다. 내부적으로는 다음과 같은 일이 벌어진다:
./if
./True
./Bool
./False
./True
-- Resolve the `./if` reference
= (λ(x : ./Bool ) → x)
./True
./Bool
./False
./True
-- β-reduce
= ./True
./Bool
./False
./True
-- Resolve the `./True` reference
= (λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True)
./Bool
./False
./True
-- β-reduce
= (λ(True : ./Bool ) → λ(False : ./Bool ) → True)
./False
./True
-- β-reduce
= (λ(False : ./Bool ) → ./False )
./True
-- β-reduce
= ./False
-- Resolve the `./False` reference
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
위 단계들은 약간의 하얀 거짓말이다. 실제 단계의 순서는 다르지만, 동치인 결과를 낳는다.
./if 함수는 사실 필요조차 없었다. ./Bool 타입의 모든 값은 이미 “미리 만들어진 if 표현식”이기 때문이다. 그래서 ./if는 ./Bool에 대한 항등 함수다. 위 예제에서 ./if를 지워도 코드는 여전히 동작한다.
이제 not 함수를 정의해서 파일에 저장해 보자:
$ annah > ./not
λ(b : ./Bool ) →
./if b
./Bool
./False -- If `b` is `./True` then return `./False`
./True -- If `b` is `./False` then return `./True`
<Ctrl-D>
이제 이 파일을 일반 함수처럼 사용할 수 있다:
$ morte
./not ./False
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
$ morte
./not ./True
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
./not ./False는 ./True를 반환하고 ./not ./True는 ./False를 반환하는 것을 볼 수 있다.
비슷하게 and 함수와 or 함수도 정의할 수 있다:
$ annah > and
λ(x : ./Bool ) → λ(y : ./Bool ) →
./if x
./Bool
y -- If `x` is `./True` then return `y`
./False -- If `x` is `./False` then return `./False`
<Ctrl-D>
$ annah > or
λ(x : ./Bool ) → λ(y : ./Bool ) →
./if x
./Bool
./True -- If `x` is `./True` then return `./True`
y -- If `x` is `./False` then return `y`
<Ctrl-D>
… 그리고 사용해 보자:
$ morte
./and ./True ./False
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
$ morte
./or ./True ./False
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
우리는 람다 표현식밖에 없는 상태에서 시작했지만, 그럼에도 불구하고 다음을 구현해냈다:
./Bool 타입./Bool 타입의 값 ./True./Bool 타입의 값 ./False./if, ./not, ./and, ./or 함수… 그리고 이들로 실제 계산을 할 수 있다! 즉, 불리언 데이터 타입을 전부 코드로만 모델링한 것이다.
연습문제: xor 함수를 구현하라.
람다 계산으로 어떤 다른 데이터 타입을 구현할 수 있는지 궁금할 수도 있다. 다행히도, annah 컴파일러는 데이터 타입 정의를 람다 표현식으로 실제로 컴파일해 주기 때문에 궁금해할 필요가 없다.
예를 들어, Peano 수로 인코딩한 자연수 타입을 정의하고 싶다고 하자. 다음처럼 쓸 수 있다:
$ annah types
type Nat
data Succ (pred : Nat)
data Zero
fold foldNat
<Ctrl-D>
위 데이터 타입 명세는 다음을 의미한다:
Nat라는 타입을 정의한다 …pred라는 필드 하나를 갖는 Succ라는 생성자를 두고, 그 필드의 타입은 Nat다 …Zero라는 생성자도 하나 둔다foldNat라는 fold를 둔다annah는 이 데이터 타입 명세를 다음 파일과 디렉터리로 번역한다:
+-- ./Nat.annah -- `annah` implementation of `Nat`
|
`-- ./Nat
|
+-- @ -- `morte` implementation of `Nat`
| --
| -- If you import the `./Nat` directory this file is
| -- imported instead
|
+-- Zero.annah -- `annah` implementation of `Zero`
|
+-- Zero -- `morte` implementation of `Zero`
|
+-- Succ.annah -- `annah` implementation of `Succ`
|
+-- Succ -- `morte` implementation of `Succ`
|
+-- foldNat.annah -- `annah` implementation of `foldNat`
|
`-- foldNat -- `morte` implementation of `foldNat`
Nat 타입이 어떻게 구현되는지 보자:
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
모든 Boehm-Berarducci 인코딩 데이터 타입은 ./Nat을 포함하여 치환(substitution) 함수로 인코딩된다. ./Nat의 어떤 값이든 세 개의 인자를 받아 자연수 표현식에 치환한다:
Nat 타입의 모든 등장 위치를 대체한다Succ 생성자의 모든 등장 위치를 대체한다Zero 생성자의 모든 등장 위치를 대체한다구체적인 예제를 따라가 보면 더 이해가 될 것이다. 먼저 ./Nat/Succ와 ./Nat/Zero 생성자를 사용해 숫자 3을 만들자:
$ morte
./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ Zero))
이제 자연수가 even인지 여부를 계산하고 싶다고 하자. 단, even을 계산할 때 치환만 사용해야 한다는 제약이 있다. 자연수가 even이면 ./True, 그렇지 않으면 ./False가 되도록, Succ 생성자 자리에는 무엇을 치환하고 Zero 생성자 자리에는 무엇을 치환할지 찾아야 한다.
동작하는 치환 한 가지는 다음과 같다:
Zero를 ./True로 바꾼다(Zero는 even이므로)Succ를 ./not으로 바꾼다(Succ는 even과 odd 사이를 번갈아 가므로)즉, 다음에서 시작해서:
./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
… ./Nat/Succ를 ./not으로 치환하고 ./Nat/Zero를 ./True로 치환하면:
./not (./not (./not ./True ))
… 이 표현식은 ./False로 축약된다.
이를 증명하기 위해 위 숫자를 ./three라는 파일로 저장하자:
$ morte > ./three
./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
$ cat three
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ Zero))
먼저 Nat을 ./Bool로 바꿔야 한다:
./three ./Bool
-- Resolve `./three`
= (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ Zero))
) ./Bool
-- β-reduce
= λ(Succ : ∀(pred : ./Bool ) → ./Bool ) → λ(Zero : ./Bool ) →
Succ (Succ (Succ Zero))
이제 다음 두 인자는 ./not과 ./True를 치환하기에 정확히 알맞은 타입이 되었다. ./Succ라는 인자는 이제 ∀(pred : ./Bool ) → ./Bool 타입의 함수인데, 이는 ./not의 타입과 같다. Zero라는 인자는 이제 ./Bool 타입의 값인데, 이는 ./True의 타입과 같다. 따라서 다음 두 인자를 적용할 수 있다:
./three ./Bool ./not ./True
-- Resolve `./three`
= (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ Zero))
) ./Bool ./not ./True
-- β-reduce
= (λ(Succ : ∀(pred : ./Bool ) → ./Bool ) → λ(Zero : ./Bool ) →
Succ (Succ (Succ Zero))
) ./not ./True
-- β-reduce
= (λ(Zero : ./Bool ) → ./not (./not (./not Zero))) ./True
-- β-reduce
= ./not (./not (./not ./True )))
결과는 원래 표현식:
./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero ))
… 에서 ./Nat/Succ를 ./not으로 바꾸고 ./Nat/Zero를 ./True로 바꿨을 때 얻는 것과 정확히 같다.
morte 컴파일러로 실행해 이것이 동작하는지 확인해 보자:
$ morte
./three ./Bool ./not ./True
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
morte는 ./three가 짝수가 아님을 계산해 ./False를 반환한다.
더 나아가 ./even 함수를 파일로 저장할 수도 있다:
$ annah > even
\(n : ./Nat ) →
n ./Bool
./not -- Replace each `./Nat/Succ` with `./not`
./True -- Replace each `./Nat/Zero` with `./True`
… 그리고 새로 만든 ./even 함수를 사용할 수 있다:
$ morte
./even ./three
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
$ morte
./even ./Nat/Zero
<Ctrl-D>
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
annah 컴파일러는 자연수 리터럴도 직접 지원하므로, 다음처럼 써도 된다:
$ annah | morte
./even 100
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
덧셈은 어떨까? 치환만 사용해 두 수를 어떻게 더할까?
두 수 m과 n을 더하는 한 가지 방법은, m에서 각 ./Nat/Succ를 ./Nat/Succ로(즉 그대로) 치환하고 Zero를 n으로 치환하는 것이다. 즉:
$ annah > plus
λ(m : ./Nat ) → λ(n : ./Nat ) →
m ./Nat -- The result will still be a `./Nat`
./Nat/Succ -- Replace each `./Nat/Succ` with `./Nat/Succ`
n -- Replace each `./Nat/Zero` with `n`
이를 확인해 보자:
$ annah | morte
./plus 2 2
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ Zero)))
Church 인코딩된 4를 얻었다!
내부적으로 일어난 치환은 다음과 같다:
./plus 2 2
-- Resolve `./plus`
= (λ(m : ./Nat ) → λ(n : ./Nat ) → m ./Nat ./Nat/Succ n) 2 2
-- β-reduce
= (λ(n : ./Nat ) → 2 ./Nat ./Nat/Succ n) 2
-- β-reduce
= 2 ./Nat ./Nat/Succ 2
-- Definition of 2
= (./Nat/Succ (./Nat/Succ ./Nat/Zero )) ./Nat ./Nat/Succ 2
-- Resolve and β-reduce the definition of 2 (multiple steps)
= (λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ Zero)
) ./Nat ./Nat/Succ 2
-- β-reduce
= (λ(Succ : ∀(pred : ./Nat ) → ./Nat ) → λ(Zero : ./Nat ) →
Succ (Succ Zero)
) ./Nat/Succ 2
-- β-reduce
= (λ(Zero : ./Nat ) → ./Nat/Succ (./Nat/Succ Zero)) 2
-- β-reduce
= ./Nat/Succ (./Nat/Succ 2)
-- Definition of 2
= ./Nat/Succ (./Nat/Succ (./Nat/Succ (./Nat/Succ ./Nat/Zero )))
-- Resolve and β-reduce (multiple steps)
= λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ Zero)))
따라서 람다 계산으로 자연수를 인코딩할 수는 있지만, 매우 비효율적이다! 시간 복잡도와 상수 계수를 크게 줄이는 트릭이 있긴 하지만, 기계 산술과 경쟁할 수는 없다. 이는 산술을 순수하게 코드만으로 모델링할 수 있다는 개념 증명에 가깝다.
연습문제: 두 자연수를 곱하는 함수를 구현하라.
annah는 주어진 표현식에 스코프를 가지는 “임시” 데이터 타입도 정의할 수 있게 해 준다. 사실 Nat이 구현된 방식이 바로 이것이다. 각 타입과 항이 morte 코드로 변환되기 전에 annah에서 어떻게 정의되는지 보려면 해당 *.annah 파일을 보면 된다.
예를 들어, Nat 타입은 annah에서 다음처럼 정의된다:
$ cat Nat.annah
type Nat
data Succ (pred : Nat)
data Zero
fold foldNat
in Nat
첫 네 줄은 우리가 커맨드라인에서 annah types 명령을 호출할 때 썼던 것과 동일하다. 같은 데이터 타입 명세를 사용해, 지정한 타입과 데이터 생성자를 참조할 수 있는 스코프 표현식을 만들 수 있다.
이 표현식을 annah에 통과시키면 Nat 타입이 반환된다:
$ annah < Nat.annah
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
이런 스코프 데이터 타입 선언을 사용하면 현재 작업 디렉터리를 어지럽히지 않고도 다양한 데이터 타입이 어떻게 인코딩되는지 빠르게 확인할 수 있다. 예를 들어 Maybe 타입이 람다 계산에서 어떻게 인코딩되는지 annah에 물어볼 수 있다:
$ annah
λ(a : *) →
type Maybe
data Just (x : a)
data Nothing
-- You can also leave out this `fold` if you don't use it
fold foldMaybe
in Maybe
<Ctrl-D>
λ(a : *) → ∀(Maybe : *) → ∀(Just : ∀(x : a) → Maybe) →
∀(Nothing : Maybe) → Maybe
Maybe 값도 또 하나의 치환 함수일 뿐이다. Just에 치환할 분기 하나와 Nothing에 치환할 분기 하나를 제공한다. 예를 들어 Just 생성자는 항상 첫 번째 분기를 치환하고, 여러분이 제공한 Nothing 분기는 무시한다:
$ annah
λ(a : *) →
type Maybe
data Just (x : a)
data Nothing
in Just
<Ctrl-D>
λ(a : *) → λ(x : a) → λ(Maybe : *) → λ(Just : ∀(x : a) → Maybe)
→ λ(Nothing : Maybe) → Just x
반대로 Nothing 생성자는 제공한 Nothing 분기를 치환하고, Just 분기는 무시한다:
$ annah
λ(a : *) →
type Maybe
data Just (x : a)
data Nothing
in Nothing
<Ctrl-D>
λ(a : *) → λ(Maybe : *) → λ(Just : ∀(x : a) → Maybe) → λ(Nothing : Maybe) → Nothing
Maybe와 Just를 순수하게 함수만으로 구현했음을 알 수 있다. 이는 함수가 있는 어떤 언어라도 Maybe를 인코딩할 수 있음을 뜻한다. 예를 들어 Python도 가능하다!
위 Just와 Nothing의 정의를 동등한 Python 코드로 번역해 보자. 차이점은 Python에서는 타입 추상화가 필요 없으므로 지운다는 것뿐이다:
def just(x):
def f(just, nothing):
return just(x)
return f
def nothing():
def f(just, nothing):
return nothing
return f
Haskell 스타일의 패턴 매칭도 비슷하게 번역할 수 있다:
example :: Maybe Int -> IO ()
example m = case m of
Just n -> print n
Nothing -> return ()
… 이는 다음 Python 코드로 번역된다:
def example(m):
def just(n): # This is what we substitute in place of `Just`
print(n)
def nothing(): # This is what we substitute in place of `Nothing`
return
m(just, nothing)
… 그리고 이 패턴 매칭 함수가 동작하는지 확인할 수 있다:
>>> example(nothing())
>>> example(just(1))
1
멋지다! 이는 대수적 데이터 타입이라면 무엇이든 함수가 있는 어떤 언어에도 임베드할 수 있음을 뜻한다. 사실상 거의 모든 언어가 그렇다!
경고: 이런 일을 하면 동료들이 화를 낼 수도 있다! 대수적 데이터 타입에 대한 내장 지원이 있는 언어를 쓰는 편이, 언어를 억지로 비틀어 다른 무언가로 만들려고 하는 것보다 낫다.
let 표현식도 람다 계산으로 번역할 수 있다. 예를 들어 어떤 것을 파일에 저장하는 대신, let 표현식을 사용해 프로그램 안에서 일시적으로 정의할 수 있다.
예를 들어 다음을 쓸 수 있다:
$ annah | morte
let x : ./Nat = ./plus 1 2
in ./plus x x
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ (Succ (Succ Zero)))))
… 하지만 이 결과만 보면 annah가 let을 어떻게 디슈가(desugar)하는지 알 수 없다. 최종 평가 결과만 보기 때문이다. annah desugar 명령으로 다른 변환 없이 디슈가만 하도록 요청할 수 있다:
$ annah desugar
let x : ./Nat = ./plus 1 2
in ./plus x x
<Ctrl-D>
(λ(x : ./Nat ) → ./plus x x) (./plus (λ(Nat : *) → λ(Succ :
∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ Zero) (λ(Nat : *) →
λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ
Zero)))
… 숫자 리터럴을 사용해 정리하면 다음 표현식이 된다:
(λ(x : ./Nat ) → ./plus x x) (./plus 1 2)
다음 형태의 표현식을 쓸 때마다:
let x : t = y
in e
… 이를 람다 계산으로는 다음처럼 디코딩한다:
(λ(x : t) → e) y
함수 정의도 디코딩할 수 있다. 예를 들어 다음처럼 쓸 수 있다:
$ annah | morte
let increment (x : ./Nat ) : ./Nat = ./plus x 1
in increment 3
<Ctrl-D>
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ Zero)))
… 그리고 중간 디슈가된 형태는 함수 정의도 람다 표현식으로 인코딩한다:
$ annah desugar
let increment (x : ./Nat ) : ./Nat = ./plus x 1
in increment 3
<Ctrl-D>
(λ(increment : ∀(x : ./Nat ) → ./Nat ) → increment (λ(Nat : *)
→ λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ (Succ
(Succ Zero)))) (λ(x : ./Nat ) → ./plus x (λ(Nat : *) → λ(Succ
: ∀(pred : Nat) → Nat) → λ(Zero : Nat) → Succ Zero)
… 이를 정리하면 다음 표현식으로 볼 수 있다:
(λ(increment : ∀(x : ./Nat ) → ./Nat ) → increment 3)
(λ(x : ./Nat ) → ./plus x 1)
let 표현식과 데이터 타입 표현식을 결합할 수도 있다. 예를 들어, 파일에 아무것도 저장하지 않고 원래의 not 프로그램을 작성하면 다음과 같다:
$ annah
type Bool
data True
data False
fold if
in
let not (b : Bool) : Bool = if b Bool False True
in
not False
<Ctrl-D>
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → True
annah는 리스트에 대한 문법적 지원도 제공한다. 예를 들어:
$ annah
[nil ./Bool , ./True , ./False , ./True ]
<Ctrl-D>
λ(List : *) → λ(Cons : ∀(head : ./Bool ) → ∀(tail : List) →
List) → λ(Nil : List) → Cons ./True (Cons ./False (Cons
./True Nil))
다른 모든 데이터 타입과 마찬가지로, 리스트는 Cons와 Nil 생성자 각각에 무엇을 치환하느냐로 정의된다. 예를 들어 각 Cons를 ./and로, Nil을 ./True로 바꾸면 다음처럼 된다:
$ annah | morte
<Ctrl-D>
[nil ./Bool , ./True , ./False , ./True ] ./Bool ./and ./True
∀(Bool : *) → ∀(True : Bool) → ∀(False : Bool) → Bool
λ(Bool : *) → λ(True : Bool) → λ(False : Bool) → False
이는 개념적으로 다음 축약 순서를 따른다:
( λ(List : *)
→ λ(Cons : ∀(head : ./Bool ) → ∀(tail : List) → List)
→ λ(Nil : List)
→ Cons ./True (Cons ./False (Cons ./True Nil))
) ./Bool
./and
./True
-- β-reduction
= ( λ(Cons : ∀(head : ./Bool ) → ∀(tail : ./Bool ) → ./Bool )
→ λ(Nil : ./Bool )
→ Cons ./True (Cons ./False (Cons ./True Nil))
) ./and
./True
-- β-reduction
= ( λ(Nil : ./Bool )
→ ./and ./True (./and ./False (./and ./True Nil))
) ./True
-- β-reduction
= ./and ./True (./and ./False (./and ./True ./True))
비슷하게 각 Cons를 ./plus로, Nil을 0으로 치환하면 리스트를 합칠 수 있다:
$ annah | morte
[nil ./Nat , 1, 2, 3, 4] ./Nat ./plus 0
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
Zero)))))))))
이는 다음을 쓴 것처럼 동작한다:
./plus 1 (./plus 2 (./plus 3 (./plus 4 0)))
annah는 순수 람다 계산에서 더 정교한 예제를 보여 주기 위한 Prelude도 함께 제공한다. Prelude 1.0은 여기서 찾을 수 있다:
http://sigil.place/prelude/annah/1.0/
URL을 참조하기만 하면 이 표현식들을 코드에서 바로 사용할 수 있다. 예를 들어 원격 Bool 표현식은 여기 있다:
http://sigil.place/prelude/annah/1.0/Bool/@
… 그리고 원격 True 표현식은 여기 있다:
http://sigil.place/prelude/annah/1.0/Bool/True
… 따라서 원격 True의 타입이 원격 Bool과 일치하는지 확인하려면 이렇게 쓰면 된다:
$ annah
http://sigil.place/prelude/annah/1.0/Bool/True : http://sigil.place/prelude/annah/1.0/Bool
<Ctrl-D>
http://sigil.place/prelude/annah/1.0/Bool/True
$ echo $?
0
마찬가지로 원격 Succ와 Zero를 사용해(아주 장황하게) 자연수를 만들 수도 있다:
$ annah | morte
http://sigil.place/prelude/annah/1.0/Nat/Succ
( http://sigil.place/prelude/annah/1.0/Nat/Succ
( http://sigil.place/prelude/annah/1.0/Nat/Succ
http://sigil.place/prelude/annah/1.0/Nat/Zero
)
)
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ Zero))
하지만 원격 경로 대신 로컬 파일 경로로 더 간단히 참조하고 싶다면 wget으로 Prelude를 로컬에 클론할 수도 있다:
$ wget -np -r --cut-dirs=3 http://sigil.place/prelude/annah/1.0/
$ cd sigil.place
$ ls
(->) Defer.annah List.annah Path Sum0.annah
(->).annah Eq Maybe Path.annah Sum1
Bool Eq.annah Maybe.annah Prod0 Sum1.annah
Bool.annah Functor Monad Prod0.annah Sum2
Category Functor.annah Monad.annah Prod1 Sum2.annah
Category.annah index.html Monoid Prod1.annah
Cmd IO Monoid.annah Prod2
Cmd.annah IO.annah Nat Prod2.annah
Defer List Nat.annah Sum0
이제 더 간결한 로컬 경로로 이 표현식들을 사용할 수 있다:
./Nat/sum (./List/(++) ./Nat [nil ./Nat , 1, 2] [nil ./Nat , 3, 4])
<Ctrl-D>
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
Zero)))))))))
또한 모든 표현식에는 let 표현식으로 그 표현식의 타입을 문서화한 대응 *.annah 파일이 있다. 예를 들어 ./List/(++) 함수의 타입은 ./List/(++).annah 파일을 보면 알 수 있다:
cat './List/(++).annah'
let (++) (a : *) (as1 : ../List a) (as2 : ../List a) : ../List a =
\(List : *)
-> \(Cons : a -> List -> List)
-> \(Nil : List)
-> as1 List Cons (as2 List Cons Nil)
in (++)
첫 줄은 (++)가 세 개의 인자를 받는 함수임을 알려 준다:
a라는 인자as1이라는 인자as2라는 인자… 그리고 함수는 두 입력 리스트와 같은 타입의 리스트를 반환한다.
람다 계산을 얼마나 멀리까지 가져갈 수 있을까? 다음은 annah로 작성된 프로그램인데, 자연수 두 개를 읽고 더한 다음 출력한다:
$ annah | morte
./IO/Monad ./Prod0 (do ./IO {
x : ./Nat <- ./IO/get ;
y : ./Nat <- ./IO/get ;
_ : ./Prod0 <- ./IO/put (./Nat/(+) x y);
})
∀(IO : *) → ∀(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) →
Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → ∀(Put_ : (∀(Nat : *)
→ ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO →
IO) → ∀(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO)
→ IO
λ(IO : *) → λ(Get_ : ((∀(Nat : *) → ∀(Succ : ∀(pred : Nat) →
Nat) → ∀(Zero : Nat) → Nat) → IO) → IO) → λ(Put_ : (∀(Nat : *)
→ ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → IO →
IO) → λ(Pure_ : (∀(Prod0 : *) → ∀(Make : Prod0) → Prod0) → IO)
→ Get_ (λ(r : ∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) →
∀(Zero : Nat) → Nat) → Get_ (λ(r : ∀(Nat : *) → ∀(Succ :
∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat) → Put_ (λ(Nat : *)
→ λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) → r@1 Nat Succ
(r Nat Succ Zero)) (Pure_ (λ(Prod0 : *) → λ(Make : Prod0) →
Make))))
이는 프로그램을 실행하는 것이 아니라, 모든 프로그램 명령과 정보 흐름을 나타내는 구문 트리를 생성한다.
annah는 do 표기도 지원하므로, annah에서 리스트 컴프리헨션 같은 것도 작성할 수 있다:
$ annah | morte
./List/sum (./List/Monad ./Nat (do ./List {
x : ./Nat <- [nil ./Nat , 1, 2, 3];
y : ./Nat <- [nil ./Nat , 4, 5, 6];
_ : ./Nat <- ./List/pure ./Nat (./Nat/(+) x y);
}))
<Ctrl-D>
∀(Nat : *) → ∀(Succ : ∀(pred : Nat) → Nat) → ∀(Zero : Nat) → Nat
λ(Nat : *) → λ(Succ : ∀(pred : Nat) → Nat) → λ(Zero : Nat) →
Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ (Succ
(Succ (Succ (Succ Zero)))))))))))))))))))))))))))))))))))))))))
))))))))))))))))))
위 Annah 프로그램은 다음 Haskell 프로그램과 동등하다:
sum (do
x <- [1, 2, 3]
y <- [4, 5, 6]
return (x + y) )
… 그런데도 어떤 데이터 타입에 대한 내장 지원도 없는, 최소적이고 전체적인(total) 람다 계산만으로 100% 구현되어 있다.
이 튜토리얼은 do 표기가 어떻게 동작하는지 다루지 않지만, 이는 Hackage 패키지에 포함된 Annah 튜토리얼을 읽으면 배울 수 있다:
많은 사람들은 전체 람다 계산에서 무엇을 얼마나 할 수 있는지 과소평가한다. 나는 순수 람다 계산을 일반적인 프로그래밍 언어로 추천하지는 않지만, 고효율 원시 연산을 더한 람다 계산이라면 이식과 배포가 쉬운 단순한 함수형 언어의 현실적인 출발점이 될 수 있다고 본다.
내가 장기적으로 추구하는 프로젝트 중 하나는 “코드를 위한 JSON”이며, annah는 그 목표로 가는 길의 한 단계다. annah가 그 언어가 될 가능성은 크지 않지만, 다른 사람들이 자신의 언어 설계를 실험할 때 annah를 포크해서 실험할 수 있도록, 나는 그 과정에서 annah를 별도의 재사용 가능한 프로젝트로 분리해 두었다.
또한 내가 알기로 annah는 다음 논문에서 개략적으로 설명한 Boehm-Berarducci 인코딩을 실제로 구현한 야생의 유일한 프로젝트다:
… 따라서 실제 코드를 통해 인코딩 알고리즘을 배우는 편을 선호한다면, annah 소스 코드를 현실 세계 구현의 참고 자료로 사용할 수 있다.
Annah 프로젝트는 Hackage나 Github에서 찾을 수 있다:
… 그리고 Annah prelude의 온라인 호스팅은 여기 있다:
Annah 튜토리얼은 Annah 언어와 컴파일러를 이 튜토리얼보다 훨씬 더 자세히 다루므로, 더 알고 싶다면 컴파일러, 디슈가, Prelude를 훨씬 더 자세히 단계별로 설명하는 튜토리얼을 읽는 것을 강력히 추천한다:
또한 궁금해하는 사람들을 위해 덧붙이자면, annah와 morte 컴파일러의 이름은 게임 Planescape: Torment의 캐릭터 이름에서 가져왔다.
Copyright © 2016 Gabriella Gonzalez. This work is licensed under CC BY-SA 4.0