PFPL 한글판

1장 추상 구문 Abstract Syntax

프로그래밍 언어를 다루기 시작할 때 우리는 보통 "문자열"부터 떠올린다. 그러나 의미론을 이야기하는 자리에서 문자열은 너무 거칠고 모호하다. 괄호 짝이 맞는지, 공백이 어디에 있는지 같은 표면적 사건은 의미와 무관하다. 우리에게 필요한 것은 표현이 가지는 구조 그 자체이며, 이를 정제해 다루는 도구가 추상 구문이다.

표현의 형태에 대한 합의

구체 구문(concrete syntax)이 시각적 표기법이라면, 추상 구문(abstract syntax)은 의미를 운반하는 골격이다. 우리는 표현을 트리로 본다. 각 노드는 어떤 연산자를 들고 있고, 그 아래로 정해진 개수의 자식이 매달려 있다. 즉, 표현은 "이 연산자가 그 아래에 무엇을 거느리는가"라는 정보의 재귀적 누적물이다.

이러한 트리를 형식화하기 위해 우리는 분류(sort)와 연산자 시그니처를 정한다. 분류 σ에 속한 표현 e가 있다고 할 때, 그것은 단일 변수이거나, 어떤 연산자 o를 머리에 두고 정해진 분류의 인자들 e₁, …, eₖ를 받은 형태이다.

왜 변수를 따로 떼어내는가

변수는 표현의 "구멍"이다. 그 자리에 무엇을 끼워 넣을지 아직 정해지지 않았다는 표시이며, 다른 어떤 노드와도 다르게 다루어야 한다. 추상 구문 트리가 갖는 가치는, 바로 이 변수와 그 변수를 구속(bind)하는 연산자가 트리 구조 안에서 명확히 분간된다는 점에 있다.

이름이 같은 두 변수가 사실은 서로 다른 구속자에 묶여 있다면 그것은 우연한 동명이인일 뿐이다. 우리는 이 차이를 구문 차원에서 제대로 잡아내기 위해 α-동치라는 동등 관계를 도입한다. 즉, λx.x와 λy.y는 — 어떤 텍스트 편집기로 보아도 다르지만 — 추상 구문의 시선에서 같은 것이다.

구속 트리(abstract binding tree)의 등장

이러한 직관을 정식화한 것이 구속 트리(ABT)다. ABT에서 한 연산자는 자식마다 "여기에서 새로 묶는 변수의 개수"를 선언한다. 예컨대 람다 추상은 한 자식 위치에서 변수 하나를 묶는다고 명시한다. 트리 위의 자유 변수와 묶인 변수는 이 선언에 따라 산출되며, 치환과 α-변환 같은 조작은 모두 이 골격 위에서 정의된다.

한 줄 요약: 추상 구문이란, "괄호와 공백을 잊고 나면 무엇이 남는가"에 대한 깔끔한 답이다.

메타이론적 한 마디

추상 구문은 의미론의 무대이다. 동작 의미와 정적 의미는 모두 이 트리 위에서 진행되는 귀납적 해설이다. 트리가 잘 정의되어야 그 위의 정의들이 잘 정의될 수 있다. 그러므로 우리는 다음 장에서 "잘 정의된 귀납"이라는 도구를 다듬는다.

2장 귀납적 정의 Inductive Definitions

언어를 다루는 우리는 끊임없이 "어떤 대상이 이 모임에 속하는가?"라는 질문을 던진다. 자연수가 그렇고, 잘 형성된 표현이 그렇고, 타입 판단이 그렇다. 이 모임을 정의하는 가장 깔끔한 도구가 귀납이다. 구체적으로는 규칙의 무리로 무엇이 그 모임에 들어갈 자격을 가지는가를 단계적으로 명시한다.

규칙으로 모임을 빚다

판단(judgment)이란 "이 대상은 이러이러하다"라는 진술의 형식이다. 가령 "n nat"이라는 판단은 n이 자연수임을 주장한다. 우리는 이 판단이 성립할 수 있는 조건들을 추론 규칙으로 풀어낸다.

규칙은 윗줄에 전제(premise), 가운데 가로선, 아래에 결론(conclusion)을 둔 그림표로 적는다. 전제가 없는 규칙은 공리(axiom)에 해당한다.

도출(derivation)이라는 증거

한 판단이 성립한다는 사실은 막연한 선언이 아니라 도출 트리로 뒷받침된다. 트리의 잎은 공리이고, 가지는 규칙의 적용이다. 즉 "succ(succ(zero)) nat"이 참이라는 말은, 그 뿌리에 해당 판단이 놓이고 두 번의 succ-규칙과 한 번의 zero-공리로 짜인 트리가 실제로 존재한다는 말이다. 도출이 있어야 판단이 있다. 그 반대 또한 우리가 강제로 그렇게 약속한 결과다.

최소 부동점, 그리고 규칙 귀납

귀납적 정의가 명시하는 모임은, 모든 규칙에 대해 닫혀 있는(closed) 모임 가운데 가장 작은 것이다. 이 "가장 작음"이 결정적이다. 그것은 우리에게 두 가지 무기를 제공한다. 첫째, 규칙 귀납(rule induction): 어떤 성질 P가 규칙들에 대해 보존된다면, 그 모임의 모든 원소는 P를 가진다. 둘째, 재귀적 정의: 함수의 값을 규칙별로 지정해도 일관된 정의를 얻을 수 있다.

예를 들어 자연수 위의 덧셈은 다음의 두 절(節)로 정의된다. add(zero, m) = m, add(succ(n), m) = succ(add(n, m)). 정의가 잘 끝남(termination)은 첫 인자에 대한 규칙 귀납으로 즉시 정당화된다.

왜 굳이 형식적으로 굴려야 하는가

이런 형식주의가 답답해 보일 때가 있다. "그냥 자연수잖아!" 그러나 우리가 다룰 대상은 곧 자연수에 그치지 않는다. 타입을 가지는 표현, 환경에 따라 평가되는 항, 효과를 추적하는 판단. 이 모든 것이 같은 골격으로 정의된다. 한 번 잘 다듬어 둔 귀납적 정의의 도구는, 이후 장에서 거의 무한히 재활용될 것이다.

규칙 귀납은 형식론자의 만능 드라이버다. 어디 하나 꽉 안 조여진 곳을 발견했다면, 십중팔구 이 도구로 풀린다.

3장 가정적·일반적 판단 Hypothetical and General Judgments

앞 장의 판단은 모두 "닫혀 있는" 진술이었다. 그러나 실제 언어를 다룰 때 우리는 "만약 x가 자연수라면 x + 1도 자연수다"처럼, 자유 변수에 대한 가정을 짊어진 판단을 다루어야 한다. 이런 판단을 가정적 판단(hypothetical judgment)이라 부른다. 또한 임의의 변수 이름을 한꺼번에 다루기 위한 일반적 판단(general judgment)도 함께 등장한다.

가정 컨텍스트 Γ

유한한 가정의 묶음을 컨텍스트 Γ라고 적는다. 변수와 그에 따르는 분류 또는 타입의 쌍이 콤마로 이어진 목록이다. 가정적 판단은 다음의 모양을 가진다.

Γ ⊢ J

해석은 단순하다. 컨텍스트 안의 가정들이 모두 성립한다고 받아들인다면, 결론 J도 성립한다는 뜻이다. 이때 Γ가 비면 우리는 닫힌 판단으로 돌아온다. 즉 · ⊢ J는 J 그 자체와 같다.

구조 규칙

가정적 판단은 그 자체가 다시 추론 규칙으로 빚어진다. 가장 기본적인 것은 가정 규칙이다.

그리고 컨텍스트의 동작에 관한 구조 규칙(structural rules)이 있다. 약화(weakening)는 새로운 가정을 더 추가해도 기존의 도출은 여전히 유효함을 말한다. 교환(exchange)은 가정의 순서를 뒤섞을 수 있음을, 수축(contraction)은 동일한 가정이 여러 번 나오면 한 번으로 줄여도 좋음을 말한다. 마지막으로 절단(substitution)은 가장 무거운 규칙이다. Γ ⊢ d : τ이고 Γ, x:τ ⊢ J라면 Γ ⊢ [d/x]J가 성립한다. 즉 가정 자리에 실제 도출을 끼워 넣을 수 있다.

일반적 판단과 매개변수

한편 우리는 종종 어떤 변수 이름이 무엇이든 상관없는 진술을 다룬다. 이를테면 "임의의 변수 x에 대해 x = x"가 그렇다. 이런 판단을 일반적 판단이라 부르며, ∀-처럼 양화의 형식을 띈다. 형식적으로는 도출이 변수 이름의 선택과 무관하게 동일한 형태를 띄는 것을 보장한다. 일반적 판단과 가정적 판단을 함께 다루면 우리는 거의 모든 언어 정의에 필요한 표현력을 얻는다.

왜 이 구별이 본질적인가

가정 규칙·약화·절단이라는 세 축은 그저 편의를 위한 장식이 아니다. 이들은 의미론이 합성적으로 이루어질 수 있게 만든다. 부분에 대한 의미가 정해지면, 그것을 가정으로 받아들인 더 큰 표현의 의미가 자동으로 정해진다는 보장이 절단 규칙이다. 이후 4장 이후의 타입 시스템은 사실상 이 세 가지 위에서 연주되는 변주곡일 뿐이다.

절단 정리(cut elimination)가 증명론의 만년 베스트셀러인 이유: 모든 어려운 일이 결국은 그 한 줄로 환원되기 때문이다.

4장 정적 의미론 (타입 시스템) Statics

정적 의미론은 프로그램이 실행되기 전에, 즉 한 줄도 돌리기 전에 그 프로그램에 대해 무엇을 단언할 수 있는가를 다룬다. 이 단언의 핵심 도구가 타입이며, 타입 시스템은 표현이 어떤 타입을 가지는지를 형식적으로 결정한다. 이 장에서는 작은 표현 언어 E를 도입하고, 그 위에 타입을 부여하는 규칙을 세운다.

표현 언어 E의 골격

언어 E는 두 가지 분류를 가진다. 타입 τ와 표현 e이다. 타입은 자연수 타입 num과 문자열 타입 str 정도로 두자. 표현은 변수 x, 수치 리터럴 num[n], 문자열 리터럴 str[s], 덧셈 plus(e₁; e₂), 이어붙임 cat(e₁; e₂), 길이 len(e), 그리고 지역 정의 let(e₁; x.e₂)로 충분하다. 마지막 항은 "값을 묶고 그 변수의 사정거리 안에서 본문을 평가"하는 구속자이다.

타입 부여 판단

타입 부여 판단은 다음의 모양이다.

Γ ⊢ e : τ

Γ는 변수의 타입 가정 묶음이다. 규칙은 표현의 모양을 따라간다.

구조적 성질들

타입 부여 판단에 대해 약화·교환·치환이 모두 성립한다. 특히 치환 보조정리(substitution lemma)는 "Γ ⊢ d : τ이고 Γ, x:τ ⊢ e : σ이면 Γ ⊢ [d/x]e : σ"이라 말한다. 또한 표현 한 개에 대해 타입은 유일하게 결정된다. 즉 Γ ⊢ e : τ이고 Γ ⊢ e : τ'이면 τ = τ'이다. 이 유일성은 후속 장에서 보존 정리를 증명할 때 결정적으로 쓰인다.

타입 시스템은 일종의 보수적 검열관이다. 의심스러우면 통과시키지 않는 쪽이 안전하다.

메타이론의 약속

아직 우리는 e가 실행되면 무슨 일이 일어나는지 정의하지 않았다. 정적 의미론은 그것 없이도 의미가 있다. "plus(num[3]; str["네"])" 같은 표현은 어떤 실행을 정의하기도 전에 거부할 수 있고, 거부해야 한다. 다음 장에서 우리는 동작을 정의하고, 그 다음 장에서 두 의미론이 서로 어긋나지 않음을 증명할 것이다.

5장 동적 의미론 (실행) Dynamics

정적 의미론이 "이 표현은 합당한가?"를 다루었다면, 동적 의미론은 "이 표현이 실행되면 무슨 일이 벌어지는가?"를 다룬다. 우리는 표현을 한 단계씩 변형하는 작은 단계 의미론(small-step semantics)을 채택한다. 이는 추상 기계 위에서 한 발자국씩 움직이는 그림과 잘 어울린다.

값과 단계

먼저 어떤 표현이 더 이상 줄어들지 않는 "최종 상태"인가를 규정해야 한다. 이를 값 판단 e val이라 적는다. 우리의 작은 언어에서는 수치 리터럴 num[n]과 문자열 리터럴 str[s]가 값이다.

다음으로 한 걸음 진행 판단 e ↦ e'을 정의한다. "표현 e는 한 단계 뒤 e'가 된다"는 의미이다. 두 종류의 규칙이 있다. 어딘가에 묻혀 있는 부분식부터 우선 평가하라는 합동 규칙(congruence)과, 진짜로 일을 해내는 지시 규칙(instruction)이다.

let의 평가 전략

let(e₁; x.e₂)는 두 가지 자연스러운 해석을 갖는다. 이름 호출(call-by-name)이라면 e₁을 그대로 본문에 치환하고, 값 호출(call-by-value)이라면 e₁을 먼저 값으로 만든 뒤 치환한다. 우리는 후자를 채택한다.

결정성과 진행의 그림

이렇게 정의된 진행 관계는 결정적(deterministic)이다. 즉 임의의 e에 대해 한 단계 뒤로 가는 결과는 많아야 하나이다. 합동 규칙들이 평가 순서를 한 가지로 못박기 때문이다. 또한 우리는 정상화되거나 막혀 있는(stuck) 두 가지 종착점을 상상할 수 있다. 값에 도달하면 정상 종료, 그러나 어떤 규칙도 적용되지 않고 값도 아닌 상태에 갇히면 그것이 막힘이다.

막힘은 컴퓨터과학의 미아(迷兒)다. 이 아이를 만들지 않는 것이 타입 시스템의 가장 절박한 약속이다.

다음 장으로의 다리

그렇다면 "잘 타이핑된 프로그램은 결코 막히지 않는다"는 약속이 정말 지켜지는가? 이 한 문장이 다음 장의 주제다.

6장 타입 안전성 (Progress & Preservation) Type Safety

정적 의미론과 동적 의미론을 따로 정의해 두었으면, 둘이 서로 잘 어울리는지를 점검할 차례다. 어울림의 표준은 두 정리로 요약된다. 진행(progress)과 보존(preservation). 이 두 정리를 함께 일컬어 "타입 안전성(type safety)"이라 부르며, 그 의미는 "잘 타이핑된 프로그램은 막히지 않는다"이다.

두 정리의 진술

편의를 위해 모든 판단은 닫힌 표현 위에서, 즉 · ⊢ e : τ의 형태로 둔다. 두 정리는 다음과 같다.

보존. · ⊢ e : τ이고 e ↦ e'이면, · ⊢ e' : τ이다.

진행. · ⊢ e : τ이면, e val이거나 어떤 e'에 대해 e ↦ e'이다.

요컨대 한 걸음을 걸어도 타입은 변치 않으며(보존), 막히지 않는다(진행). 두 정리를 합치면 잘 타이핑된 프로그램은 영원히 막히지 않거나 끝내 값에 도달함을 얻는다.

증명의 골격

두 정리 모두 규칙 귀납의 표준 응용이다. 보존 정리는 e ↦ e'의 도출에 대한 귀납으로 진행한다. 합동 규칙들에서는 부분식의 타입이 보존된다는 가설을 가져다 그대로 쓰면 된다. 지시 규칙에서는 종종 별도의 보조정리가 필요하다. 가장 자주 쓰이는 것이 치환 보조정리이다. 예컨대 let(v; x.e₂) ↦ [v/x]e₂의 경우, · ⊢ v : τ₁과 x:τ₁ ⊢ e₂ : τ₂로부터 · ⊢ [v/x]e₂ : τ₂를 끌어내는 것이 핵심이다.

진행 정리는 타입 부여의 도출에 대한 귀납으로 진행한다. 변수의 경우는 Γ가 비어 있다는 가정에 의해 비어 있는 케이스이고, 리터럴은 곧바로 값이며, 합성적 표현들에서는 부분식이 값인 경우와 그렇지 않은 경우로 나누어 합동 규칙 또는 지시 규칙을 적용하면 된다.

표준 형식 보조정리

진행 증명을 매끈하게 만드는 도구가 표준 형식 보조정리(canonical forms lemma)이다. "닫힌 값 v가 num이면 v는 어떤 n에 대해 num[n] 모양이다"와 같이, 타입에 따라 값의 모양을 좁혀준다. 이 보조정리는 타입 시스템을 작성한 사람이 의도한 것이 실제로 동적으로도 성립하는지 확인하는 정직한 거울이다.

진행 정리가 한 번 깨지면, 그것은 거의 항상 표준 형식 보조정리의 어딘가가 어긋났다는 신호다.

안전성이라는 약속의 무게

타입 안전성은 단지 깔끔한 정리가 아니다. 그것은 언어 설계자가 사용자에게 거는 계약이다. "내가 통과시킨 프로그램은 결코 정의되지 않은 행동에 빠지지 않는다." 이 계약을 지키지 못하는 시스템은 — 아무리 표현력이 풍부해 보이더라도 — 전제로부터 다시 살펴볼 필요가 있다. 다음 장에서는 진행을 한꺼번에 보지 않고, 시작에서 끝까지 한 번에 평가하는 또 다른 시각을 도입한다.

7장 평가 동역학 (대형 단계 의미론) Evaluation Dynamics

앞 장까지의 동적 의미론은 한 발씩 옮기는 카메라였다. 그러나 어떤 분석에서는 한 발씩 보는 일이 오히려 시야를 흐린다. 우리는 종종 "이 표현은 어떤 값으로 평가되는가?"만을 단번에 묻고 답하고 싶다. 이런 시각이 평가 동역학(evaluation dynamics), 흔히 대형 단계 의미론(big-step semantics)이라 불린다.

평가 판단 e ⇓ v

평가 판단은 다음의 모양을 가진다.

e ⇓ v

의미는 단순하다. 표현 e는 평가되어 값 v가 된다. 규칙은 다시 표현의 모양을 따라간다.

여기에는 "한 걸음" 같은 개념이 없다. 부분식이 값에 도달했다는 가설들을 모아, 전체가 어떤 값에 도달하는지를 한꺼번에 결론짓는다.

작은 단계와의 일치

두 의미론은 같은 언어를 다루는 한, 같은 결과를 내야 한다. 형식적으로 다음의 등가가 성립한다.

e ⇓ v ⇔ e ↦* v이고 v val

여기서 ↦*는 한 걸음의 반사·이행적 폐포이다. 한쪽 방향(⇒)은 ⇓의 도출에 대한 귀납으로, 다른 쪽 방향(⇐)은 ↦*의 길이에 대한 귀납으로 증명된다. 후자에서는 한 걸음을 평가에 합치는 보조정리, 즉 "e ↦ e'이고 e' ⇓ v이면 e ⇓ v"가 결정적인 역할을 한다.

두 시각의 장단

대형 단계 의미론은 컴팩트하고, 합성적 추론에 자연스럽다. 그러나 그것이 잘 작동하는 곳은 종결성이 보장된 단편이다. 평가 판단은 본질적으로 "값에 도달했다"를 전제로 결론을 짓기 때문에, 발산하는(diverging) 표현이나 효과적 동작을 직접 다루기에는 어색하다. 작은 단계 의미론은 그런 문맥에서도 침착하다. 한 걸음씩만 약속하므로, 끝나지 않는 계산 자체를 무한 도출 시퀀스로 표현할 수 있다.

한쪽은 결과만 보고, 한쪽은 과정을 본다. 둘 다 필요하다 — 인생도 언어도.

맺으며: Part II의 마무리

이로써 우리는 정적 의미론, 동적 의미론, 그리고 둘의 정합성, 그리고 같은 동적 의미론을 다른 시각으로 보는 두 가지 방식까지 갖추었다. 다음 부에서 우리는 이 도구들 위에 함수, 합타입, 곱타입, 재귀 같은 본격적인 구문을 얹어 가며, 이 골격이 얼마나 멀리까지 견디는지 시험할 것이다.

8장 함수 정의와 값 Function Definitions and Values

지금까지 우리가 다룬 산술 표현식들에는 한 가지 결정적인 것이 빠져 있다. 바로 추상이다. 같은 패턴의 계산을 매번 새로 적어내야 한다면, 그 언어는 사실상 매크로 치환기에 가깝다. 이 장에서는 함수를 일급 시민으로 격상시키지는 않되, 적어도 이름 붙은 정의로서 다루는 첫 단계를 밟는다.

정의에 의한 함수

가장 소박한 형태의 함수는 "이름 + 매개변수 목록 + 본문"이라는 삼중주이다. fun f(x:τ₁):τ₂ = e 와 같은 선언은 실행되지 않고, 환경에 등록되어 호출될 때 비로소 본문이 풀려난다. 이때의 의미론은 단순한 매크로 펼침과 미묘하게 다르다. 매개변수 x는 자유 변수가 아니라 묶인 이름이며, α-동치 하에서 의미가 보존되어야 한다.

호출 f(e)의 형식 규칙은 직관적이다.

여기서 Σ는 전역 함수 시그니처들의 모임이다. 본문 e는 Σ에 속한 다른 이름들을 자유롭게 호출할 수 있으나, 자기 자신은 호출할 수 없다. 적어도 이 장의 시점에서는 그렇다. 재귀는 다음 단계로 미뤄두자.

값으로서의 함수

이름 붙은 정의는 편리하지만 한계가 분명하다. 함수를 인자로 넘기거나, 반환값으로 돌려보내거나, 자료구조에 담을 수 없기 때문이다. 다음 발걸음은 함수를 값으로 취급하는 것이다. 즉 람다 추상 λ(x:τ).e를 표현식의 한 종류로 인정하고, τ₁ → τ₂라는 새 타입을 도입한다.

호출의 동역학은 β-축약이다. (λ(x:τ).e)(v) ↦ [v/x]e. 호출 시점에 인자가 이미 값인지를 따지느냐 마느냐에 따라 호출-바이-값과 호출-바이-네임이 갈라지지만, 이 장에서는 전자에 머무른다.

함수를 값으로 취급한다는 말은, 함수란 본디 "쓰는 것"이 아니라 "주고받는 것"이라는 선언이다. 매크로의 시대는 이로써 끝난다.

메타이론 한 마디

정의에 의한 함수와 값으로서의 함수는 표현력이 같은가? 결론부터 말하면 그렇지 않다. 일급 함수가 있는 언어에서는 정의 모음을 손쉽게 흉내낼 수 있지만, 그 역은 일반적으로 성립하지 않는다. 고차성은 표현력의 질적 도약이며, 9장의 System T는 그 도약 위에서 비로소 가능해진다.

9장 고차 타입의 System T System T of Higher Type

자연수 위에서 종료하는 모든 함수를 적고 싶다면 어디까지 가야 할까? Gödel의 답은 "충분히 높은 차수까지"였다. System T는 자연수와 함수 타입, 그리고 원시 재귀자(recursor) 하나로 이루어진 미니멀한 언어이지만, 그 표현력은 전체 함수의 거대한 부분 클래스를 포함한다.

구문과 타입

타입은 τ ::= nat | τ₁ → τ₂로 단정하게 시작한다. 항은 변수, 람다, 적용, 0, 후속자 s(e), 그리고 재귀자 rec e {z ↦ e₀ | s(x) with y ↦ e₁}로 구성된다. 재귀자의 형식 규칙은 다음과 같다.

핵심은 y이다. 재귀 호출의 결과를 직접 다시 부르는 대신, 한 단계 아래의 결과를 이미 계산된 값으로 받아쓴다. 이는 무한 루프를 원천 봉쇄한다.

동역학과 종료성

축약 규칙은 두 갈래다. rec z {…}는 e₀로 가고, rec s(n) {…}는 [n, rec n {…} / x, y]e₁로 풀린다. 매번 인자 자연수가 한 단계씩 내려가므로, 어떤 입력에서 시작해도 유한 단계 안에 멈춘다.

덧셈은 가벼운 손풀기 예다.

add ≡ λ(m:nat).λ(n:nat). rec m {z ↦ n | s(_) with y ↦ s(y)}

곱셈, 거듭제곱, 아커만 함수의 잘려나간 형태까지 모두 같은 틀에 들어간다. 다만 진짜 아커만은 차수가 부족해 표현되지 않는데, 이는 결함이 아니라 설계의 정직함이다.

고차의 효용

왜 굳이 차수를 올려야 하는가? 어떤 자연수 함수는 1차 원시 재귀로는 정의되지 않지만, 함수를 인자로 받는 재귀자 사용을 허용하면 비로소 잡힌다. (nat → nat) → nat이나 그보다 높은 타입을 매개로 삼아야만 도달 가능한 함수들이 있다는 사실은 표현력과 타입 차수 사이의 미묘한 사다리를 보여준다.

아커만이 위로 솟구쳐 도망가도, 충분한 차수의 사다리만 있다면 따라잡을 수 있다. 단, ω차에는 영영 닿지 못한다 — 그 너머는 9장의 영토가 아니다.

메타이론 한 마디

System T로 정의 가능한 함수 클래스는 정확히 Gödel의 원시 재귀 함수족이며, 이는 Peano 산술에서 종료성이 증명되는 함수들과 일치한다. 즉 "표현력 = 증명력"이라는 깔끔한 등식이 성립한다. 그러나 모든 계산 가능 함수를 잡으려면, 종료를 포기해야 한다. 다음 장의 PCF는 바로 그 거래의 형식이다.

10장 Plotkin의 PCF Plotkin's PCF

전체 함수만으로는 진짜 프로그래밍 언어의 영혼을 담을 수 없다. 무한 루프와 비종료, 발산하는 계산 — 이 모든 그림자를 끌어안기 위해 Plotkin은 부분성을 정면으로 받아들이는 미니 언어 PCF를 설계했다. 종료를 보장하는 재귀자 대신, 일반 재귀를 도입하는 것이다.

구문과 타입

타입은 System T와 똑같다. 차이는 항에 있다. 재귀자가 사라지고, 그 자리를 부동점 연산자 fix(x:τ.e)가 차지한다. 또한 자연수 분기를 위한 ifz e {z ↦ e₀ | s(x) ↦ e₁}를 갖춘다.

의미는 자기 자신과 동치인 항을 한 번에 만들어낸다는 것이다. 동역학 규칙도 그만큼 솔직하다.

fix(x:τ.e) ↦ [fix(x:τ.e)/x] e

축약이 끝없이 풀려나갈 가능성을 안고 있는데, 이게 바로 PCF가 부분 함수의 언어인 까닭이다.

발산을 허용한 대가

이제 fix(x:nat.x)와 같은 무해한 듯 위험한 항이 합법적으로 타입을 갖는다. 평가하면 영영 자기 자신으로 돌아오며 결코 값이 되지 않는다. 우리는 이를 발산이라 부르고, ⇑로 표기한다. 진보 정리는 살아남되, "값으로 끝나거나 무한히 한 발씩 나아간다" 형태로 약화된다.

예: 계승 함수

fact ≡ fix(f:nat→nat. λ(n:nat). ifz n {z ↦ s(z) | s(m) ↦ mul(n, f(m))})

System T에서 짠 계승보다 자연스럽다. 종료가 자명하지 않다는 점 또한 자연스럽다 — 일반 재귀는 자유와 위험을 함께 준다.

PCF의 부동점은 약속한다. "당신이 필요로 하는 자기 참조는 내가 제공하겠다. 다만 멈춘다는 보장은 함께 가지 않는다."

메타이론 한 마디

PCF는 "고차 함수형 언어의 본질을 담은 가장 작은 표본"으로 자주 인용된다. Plotkin이 1977년에 보였듯, 이 언어의 연산적 의미와 표시적 의미 사이에는 미묘한 간극이 있다 — 표시적 의미에서 동치인 두 항이 연산적으로 구별 불가능하지 않을 수 있다는 완전 추상성 문제다. PCF는 그 작음에 비해 놀라울 만큼 깊은 메타이론을 거느린다.

11장 곱 타입 Product Types

현실의 데이터는 좀처럼 단독으로 다니지 않는다. 좌표는 두 수의 짝, 사람은 이름과 나이의 짝, 기록은 여러 필드의 묶음이다. 곱 타입은 이러한 "함께 다님"을 가장 단순한 형태로 형식화한다.

이항 곱과 단위

두 타입 τ₁, τ₂에 대해 곱 τ₁ × τ₂는 짝 ⟨e₁, e₂⟩의 타입이다.

해체 규칙은 두 사영 e·l, e·r로 주어지며, 동역학은 명확하다. ⟨v₁, v₂⟩·l ↦ v₁, ⟨v₁, v₂⟩·r ↦ v₂. 단위 타입 unit은 0항 곱으로, 유일한 값 ⟨⟩를 갖는다. "정보를 거의 주지 않는 타입"이지만 이후 합 타입과 짝지어 큰 역할을 맡는다.

유한 곱: 라벨이 있는 묶음

인덱스 집합 I = {l₁, …, lₙ}에 대해 ×{l : τ_l}_{l ∈ I}를 도입한다. 항은 라벨이 있는 묶음 ⟨l ↪ e_l⟩_{l ∈ I}이고, 사영은 e·l이다. 위치가 아니라 이름으로 접근한다는 점에서 레코드의 형식론적 골격이다.

두 가지 평가 방식

짝의 평가는 두 가지 결을 갖는다. 열심히(eager) 만들면 짝을 구성하기 전에 두 성분을 모두 값으로 환원한다. 게으르게(lazy) 만들면 짝은 곧장 값이 되고, 사영을 만났을 때 비로소 해당 성분을 평가한다. 표현력에는 미묘한 차이가 생긴다 — 게으른 곱에서는 ⟨fix(x.x), 0⟩·r이 0이 되지만, 열심인 곱에서는 발산한다.

짝을 만든다는 것은 약속이다. 열심한 약속은 즉시 갚고, 게으른 약속은 청구가 들어와야 갚는다.

메타이론 한 마디

곱 타입의 도입·소거 규칙은 자연 연역의 합집(conjunction) 규칙과 정확히 평행하다. Curry–Howard 대응 하에서 곱은 논리곱이고, 사영은 A ∧ B ⊢ A의 증명이다. 형식론에서는 이런 평행이 우연이 아니라 설계의 거울이다.

12장 합 타입 Sum Types

곱이 "함께"의 형식이라면, 합은 "혹은"의 형식이다. 어떤 값은 이 모양일 수도 있고 저 모양일 수도 있다. 이 선택지를 타입 차원에서 명시할 때 비로소 우리는 "데이터가 어떤 모양인지" 정직하게 적을 수 있다.

이항 합과 빈 타입

합 τ₁ + τ₂의 항은 두 가지 주입 중 하나다.

그리고 마찬가지로 r·e : τ₁ + τ₂가 있다. 해체는 분기로 이루어진다.

빈 타입 void는 0항 합이다. 값이 존재하지 않는 타입이며, 분기 규칙은 0개의 분기를 요구한다 — 즉 void 값을 받았다고 가정하면 무엇이든 결론지을 수 있다. 모순으로부터 임의의 결론. 논리에서 본 적 있는 풍경이다.

유한 합: 태그된 합집합

+{l : τ_l}_{l ∈ I}는 라벨로 인덱스된 합이다. 옵션 타입, 결과 타입, 색깔 열거 — 모두 이 형식의 인스턴스다. 가령 option(τ) ≡ +{none : unit, some : τ}는 unit과의 합으로 결측을 표현한다.

예: 트리 형태

tree ≈ +{leaf : unit, node : tree × nat × tree}

물론 이 정의는 자기 참조이므로, 진짜로 닫힌 형태로 쓰려면 다음 장 이후의 귀납형이 필요하다. 그러나 합 타입이 모양을 가르고, 곱 타입이 한 모양 안의 데이터를 묶는다는 분업은 이미 분명하다.

합 타입이 없다면 우리는 "이건 사실 두 가지 중 하나야"라고 말할 수밖에 없다. 합 타입이 있으면, 컴파일러도 그 말을 이해한다.

메타이론 한 마디

합은 Curry–Howard 하에서 논리합에 대응한다. 분기 분석은 "A ∨ B가 주어졌을 때 어느 쪽이든 같은 결론을 끌어낼 수 있어야 한다"는 추론 그 자체다. 곱과 합은 서로의 거울상이며, 이 대칭성은 다음 장의 패턴 매칭에서 한층 더 분명한 모습으로 드러난다.

13장 패턴 매칭 Pattern Matching

합과 곱이 갖춰지자, 분기와 사영을 일일이 적는 일이 부끄러울 만큼 번거로워진다. 패턴 매칭은 데이터의 모양을 "그림"으로 적게 해주는 표기 장치이자, 그 자체로 흥미로운 형식론적 대상이다.

패턴의 문법

패턴은 항을 거꾸로 본 것이다. 변수 패턴 x, 와일드카드 _, 곱 패턴 ⟨p₁, p₂⟩, 합 패턴 l·p가 기본 재료다. 매칭 표현은 다음과 같이 적는다.

match e {p₁ ↦ e₁ | … | pₙ ↦ eₙ}

각 패턴은 자기 자신만의 변수 컨텍스트를 만들고, 그 아래에서 우변이 타입을 검사받는다.

여기서 p : τ ⊣ Δ는 "타입 τ의 패턴 p가 변수 컨텍스트 Δ를 만들어낸다"고 읽는다.

완전성과 비완전성

패턴 모음이 모든 가능한 값의 모양을 덮느냐 — 이것이 완전성(exhaustiveness) 검사다. 합 타입의 모든 라벨이 등장하는가? 곱 안의 분기가 빠짐없는가? 이론적으로는 패턴들의 집합이 타입의 값 집합에 대한 분할을 이루어야 한다. 실용적으로는 컴파일러가 누락된 케이스를 짚어주거나, 적어도 경고로 알린다.

중첩과 컴파일

중첩된 패턴은 깊이 우선 분기 트리로 펼쳐진다. match e {⟨l·x, y⟩ ↦ …}는 먼저 짝을 분해하고, 그 첫 성분이 l로 태그되었는지 검사하고, 안의 x를 묶는 일련의 과정으로 풀어쓸 수 있다. 이 펼침은 형식적으로 정의 가능하며, 표면 언어의 표현력은 핵심 언어의 분기와 사영의 합으로 환원된다.

패턴 매칭은 추리 소설의 단서표와 같다. 데이터의 모양을 그림으로 그려두면, 컴파일러는 우리가 빠뜨린 용의자를 친절하게 일러준다.

메타이론 한 마디

패턴은 "직관적 표기 → 형식적 핵심"으로 번역되는 다리다. 이 번역이 잘 정의되어 있고 의미를 보존한다는 사실은, 표면 문법과 핵심 의미론을 분리하는 이층 구조가 형식론에서 얼마나 유용한지를 보여준다. 사용자는 그림을 그리고, 이론은 그것을 풀어 쓴다.

14장 제네릭 프로그래밍 Generic Programming

자료구조의 모양은 다양하지만, 그 위에서 하고 싶은 일은 종종 같다. 모든 잎에 함수를 적용하고 싶다, 모든 정수 필드를 두 배로 만들고 싶다, 구조를 보존하면서 한 자리만 갈아끼우고 싶다. 제네릭 프로그래밍은 이 "모양에 따라 자동으로 행동이 정해지는" 일을 형식적으로 다룬다.

타입 함수와 위치

타입 변수 α를 매개로 한 타입 표현 t[α]를 생각하자. 이는 α의 위치에 따라 모양이 달라지는 "구멍 뚫린" 타입이다. 가령 t[α] = α × (α → nat)은 양의(positive) 위치와 음의(negative) 위치 양쪽에 α가 등장한다. 제네릭 변환은 이 위치 분석에 의지한다.

맵 연산

가장 자주 만나는 제네릭 연산은 map_t : (α → α') → t[α] → t[α']이다. 단, t에 음의 위치에서 α가 등장하면 이 단방향 맵은 정의되지 않는다. 양방향이 필요해지기 때문이다. 그래서 일반적인 정의에서는 t를 양의 위치만 사용하는 공변(covariant) 타입 함수로 제한하거나, 두 방향의 함수를 함께 받는다.

map_{τ₁ × τ₂}(f, ⟨e₁, e₂⟩) ≡ ⟨map_{τ₁}(f, e₁), map_{τ₂}(f, e₂)⟩

곱 타입 위에서는 성분별로, 합 타입 위에서는 라벨을 보존한 채 안쪽으로 내려가며, 함수 타입에서는 입력을 후방으로 변환하고 출력을 전방으로 변환한다 — 이것이 음의 위치의 비밀이다.

구조에 따른 정의

이런 변환은 타입의 구조에 대한 재귀로 정의된다. 즉 타입을 인덱스 삼아 함수를 만든다는 뜻이다. 이 점에서 제네릭 프로그래밍은 의존 타입의 사촌이지만, 우리는 메타 수준의 구조 재귀로도 충분히 많은 일을 해낼 수 있다.

제네릭은 게으름의 형식이다. "이 모양에 대해 매번 적기는 귀찮으니, 모양 자체를 인자로 받자." 좋은 게으름은 좋은 추상이 된다.

메타이론 한 마디

제네릭 변환의 존재는 타입 시스템의 부수적 사치가 아니다. 그것은 타입을 단순히 값을 분류하는 라벨이 아니라, 그 위에서 함수를 자동으로 합성할 수 있는 대수적 대상으로 본다는 선언이다. 이 관점은 다음 장의 귀납형에서 정점을 찍는다 — 거기서는 타입 자체가 부동점으로 정의되며, 제네릭 도구는 그 부동점을 다루는 표준 수단이 된다.

15장 귀납·공귀납 타입 Inductive and Co-Inductive Types

자연수, 리스트, 트리는 "유한하게 쌓아 올린 데이터"이고, 무한 스트림과 게으른 객체는 "끝없이 관찰할 수 있는 데이터"다. 두 세계는 형식적으로 거울상이며, 이 장은 양쪽을 같은 언어 안에 들여놓는다.

귀납형: μ로 묶기

타입 함수 t[α]가 공변일 때, 귀납형 μα.t[α]는 "이 등식 α ≅ t[α]의 최소 해"로 이해된다. 그 항은 접기 fold(e)로 만들고, 펼치기로 해체한다.

자연수는 μα. unit + α이고, 리스트는 μα. unit + (τ × α)다. 진짜 재귀자는 다음과 같이 등장한다.

rec_{μα.t[α]} : (t[ρ] → ρ) → μα.t[α] → ρ

"한 단계의 펼친 모양에서 답을 만드는 법"을 주면, 임의의 깊이까지 자동으로 끌어 올린다. 종료는 부동점이 최소라는 사실에서 따라온다.

공귀납형: ν로 풀어내기

같은 등식 α ≅ t[α]의 최대 해는 공귀납형 να.t[α]다. 이쪽의 항은 풀어내기 unfold로 만든다.

"한 단계 관찰을 만들어내는 법"을 주면, 무한히 관찰 가능한 객체가 된다. 자연수의 거울상인 자연수-혹은-무한대 nat∞ = να. unit + α는 종료가 보장되지 않은 카운터를 정직하게 표현한다. 무한 스트림 να. τ × α는 머리와 꼬리를 영원히 내어준다.

두 세계의 대칭

귀납형은 "구성"의 언어이고, 공귀납형은 "관찰"의 언어다. 전자에서는 어떻게 지어졌는지를 가지고 분석하고, 후자에서는 무엇이 보이는지를 가지고 정의한다. 한쪽은 패턴 매칭, 다른 쪽은 코쇼크-매칭이라 부르는 이중성이 자연스레 나온다.

귀납이 "어디서 왔는가"라면, 공귀납은 "무엇을 보여주는가"다. 같은 방을 안에서 보느냐, 밖에서 보느냐의 차이.

메타이론 한 마디

두 부동점의 공존은 형식론의 우아한 균형을 보여준다. 최소 부동점은 유한한 증인을, 최대 부동점은 가능한 모든 일관된 행동을 잡는다. 후자는 PCF의 일반 재귀를 다른 각도에서 끌어안는 길이기도 하며, 부분성을 데이터의 모양 자체에 새긴다는 점에서 깊다. 본질적으로 같은 등식이 두 가지 합법적 해를 갖는다는 사실 — 이 작은 비대칭이 데이터의 유한성과 무한성이라는 거대한 차이를 만든다.

16장 타입 없는 λ-계산 Untyped λ-Calculus

타입의 그늘에서 한 발 벗어나 보자. 모든 항이 동일한 자격으로 굴러다니는 세계, 즉 단 하나의 문법 범주만으로 계산을 흉내내는 자리에서 우리는 무엇이 가능하고 무엇이 잃어버려지는지를 가늠하게 된다.

왜 타입을 벗기는가

타입 시스템은 의미 있는 항만 골라내는 검열관이다. 이 검열관을 잠시 해고하면 이상한 일이 벌어진다. 자기 자신을 인자로 받는 항도, 자신을 호출하는 함수도 모두 적법해진다. 이러한 자유에는 대가가 따른다. 항의 정상화는 보장되지 않으며, "값"의 개념은 함수 추상으로 축소된다. 그러나 이 축소된 세계가 충분히 풍부하다는 사실이 바로 이 장의 핵심 주장이다.

형식

타입 없는 λ-계산 Λ의 항은 단 세 가지로 충분하다.

e ::= x | λx.e | e₁(e₂)

평가는 β-축약 한 줄로 요약된다. (λx.e)(e′) ↦ [e′/x]e. 여기서 호출 전략을 어떻게 잡느냐에 따라 의미는 갈린다. 이름값 호출(call-by-name)은 인자를 손대지 않은 채 대입하고, 값 호출(call-by-value)은 인자를 먼저 값으로 끌고 간 뒤에야 함수에 건넨다. 두 전략의 표상적 차이는 발산하는 항을 만났을 때 비로소 드러난다.

표현력의 시범

자연수, 부울, 쌍, 합 — 이 모든 자료 구조가 함수 하나로 표현된다. 가령 자연수 n은 어떤 함수 f와 시작값 z를 받아 f를 n회 적용하는 항으로 정의된다(처치 인코딩). 이때 후속자, 덧셈, 곱셈은 모두 λ-항으로 표현 가능하며, 재귀는 부동점 결합자 Y = λf.(λx.f(x x))(λx.f(x x))가 떠받친다. Y(F)는 자기 자신을 인자로 받는 F의 부동점이다.

메타이론적 코멘트

타입 없는 λ-계산은 튜링 완전하다. 즉, 정상화하지 않는 항이 존재한다 — (λx.x x)(λx.x x)가 그 표본이다. 이 발산 가능성은 약점이 아니라 표현력의 영수증이다. 직관주의 형식 체계가 보장하던 정지 정리(strong normalization)는 여기서 깨지고, 그 자리에 자기 적용이 들어온다. 다음 장에서 우리는 이 무정형의 세계를 다시 타입의 어휘로 흡수하는 한 가지 방법, 즉 동적 타이핑을 다룬다.

"타입이 없다"는 말은 사실 "타입이 하나뿐이다"라는 말의 다른 표현이다.

17장 동적 타이핑 Dynamic Typing

동적 언어가 "타입이 없다"는 통념은 절반만 맞다. 실제로는 모든 값이 자신의 종류를 표시하는 꼬리표를 달고 다닐 뿐, 그 꼬리표가 정적 단계가 아니라 실행 단계에서 검사된다. 이 장에서는 그 꼬리표 사고방식을 형식화한다.

한 타입, 여러 클래스

동적 타입 언어 DPCF의 모든 항은 단일한 정적 타입 dyn을 가진다. 그러나 dyn 값은 내부적으로 클래스(class)로 구분된다. 자연수, 부울, 쌍, 함수 등은 각각의 생성자를 통해 dyn으로 주입(injection)되고, 사용 시점에 클래스 검사를 통해 사영(projection)된다. 이렇게 보면 동적 언어는 사실상 거대한 합 타입(sum type)을 등에 짊어지고 다니는 정적 언어다.

형식

여기서 num!은 자연수 클래스로의 주입자다. 반대로 사영은 검사를 동반한다.

실행 시 num?(num!(v))는 v로 풀리지만, num?(fun!(v))는 클래스 불일치 오류로 정지한다. 즉 정적으로는 모두 dyn → dyn으로 통하던 호출이, 동적으로는 클래스 부조화를 만나면 실패한다.

왜 이런 설계가 매력적인가

동적 타이핑의 매력은 "지금은 모르겠다"를 합법화한다는 점이다. 프로토타이핑 단계에서 자료 구조는 자주 변하고, 정적 타이핑은 그때마다 부담을 지운다. 모든 값이 하나의 타입으로 통일되면, 컬렉션은 이질적이 되고 함수는 다형적으로 보이며, REPL은 즉시 응답한다. 이는 형식 체계의 결함이 아니라 의도적 결정이다 — 검사 시점을 늦춤으로써 표현의 자유를 사들인 것이다.

메타이론적 코멘트

안전성 정리(safety)는 살아남는다. 다만 진보(progress) 진술이 약화될 뿐이다. 잘 타입된 항은 값이 되거나, 한 걸음 진행하거나, 클래스 불일치로 정지한다. 이 세 번째 출구가 정적 타입에는 없던 것이다. 결국 동적 타이핑이란 "타입 검사를 시간축 위에서 미루는 일"이며, 정적 타입과 동적 타입의 우열 논쟁은 이 시간축 위에서의 비용 분담 문제로 환원된다.

동적 언어는 타입을 잃은 것이 아니라, 타입을 항상 휴대하고 다닌다.

18장 혼합 타이핑 Hybrid Typing

정적은 안전하나 답답하고, 동적은 자유로우나 불안하다. 그렇다면 두 세계를 한 언어 안에 동거시키되 그 경계를 형식적으로 그어두면 어떨까? 이 장에서 다루는 혼합 타이핑은 바로 그 동거 계약서다.

이중 시민권

혼합 언어 HPCF에서는 정적으로 알려진 타입 τ와 만능 타입 dyn이 함께 산다. 이 둘 사이를 오가는 통로는 두 가지 변환자다. 하나는 정적 값을 동적 영역으로 띄우는 τ ⇒ dyn이고, 다른 하나는 동적 값을 정적 타입으로 끌어내리는 dyn ⇒ τ다. 후자는 본질적으로 불완전한 변환이다. 검사가 실패하면 실행은 정지한다.

형식

혼합 언어의 핵심 조작은 다음 두 형태다.

e ⇑ τ : dyn     e ⇓ τ : τ

위쪽 화살표는 안전한 주입이고, 아래쪽 화살표는 검사 동반 사영이다. 가령 τ = nat → nat일 때, 동적 영역에서 받은 값 e : dyn을 정적 함수로 쓰려면 e ⇓ (nat → nat)로 적어야 한다. 그러나 함수의 본문은 인자를 받기 전엔 검사할 수 없으므로, 실제로는 인자와 결과 양쪽에 대해 또 한 번씩 변환자가 끼어든다. 이른바 계약(contract) 또는 캐스트의 전파다.

점진적 타이핑이라는 풍경

이 형식은 점진적 타이핑(gradual typing)의 토대로도 익숙하다. 프로그램의 일부는 풍부하게 타입되어 있고, 다른 일부는 dyn으로 남아 있다. 두 영역의 접합점마다 캐스트가 자동으로 삽입되며, 정적 부분의 보장은 동적 부분에서 들어온 값이 캐스트 검사를 통과하는 한도 내에서 유지된다. 이것이 "점진적 보장"의 본질이다 — 정적 타입은 자신의 영역 내에서는 전통적 안전성을 누린다.

메타이론적 코멘트

혼합 언어의 정연함은 캐스트가 일등 시민이라는 점에서 비롯된다. 캐스트는 단순한 어댑터가 아니라 의미를 생성하는 행위자다. nat → nat으로의 캐스트와 nat → bool로의 캐스트는 같은 동적 함수 위에 다른 운명을 부여한다. 후자는 호출되는 순간이 아니라 결과를 돌려주는 순간 무너진다. 이 지연 검사가 혼합 시스템 메타이론의 묘미이며, 정적/동적의 이분법이 사실은 연속체임을 일깨운다.

캐스트는 변환이 아니라 약속이다. 어길 때 비로소 의미가 드러난다.

19장 직관주의 논리 Constructive Logic

"증명한다"와 "구성한다"가 한 단어가 되는 순간, 논리는 프로그래밍 언어가 된다. 직관주의 논리는 진리치가 아니라 증거에 무게를 두고, 증거는 항상 무언가를 만들어내는 절차여야 한다는 입장이다. 카리-하워드 대응이 자라나는 토양이 바로 여기다.

증거가 곧 항

고전 논리에서 A ∨ ¬A는 무료로 주어진다. 직관주의 논리에서는 그렇지 않다. A ∨ B의 증거를 가지려면 A의 증거를 제시하거나 B의 증거를 제시해야 하며, 어느 쪽인지를 명시해야 한다. 즉 분리는 합 타입이고, 두 가지 도입 규칙은 inl과 inr에 대응한다. 마찬가지로 함의 A ⊃ B는 함수 타입 A → B이며, 그 증거는 A의 증거를 받아 B의 증거를 돌려주는 절차다.

형식

직관주의 명제 논리의 도입·소거 규칙은 다음 짝으로 정리된다.

거짓 ⊥은 도입 규칙이 없는 명제이며, 그 소거 규칙은 어떤 결론이든 끌어내는 폭발률(ex falso)이다. ¬A는 A ⊃ ⊥의 약어로 정의된다. 즉 부정은 별도의 연결자가 아니라 함의의 특수형이다.

구성성의 의미

"구성적"이라는 형용사는 단순한 신중함이 아니다. 그것은 모든 존재 진술이 증인을 동반해야 한다는 강한 요구다. ∃x.P(x)를 증명한다는 것은 그러한 x를 실제로 만들어내는 알고리즘을 제시한다는 의미다. 이 관점에서 보면 직관주의 산술의 모든 정리는 자동으로 프로그램이며, 그 프로그램은 증명에서 직접 추출된다.

메타이론적 코멘트

증명의 정상화(normalization)는 프로그램의 평가에 정확히 대응한다. β-축약은 절단 제거(cut elimination)이며, 정상형은 직접 증명이다. 이 대응은 단순한 비유가 아니라 형식적 동치다 — 명제는 타입이고, 증명은 항이며, 증명의 단순화는 평가다. 그러므로 직관주의 논리를 공부하는 일은 곧 함수형 언어의 의미론을 공부하는 일이다.

고전논리가 "그렇다"를 말한다면, 직관주의 논리는 "어떻게 그러한지"를 보여달라고 요구한다.

20장 고전 논리 Classical Logic

배중률을 다시 가져오면 어떤 일이 벌어지는가? 놀랍게도 논리는 그대로 풍부해지지만, 대응되는 계산 모델은 함수가 아니라 제어(control)의 세계가 된다. 고전 논리는 곧 계속(continuation)의 논리다.

거리감

직관주의 논리에서는 도입과 소거가 좌우 대칭으로 균형 잡혀 있다. 고전 논리는 이 균형을 한쪽으로 기울인다. 이중 부정 제거 ¬¬A ⊃ A나 페어스 법칙 ((A ⊃ B) ⊃ A) ⊃ A는 직관주의에서는 증명되지 않으나 고전에서는 공리로 들어온다. 이러한 추가 원리들은 단순한 진리치 보충이 아니라, 계산적으로는 "지금까지의 맥락을 통째로 끌어다 쓰는 능력"으로 해석된다.

형식

고전 자연 연역은 다중 결론(multiple-conclusion) 시퀀트로 가장 자연스럽게 표현된다.

Γ ⊢ Δ

여기서 Γ는 가정의 다중집합, Δ는 결론의 다중집합이다. 직관주의에서 Δ는 한 개로 제한되었지만, 고전에서는 여럿이 허용된다. 이 사소해 보이는 변화가 배중률을 돌려준다 — ⊢ A, ¬A는 두 결론을 동시에 후보로 두는 시퀀트로 즉시 도출된다.

제어의 계산

카리-하워드 대응을 고전 논리로 끌어올리면 새로운 항이 등장한다. 그 대표가 callcc다. 페어스 법칙은 callcc의 타입이며, 이 항은 자신을 호출하는 시점의 계속을 포착해 변수에 묶는다. 즉 고전 증명은 계산적으로 백트래킹·예외·점프를 포함한 제어 흐름의 표현력을 갖는다. throw는 그렇게 묶어둔 계속에 값을 던져 흐름을 옮기는 행위다.

메타이론적 코멘트

고전 논리의 정상화는 직관주의에 비해 까다롭다. β-축약 외에 계속에 관한 축약 규칙이 추가되며, 한 항의 정상형이 유일하지 않을 수도 있다(컨플루언스의 약화). 그러나 이것은 결함이라기보다 본성이다. 프로그램이 평가 순서에 따라 다르게 부수효과를 일으키는 현실을, 고전 증명의 비결정성이 그대로 담아낸다. 결국 고전 논리는 더 강한 논리가 아니라, 다른 종류의 계산을 드러내는 논리다.

고전 논리가 "지금까지의 맥락"을 일급 객체로 다룬다면, 이는 사실 운영체제가 스택을 다루는 일과 닮아 있다.

21장 다형성 — System F Polymorphism (System F)

하나의 알고리즘이 여러 타입에서 작동해야 한다는 요구는 흔하다. 리스트의 길이를 재는 일에 원소의 종류는 무관하다. 이 무관함을 형식적으로 포착하는 장치가 타입에 대한 양화이며, 그 표준 무대가 시스템 F다.

두 단계의 추상

시스템 F는 항 추상 λx:τ.e 위에 타입 추상 Λα.e를 한 층 더 얹는다. 후자는 "어떤 타입 α가 들어오든 본문 e를 그 α로 인스턴스화해 쓸 수 있다"는 약속이다. 대응하는 타입은 보편 양화 ∀α.τ이며, 적용은 e[σ]로 적는다. 이 두 단계의 추상이 시스템 F의 표현력을 폭발시킨다.

형식

항등 함수의 다형 버전은 Λα.λx:α.x : ∀α.α → α이다. 이 한 항이 자연수 항등, 부울 항등, 함수 항등 모두로 인스턴스화된다.

표현력의 폭

시스템 F는 명시적 자료 구조 없이도 곱·합·자연수·리스트를 모두 정의한다. 가령 자연수 타입은 ∀α.(α → α) → α → α로 인코딩되며, 이는 직관적으로 "어떤 결과 타입에서든, 후속자 함수와 시작값이 주어지면 답을 만들어내는 절차"다. 이 인코딩은 처치의 유산을 타입 위로 끌어올린 것이다. 차이는 분명하다 — 타입 없는 인코딩이 동음이의로 흐릿했다면, 시스템 F의 인코딩은 타입이 의미를 고정한다.

메타이론적 코멘트

시스템 F는 강한 정상화 성질을 가진다 — 모든 잘 타입된 항은 정상형으로 환원된다. 그러나 이 정리의 증명은 더 이상 단순한 구조 귀납이 아니다. 타입 위의 양화가 자기 자신을 포함할 수 있기 때문이다(임프레디카티브 양화). 이 자기 참조의 위험을 다루는 표준 도구가 가환성 술어 또는 논리 관계 기법이다. 또 한 가지 — 시스템 F의 타입 추론은 결정 불가능하다. 따라서 실용 언어는 부분 다형성(예: 랭크-1 다형성)으로 절충한다.

"다형성"이라는 이름은 그리스어로 "여러 모양"이지만, 시스템 F에서는 "단 하나의 모양이 모든 타입을 견뎌낸다"는 뜻에 가깝다.

22장 추상 타입 — 존재 양화 Abstract Types (Existentials)

"이 모듈은 어떤 표현을 쓰는지 묻지 마라. 다만 약속된 인터페이스를 통해 쓰라." 이 모듈성의 격언이 형식 체계로 옮겨질 때, 우리는 존재 양화 ∃α.τ를 만난다. 보편 양화가 "임의의 타입에 대해"라면, 존재 양화는 "어떤 타입이 있어서"이다.

봉인과 개봉

존재 타입의 도입은 패키징(packing)이다. 구현 타입 ρ와 그 위의 구현체 e : [ρ/α]τ를 묶어 pack {ρ; e} as ∃α.τ를 만든다. 외부에서 보이는 것은 ∃α.τ뿐이며, 내부 표현 ρ는 봉인된다. 이 봉인을 풀어 쓰는 일이 개봉(unpacking)이다.

open e₁ as ⟨α, x⟩ in e₂

여기서 α는 새로운 타입 변수로, e₂의 본문 안에서만 통한다. 이 범위 제한이 추상의 핵심이다 — 누설이 일어나면 추상은 무너진다.

형식

σ가 α를 포함해서는 안 된다는 마지막 조건이 표현 누설(representation leakage)을 막는 빗장이다.

예시

스택의 추상 타입을 살펴보자. 인터페이스는 τ_stack ≡ {empty : α, push : nat × α → α, pop : α → (nat × α) opt}로 잡자. 한 구현은 리스트를 사용하고 다른 구현은 배열을 사용해도 좋다. 두 구현 모두 ∃α.τ_stack의 시민이며, 외부 코드는 어느 구현이 들어 있는지 알지 못한 채 동일한 함수 호출만으로 작업한다. 모듈 시스템의 시그니처 매칭은 본질적으로 이 패키징의 정교화다.

메타이론적 코멘트

존재 타입의 안전성은 표현 독립성(representation independence) 정리로 이어진다. 두 구현이 인터페이스 위에서 관찰적으로 동등하다면, 어느 쪽으로 바꿔 끼워도 클라이언트 코드의 의미는 변하지 않는다. 이 정리는 모듈 교체·리팩터링·최적화의 형식적 근거다. 실용 언어의 모듈은 이 위에 함자(functor), 정련(refinement), 봉인(sealing) 같은 장식을 얹지만, 뼈대는 모두 ∃α.τ다. 그러므로 다음 부에서 다룰 더 풍부한 모듈 체계는 결국 존재 양화의 후예들이라고 보아도 좋다.

보편 양화는 너그러움이고, 존재 양화는 비밀주의다. 좋은 라이브러리는 두 미덕을 모두 갖춘다.

23장 고차 종류 Higher Kinds

타입에도 타입이 필요하다. 정확히 말하면 — 타입을 분류하는 어떤 메타 단계의 표지가 필요한데, 우리는 이를 종류(kind)라 부른다. 단순한 타입과 종류의 구분에서 한 걸음 더 나가, 종류 자체가 →로 합성될 때 무슨 일이 벌어지는가.

왜 한 층으로는 부족한가

리스트 생성자 List는 그 자체로는 값을 담는 타입이 아니다. List nat나 List bool이 되어야 비로소 타입이 된다. 즉 List는 타입을 받아 타입을 돌려주는 함수다. 만약 우리에게 Type이라는 종류 하나밖에 없다면 List는 어디에도 분류되지 못한 채 표류한다. 이 곤란함이 고차 종류를 도입하는 동기다.

형식: λ를 메타 단계로

종류 문법을 κ ::= Type | κ₁ → κ₂로 확장하고, 생성자 단계에 람다·적용을 둔다.

Λα::κ. c  와  c₁ [c₂]

판단은 Δ ⊢ c :: κ로 적는다 (Δ는 종류 환경). 동치는 β/η에 의한 정규화로 정의되며, 종류 보존성과 신뢰성(soundness)을 보이는 길은 STLC와 거의 평행하다. 차이라면, 항(term) 단계의 타입 검사가 이제 생성자 동치를 호출한다는 점이다.

예시·메타이론

Pair :: Type → Type → Type, Map :: Type → Type → Type처럼 친숙한 다인수 생성자가 자연스럽게 자리잡는다. 더 나아가 Functor를 구체적인 생성자로 다루려면 (Type → Type) → Type 같은 종류가 필요하다. 메타이론적으로는 — 종류 단계가 강한 정규화를 가지므로, 생성자 동치가 결정 가능하고, 따라서 타입 검사 알고리즘이 종료한다. 이 점이 23장의 진짜 보상이다.

24장 부타입 관계 Subtyping

"이 자리에 저 값을 넣어도 되는가?" — 부타입 관계 τ <: σ는 그 질문에 답한다. 본질은 단순하다. τ의 값이 어디서나 σ의 값처럼 행세할 수 있다면 τ <: σ다.

포섭 규칙과 일관성

부타입을 시스템에 들이는 표준 통로는 포섭(subsumption)이다.

이 규칙이 들어오면 타입은 더 이상 유일하지 않다 — 한 항이 여러 타입을 가질 수 있다. 그래서 알고리즘적 타이핑은 "주어진 항의 최소 타입"을 추론하고, 필요한 자리에서만 부타입 점검을 호출하는 방식으로 재구성된다.

분산: 공·반·불변

합성 타입에서 부타입은 위치마다 다르게 흐른다. 곱 타입은 양쪽 모두 공변이다.

τ₁ <: σ₁   τ₂ <: σ₂ ⇒ τ₁ × τ₂ <: σ₁ × σ₂

함수 타입은 결과는 공변, 인자는 반변이다.

σ₁ <: τ₁   τ₂ <: σ₂ ⇒ τ₁ → τ₂ <: σ₁ → σ₂

가변 참조 셀은 양쪽이 모두 일치해야 하므로 불변(invariant)이다. 이 차이를 직관으로 말하면 — 받는 입장에서는 더 좁아도 되지만, 주는 입장에서는 더 넓어야 한다.

레코드와 폭/깊이

레코드 부타입은 두 축으로 갈라진다. 필드를 더 가지면 좁다 (폭 부타입), 같은 필드에서 각 타입이 좁으면 좁다 (깊이 부타입). 객체 지향 언어가 부타입을 사랑하는 이유가 여기 있다 — "더 많은 메서드를 가진 객체는 더 적게 요구하는 자리에 들어갈 수 있다"는 직관이 깔끔히 형식화된다. 메타이론에서는 일관성(coherence)을 챙겨야 한다. 같은 항을 같은 타입으로 유도하는 두 경로가 의미상 일치해야 한다는 요구다.

25장 싱글턴 종류 Singleton Kinds

종류 단계에 "이 생성자는 정확히 저 생성자와 같다"라는 사실을 새겨 넣을 수 있을까? 싱글턴 종류 S(c)는 바로 그 도구다. 모듈 시스템과 추상 타입의 정밀 제어가 여기서 시작된다.

정의: 단 하나의 거주자

종류 S(c :: Type)은 — c와 동치인 생성자만이 거주하는 종류다. 형식적으로는

Δ ⊢ c′ :: S(c) ⟺ Δ ⊢ c′ ≡ c :: Type

로 읽는다. 이 정의는 종류와 동치를 동시에 흔들기 때문에, 보통은 종류 부속(subkinding) S(c) <:: Type까지 함께 도입한다. 그러면 어떤 자리에서는 c를 좁게 보고("정확히 저 타입"), 다른 자리에서는 단지 일반 타입으로만 본다.

왜 좋은가: 투명·반투명 정의

모듈 M : sig type t = nat ... end를 생각하자. 외부에 t가 nat임을 노출하면 투명, 감추면 불투명, 일부만 알리면 반투명이다. 싱글턴 종류는 이 스펙트럼을 통일된 언어로 적게 해준다. 노출은 t :: S(nat), 은폐는 t :: Type, 그 사이 어딘가는 종속 종류와의 합성으로 표현한다.

메타이론의 함정

싱글턴은 동치 판단을 종류에 의존하게 만든다. 즉 c₁ ≡ c₂ :: κ를 결정하려면 κ를 들여다봐야 한다 — 함수 종류라면 외연성(extensionality)을, 싱글턴이라면 거주자가 강제되는 사실을 써야 한다. 정규형 알고리즘은 종류 주도 정규화(kind-directed normalization)로 진행되며, 결정 가능성·소거 가능성을 보장한다. 표면은 작아 보여도, 모듈 시스템 메타이론의 절반이 이 한 가지 종류 위에 서 있다.

26장 동적 디스패치 Dynamic Dispatch

"같은 메시지에 대해 객체마다 다르게 반응한다." — 객체 지향의 핵심 마법이지만, 사실은 매우 보수적인 형식 장치다. 디스패치를 떼어내 보면 결국 태그된 합 + 람다 테이블일 뿐이다.

객체란 무엇인가, 형식적으로

한 객체를 클래스 태그와 인스턴스 상태의 짝으로 본다. 메서드 호출은 두 단계로 일어난다. 첫째, 태그를 보고 적절한 메서드 본문을 골라낸다. 둘째, 그 본문을 인스턴스 상태에 적용한다. 메서드 모음을 클래스 벡터 cls : { c₁ ↦ m₁, ..., cₙ ↦ mₙ }로 두면, 호출 의미는

(c, s) ⇐ msg   ⇓   cls(c).msg(s)

로 깨끗이 적힌다. 즉, 디스패치는 분기일 뿐이다 — 하지만 분기 키가 컴파일 시점이 아닌 실행 시점의 객체에 박혀 있다는 점이 다르다.

클래스 분파 vs. 메서드 분파

같은 디스패치를 두 갈래로 조직할 수 있다. 클래스 우선은 클래스 본문 안에 메서드 케이스를 모은다(전형적인 OO 언어). 메서드 우선은 메서드 이름별로 모든 클래스 케이스를 한 곳에 모은다(다중 메서드의 출발점). 두 표현은 행렬의 행과 열처럼 서로의 전치(transpose)다. 어느 쪽이 더 "자연"한가는 — 어떤 차원으로 확장할 일이 잦은가에 달려 있다(표현 문제).

형식적 보상

이 시점에서 부타입은 자연히 등장한다. 메시지 집합이 더 많은 클래스 태그는 더 적게 요구하는 자리에 들어갈 수 있다 — 폭 부타입의 정확한 재현이다. 진보(progress)와 보존(preservation)은 표준 합 타입의 경우와 평행하게 증명된다. 마법은 사라지고, 형식만 남는다.

27장 상속 Inheritance

상속은 단지 코드 공유가 아니다. 자기 참조(self-reference)와 덮어쓰기(override)의 결합이며, 그래서 의외로 미묘한 고정점 의미론을 끌어들인다.

믹스인으로서의 클래스

상속을 깨끗이 다루려면 클래스와 객체를 분리해야 한다. 클래스는 — 슈퍼 클래스의 메서드 표를 받아 새 메서드 표를 돌려주는 함수다.

cls : (self → super) → (self → own)

여기서 self는 아직 결정되지 않은 "자기 자신"의 메서드 표를 가리키는 자리다. 객체 생성은 이 함수에 고정점을 취하는 일이다.

obj ≡ fix self. cls(self) ⊕ super(self)

self와 super의 분기

self는 항상 최종 객체를 가리킨다 — 그래서 서브클래스에서 덮어쓴 메서드도 슈퍼클래스가 호출했을 때 자동으로 새 버전이 불려나온다(이른바 open recursion). 반면 super는 덮어쓰기 직전의 표를 가리키므로, 자식에서 부모 구현을 명시적으로 호출할 수 있다. 이 두 자리의 분리가 상속의 의미를 결정한다.

형식과 위험

타입 측면에서 — 리스코프 치환 원리는 결국 부타입의 한 그림자다. 자식 클래스의 메서드는 부모 메서드의 자리에 들어가야 하므로, 인자에는 반변, 결과에는 공변이라는 같은 분산 규칙이 적용된다. 그러나 자기 참조 때문에 허약한 기반 클래스 문제(fragile base class)가 발생한다 — 부모를 살짝 바꿨을 뿐인데 자식이 깨진다. 메타이론은 이를 정직히 인정한다. 상속은 모듈성을 끊는다(breaks abstraction). 그래서 PFPL은 클래스를 모듈 위의 편의 표기로 격하시키고, 진짜 추상화는 시그너처가 담당하게 둔다.

28장 제어 스택 Control Stacks

평가 문맥(evaluation context)을 명시적인 자료 구조로 빼내면 — 그것이 곧 제어 스택이다. 이 단순한 변환이 예외, 연속, 코루틴 같은 모든 제어 효과의 출발점이 된다.

K-기계: 스택을 자료로

큰-단계 의미론은 평가 문맥을 메타 단계에 숨긴다. 작은-단계로 가도 평가 문맥은 여전히 메타 표기다. 제어 스택은 그 문맥을 항(term) 옆에 붙는 스택 프레임의 리스트로 객체화한다. 상태는 세 가지 모드를 오간다.

k ▷ e (평가 모드)   k ◁ v (반환 모드)   (종료)

예컨대 함수 적용 e₁(e₂)는 먼저 프레임 (□)(e₂)를 푸시하고 e₁로 진입한다. e₁이 값 v₁으로 반환되면 그 프레임이 v₁(□)로 갱신되고 e₂를 평가하기 시작한다. 모든 평가 규칙이 이런 식의 푸시·팝으로 적힌다.

왜 명시화하는가

스택이 데이터가 되면 — 우리는 그것을 조작할 수 있다. 잘라낼 수도, 복제할 수도, 어딘가에 저장해 두었다가 다시 불러올 수도 있다. 예외는 스택을 어떤 표지점까지 잘라낸다. 연속은 스택을 통째로 잡아채 값처럼 다룬다. 코루틴은 두 스택을 번갈아 활성화한다. 제어 효과의 동물원이 모두 같은 한 가지 자료 구조 위에서 살게 된다.

등가성과 보존

K-기계와 원래의 구조적 작은-단계 의미론 사이의 등가성은 — 형식적으로 흥미로운 정리다. 스택을 평가 문맥으로 풀어내는 함수 plug(k, e)를 정의하고, k ▷ e ↦ k′ ▷ e′이면 plug(k, e) ↦* plug(k′, e′)임을 보인다. 보존성과 진보는 세 모드 각각에 대해 따로 진술되며, 스택 자체에도 타입을 매겨 — 스택 타입 τ ⇒ σ이라는 새로운 분류 도구를 얻는다. 이 도구가 다음 장들의 기반이다.

29장 예외 Exceptions

정상 흐름이 어긋났을 때 우리는 호출 사슬의 임의의 지점까지 한 번에 빠져나가고 싶다. 예외는 — 제어 스택을 표지점까지 잘라내는 비국소 점프의 형식적 정수(精髓)다.

throw와 try의 의미론

두 가지 새 항이 들어온다. throw(e)와 try e₁ ow x. e₂(예외 발생 시 x로 결박된 값과 함께 핸들러로 분기). K-기계 위에서 의미는 깔끔하다.

k ▷ throw(v)   ↦   unwind(k, v)

여기서 unwind는 가장 가까운 try 프레임을 찾을 때까지 스택을 팝하고, 찾으면 핸들러로 진입하는 함수다. 만약 끝까지 핸들러가 없다면 — 프로그램은 비정상 종료한다.

타입과 효과

예외 값에는 타입이 있어야 한다. 단순한 길은 전역 예외 타입 exn을 두고 throw : exn → τ로 두는 것이다. throw의 결과 타입이 임의의 τ일 수 있는 이유는 — 정상적으로 반환하지 않기 때문에 어떤 결과 타입에도 일치한다고 칭할 수 있어서다(보존성에는 무해하다). 좀 더 정밀하게는 효과(effect) 시스템으로 어떤 함수가 어떤 예외를 던질 수 있는지를 타입에 새기지만, 그쪽은 표현력과 사용성의 균형 문제다.

메타이론과 위트

예외는 본질적으로 일방향이다. 한 번 빠져나가면 돌아올 수 없다. 이 비대칭이 — 다음 장의 연속과의 결정적 차이다. 보존성 증명은 unwind가 잘 정의되어 있고 핸들러의 결박 타입이 throw의 인자 타입과 일치함을 확인하는 일로 환원된다. 진보 명제는 "값이 아닌 항은 한 발 더 가거나, 처리되지 않은 예외를 던지거나" 둘 중 하나라는 살짝 확장된 형태로 진술된다. 예외가 있는 언어에서는 — "막다른 골목"도 정상적인 결과의 한 종류라는 사실을 메타이론이 인정해야 한다.

30장 연속 Continuations

"여기서 끝까지 가면 무슨 일이 일어날까?"라는 질문 자체를 값으로 만들 수 있다면 — 그 값이 연속이다. 28장의 제어 스택에 일급 시민권을 부여한 결과다.

letcc와 throw

두 연산이 핵심이다. letcc x in e는 현재 시점의 제어 스택을 잡아내 x에 결박한 뒤 e를 평가한다. throw v to k는 그 잡아둔 스택을 복원하고 거기에 v를 반환시킨다. K-기계 위에서

k ▷ letcc x in e   ↦   k ▷ [k/x]e

k ▷ throw v to k′   ↦   k′ ◁ v

두 번째 규칙을 보라 — 현재 스택 k를 그냥 버리고 k′로 갈아탄다. 시간을 거슬러 가는 것이 아니라, 평행 우주로 옮기는 것에 가깝다.

연속의 타입

연속은 "τ를 받는 자리"이므로, 스스로의 타입은 τ cont로 적는다. throw : τ × τ cont → σ가 어떤 σ로도 일치할 수 있는 이유는 예외와 같다 — 정상 반환하지 않기 때문이다. 연속의 진짜 위력은 표현력에 있다. 비국소 점프, 코루틴, 백트래킹, 비결정성, 발생기 — 이 모든 제어 패턴이 연속과 작은 상태(state)만으로 구현된다.

이중성과 위험

연속과 함수는 깊은 이중성을 이룬다. 함수는 결과를 생산하고, 연속은 결과를 소비한다. CPS(continuation-passing style) 변환은 이 이중성을 코드 차원에서 노출시킨다 — 모든 함수에 그 결과를 받을 연속을 명시적으로 넘기게 된다. 메타이론은 이 변환이 의미를 보존함을 증명한다. 그러나 일급 연속은 위험하다. 같은 연속을 두 번 호출하면 같은 시점으로 두 번 돌아간다 — 부수 효과가 있는 언어에서는 이 행동이 예측을 초과한다. 그래서 PFPL은 연속을 강력하지만 조심히 다뤄야 할 도구로 자리매김한다.

31장 심볼 Symbols

"그저 이름일 뿐인 이름"이 필요한 순간이 있다. 비교만 가능하고 내용은 없는 — 심볼은 언어가 새 이름을 동적으로 만들어내고 영원히 구분하게 해준다.

도입과 범위

새 심볼을 도입하는 연산을 new a:τ in e로 적는다. 이 식은 — 완전히 새로운 이름 a를 하나 만들어 그 사용 범위를 e로 한정한다. 표면적으로는 let과 비슷해 보이지만 본질이 다르다. a는 값이 결박된 변수가 아니라, 식별자 그 자체다. 형식 판단은 심볼 환경 Σ를 추가해

Γ ⊢_Σ e : τ

로 적고, new는 Σ를 확장하면서 본문을 평가한다.

심볼은 어떻게 사용되는가

심볼만으로는 거의 아무것도 못한다. 같은가 다른가만 물을 수 있을 뿐이다(a == b). 그런데 이 약함이 곧 유용함이다 — 심볼을 키로 삼아 다른 자료 구조에 결합할 수 있다. 다음 장의 유동 바인딩, 동적 분류된 데이터(dynamic classification), 가변 셀의 식별자, 클래스 태그까지 — 심볼이 비공식적으로 깔리지 않은 자리가 거의 없다.

새로움의 의미

"전적으로 새로운"이라는 말을 형식화하기 위해서는 — α-동치를 매우 진지하게 다루어야 한다. new a in e와 new b in [b/a]e는 동치이고(이름의 선택은 의미가 아니다), 동시에 한 평가 시퀀스 안에서 두 번 도입된 심볼은 결코 같지 않다(이름의 동일성은 의미다). 이 두 직관이 모순처럼 보이지만 형식적으로는 깔끔히 양립한다 — 심볼은 구문 안에서는 묶여 있고, 실행 중에는 풀려 외부 환경 Σ에 등록되기 때문이다. 진보·보존성은 평소대로지만, 이제는 Σ가 단조 증가한다는 점을 추가로 챙겨야 한다.

32장 유동 바인딩 Fluid Binding (Dynamic Scope)

정적 범위는 — 변수가 텍스트상의 결박에 묶인다. 유동 바인딩은 다르다. 변수의 값이 호출 시점의 동적 환경에 따라 결정된다. 강력하고, 위험하며, 그리고 여전히 진짜 쓸모가 있다.

fluid 변수와 binding 식

심볼 a:τ를 동적 변수로 쓰는 두 연산이 있다. get[a]는 현재 동적 환경에서 a의 값을 읽고, fluid a := v in e는 e가 평가되는 동안 a의 동적 결박을 v로 — 일시적으로 — 덮어쓴다. 종료되면 이전 결박이 복원된다. 본질적으로 — 동적 환경 μ : Σ ⇀ Val이 평가 상태에 함께 흐른다.

μ; e ↦ μ′; e′

왜 위험하고, 왜 유용한가

유동 바인딩은 추상화를 깬다 — 함수의 행동이 그 호출자가 어떤 fluid를 두르고 있었는지에 따라 달라진다. 같은 함수가 다른 자리에서 다르게 실행될 수 있다는 뜻이다. 이는 결박 등치(α-동치)가 동적 변수에는 적용되지 않음을 의미한다. 그러나 — 예외 핸들러, 출력 스트림, 트랜잭션 컨텍스트, 인쇄 정밀도, 실행 추적 같은 "주변 정보"를 함수 시그너처에 끼워 넣지 않고도 흐르게 할 수 있다. Lisp의 special variable, Haskell의 implicit parameter, 현대 언어의 scoped context가 모두 이 형식의 변종이다.

형식과 메타이론의 마지막 한 마디

유동 변수는 31장의 심볼 위에 자연히 얹힌다 — a는 새로 도입된 심볼이고, 동적 환경 μ는 그 심볼 키를 값으로 보내는 부분 함수다. 보존성은 μ가 항상 잘 타입된 값을 담고 있음을 유지한다. 진보 명제는 get[a]가 μ에 등록된 자리에서만 의미를 갖는다는 사전 조건을 요구한다. 그리고 가장 미묘한 정리 — 유동 바인딩은 일급 연속과 결합할 때 직관과 어긋난다. 잡아둔 연속을 다른 동적 환경에서 호출하면, 본문이 어느 환경을 보는지가 언어 설계 결정 사항이 된다. 여기서 PFPL의 메시지가 분명해진다. 형식은 자유를 보장해 주지만, 자유는 절제와 짝을 이룰 때만 의미를 가진다.

33장 동적 분류와 완전 비밀성 Dynamic Classification

합 타입 (sum type)은 컴파일 시점에 어떤 변형 (variant)들이 있을지를 미리 못박는다. 하지만 보안 토큰처럼 실행 중에 새로 생성되는 분류자가 필요하다면 어떻게 해야 할까. 이번 장의 주제는 동적으로 만들어지는 클래스, 그리고 그것이 자연스럽게 실현하는 완전 비밀성이다.

왜 정적 합 타입으로는 부족한가

32장에서 본 심볼 (symbol)은 이름의 정체성을 동적으로 다룰 수 있게 해주었다. 이 장에서는 한 걸음 더 나아간다. 분류된 값 (classified value)은 캡슐 안에 데이터를 넣고 봉인하는데, 이 봉인을 풀 수 있는 자는 같은 클래스 키를 쥔 자뿐이다. 키는 new a:τ in e 식으로 새 심볼 a를 만들어 그 스코프 e에서만 유효하게 한다. 정적 합 타입과의 결정적인 차이는, 클래스의 집합이 프로그램 실행 도중 자라난다는 점이다.

형식: clsfd τ와 두 연산

핵심 타입은 clsfd다. 이는 “어떤 클래스 키로 봉인된, 무언가의 값” 정도를 가리키며, 키 a를 알아야만 의미 있는 데이터를 꺼낼 수 있다. 두 가지 기본 연산이 있다.

a · e — 키 a로 e를 봉인 (intro),
match e {a · x ⇒ e₁ ; _ ⇒ e₂} — 키 a가 맞으면 x로 풀고, 아니면 대안 e₂를 실행 (elim).

타입 규칙은 직관 그대로다. a가 τ의 클래스 키라면:

완전 비밀성의 직관

비유하자면, a는 자물쇠를 여는 유일한 열쇠이고 clsfd 값은 그 자물쇠로 잠긴 상자이다. 키 a의 스코프 밖으로 상자가 새어 나가도, 외부 관찰자는 상자가 열린 상태와 닫힌 상태를 구별할 방법이 없다. 이는 패턴 매칭의 “와일드카드” 분기에서 동등한 항이 들어와도, 키를 모르는 한 항상 else 가지로 떨어진다는 사실에서 형식적으로 따라온다.

메타이론: 표현 독립성

이 비밀성은 단순한 인상이 아니라 이중 시뮬레이션 (logical relation)으로 증명되는 정리다. 동일한 키 아래 같은 인터페이스를 구현한 두 모듈은, 외부에서는 절대로 구별되지 않는다. 즉 데이터의 표현 (representation)을 키 안쪽에 가두면 표현 독립성이 자동으로 보장된다. 이로써 동적 분류는 추상 타입의 강력한 보안 버전을 제공한다 — “타입이 단지 시간이 흐르며 만들어진다”는 것이 곧 비밀이 된다.

34장 모더나이즈드 알골 Modernized Algol

알골 60은 명령형 언어의 시조이지만, 오늘의 기준으로 보면 타입 체계와 의미론이 어색하다. 모더나이즈드 알골 (Modernized Algol, MA)은 그 정신을 살리되, 함수형의 식 (expression)과 명령형의 명령 (command)을 또렷이 분리하여 둘 사이의 거래를 명시적으로 만든 작은 칼리브레이션이다.

두 세계의 분리: 식 vs. 명령

MA의 기본 모토는 이중층 구조 (stratification)다. 식은 Γ ⊢ e : τ 처럼 보통의 타입 판단을 받지만, 명령은 메모리 변화를 일으키는 행위이므로 별도의 판단 Γ ⊢ m ÷ τ를 둔다. 여기서 ÷는 “명령이 끝나면 τ형 결과를 돌려준다”는 약속이다. 식과 명령은 같은 책상 위에 놓이지만, 종이의 색은 다르다.

두 세계를 잇는 두 다리가 있다. 첫째, cmd m은 명령을 식으로 캡슐화하여 1급 시민으로 만든다. 둘째, do(e)는 식이 지정한 명령 캡슐을 풀어 실제로 실행한다. 이 구분 덕분에 “계산을 만드는 일”과 “계산을 일으키는 일”이 헷갈리지 않는다.

형식의 핵심 규칙

명령에는 ret(e) (식의 값을 돌려줌), bnd x ← m₁ ; m₂ (순차 실행과 결과 묶기) 같은 표준 구성이 있다. bnd는 모나드 결합 (bind)에 해당하지만, 여기서는 모나드라는 단어를 굳이 쓰지 않아도 형식이 자명하다.

예시: 카운터를 만드는 명령

가령 “1을 더하고 새 값을 돌려준다”는 명령 m은 bnd n ← get ; set(n+1) ; ret(n+1) 형태가 된다 (다음 장에서 정식으로 본다). 이 m을 cmd m으로 감싸면 함수에 인수로 넘기거나 자료 구조에 담을 수 있는 일급 명령이 된다. 함수가 그 캡슐을 받아 do(·)로 실행하기 전까지는, 부수 효과는 잠자고 있을 뿐이다.

메타이론: 효과의 격리

이 분리는 단순한 미관의 문제가 아니다. 식 부분만 보면 MA는 여전히 순수 함수형으로서, 베타 등치와 외연성을 유지한다. 효과는 명령으로 빠져나가 cmd 캡슐 안에 분리 보관되며, 식 단위의 등식 추론은 명령의 실행 순서에 영향받지 않는다. 다음 장에서 등장할 가변 참조는 이 무대 위에서 비로소 의미를 얻는다.

35장 참조 할당 Assignable References

메모리 셀 — 읽고 쓸 수 있는 작은 칸 — 은 명령형 언어의 호흡이다. MA에 참조 (reference)를 얹으면 비로소 알골스러운 흐름이 산다. 그러나 참조는 단순히 “주소를 가리키는 값”이 아니라 심볼로 이름 붙은 셀로 보는 것이 깔끔하다.

참조의 이중 본질

두 가지 관점이 가능하다. 하나는 심볼 참조로, 셀의 이름을 32장의 심볼처럼 다루는 방식이다. 다른 하나는 주소 참조로, τ ref라는 일급 타입의 값으로 셀을 다루는 방식이다. MA에서는 두 관점을 분리해 두는 편이 형식이 깨끗하다. 심볼 a는 그 자체로 “τ형 셀의 이름”이고, &a를 통해 τ ref 값으로 변환된다.

새 셀, 읽기, 쓰기

세 가지 명령이 핵심이다.

dcl a := e₀ in m — 새 셀 a를 e₀로 초기화하고 m 동안 사용,
get[a] — a의 현재 값 읽기,
set[a](e) — a의 값을 e로 갱신.

여기서 Σ는 현재까지 살아있는 셀들의 시그너처다. 동적 의미론은 메모리 (store) μ를 함께 운반하며, μ ‖ m 꼴의 상태 위에서 한 걸음씩 평가한다.

예시: 비밀스런 누산기

dcl a := 0 in cmd (bnd n ← get[a]; set[a](n+1); ret n)은 “호출할 때마다 0,1,2,…를 차례로 내놓는” 캡슐이 된다. 셀 a는 dcl의 스코프 안에서만 살아있고 외부에서는 보이지 않는다. 이는 33장의 동적 분류와 같은 정신이다 — 이름이 캡슐 안에서 태어나 그 안에서 살아간다.

메타이론: 안전성과 등식

형식 안정성의 진술은 메모리를 명시적으로 포함한다. μ : Σ (메모리가 시그너처와 정합)와 Σ ⊢ m ÷ τ가 함께 진행 (progress)·보존 (preservation)을 만족한다. 한편 셀이 끼어들면 식 단위의 외연 등식은 더 이상 자유롭지 못하다. 흥미롭게도, 셀의 사용 영역이 dcl로 국소화되어 있으면 외부 관찰자에게는 지역 상태가 등식적으로 사라진다 — 이것이 MA의 깔끔함이 보장하는 추상화의 보상이다.

36장 게으른 평가 Lazy Evaluation

엄격한 (strict) 평가는 인수를 먼저 갈아 넣고 함수를 호출한다. 게으른 (lazy) 평가는 정반대로, 결과가 정말 필요할 때까지 계산을 미룬다. 그러나 이 두 풍경은 단순한 평가 전략의 차이가 아니라, 타입에 새겨지는 의미론적 차이를 낳는다.

지연 (suspension)과 강제 (force)

핵심 타입은 τ susp — “언젠가 τ를 내놓겠다는 약속”이다. 두 연산이 짝을 이룬다.

susp(e) : τ susp — 식 e를 봉투에 넣어 보관,
force(e) : τ — 봉투를 뜯어 안의 값을 강제.

실용적으로는 메모이제이션이 따라붙는다. 한 번 강제된 지연은 결과를 캐시해 두 번째부터는 즉시 값을 돌려준다. 이는 형식적으로 메모리 셀로 모델링되며, 35장의 참조 위에 깔끔히 얹힌다.

by-name과 by-need 사이

두 가지 변종을 구별해야 한다. 호출-by-name은 매번 다시 평가하는 “원조 게으름”이고, 호출-by-need는 메모이제이션을 더한 “실용적 게으름”이다. 후자는 동일 표현이 몇 번 평가되는지가 더 이상 관찰 가능하지 않다는 점에서 등식 추론에 친화적이다 — 단, 효과가 없을 때만 그렇다.

예시: 무한 자료의 유한한 사용

자연수의 무한 스트림 nats = 0 :: map (+1) nats를 정의해도, take 5 nats만 강제하면 앞쪽 다섯 칸만 계산된다. 이것이 게으름의 매력이다. 데이터의 모양은 무한대지만, 실제 일은 “보는 만큼”만 한다. 한편 length nats를 강제하면 평가는 영원히 끝나지 않는다 — 약속이 거짓말이 되는 것이 아니라, 약속을 지키는 데에 시간이 무한히 들 뿐이다.

메타이론: 종료성과 효과의 위험

게으름의 안전 정리는 “필요할 때만 진행”이라는 수정된 진행 명제로 진술된다. 그러나 효과가 있는 식을 susp로 가두면 언제 효과가 일어나는가가 관찰 시점에 좌우되어, 추론이 까다로워진다. PFPL의 입장은 분명하다. 게으름은 강력하지만, 부수 효과와 결합할 때는 비용이 따른다. 다음 장의 양극화는 이 긴장을 타입 차원에서 정리하는 한 가지 방법이다.

37장 양극화 Polarization

왜 어떤 타입은 “값으로 충분”하고 어떤 타입은 “계산으로만 의미가 있는가”? 양극화 (polarization)는 이 질문을 정면으로 다룬다. 타입을 양극 (positive, +)과 음극 (negative, −)으로 갈라, 데이터와 행위 사이의 평형을 형식 위에 새기는 작업이다.

두 극의 직관

양극 타입은 구성된 값이 곧 의미인 타입이다. 합 타입 τ₁ + τ₂, 곱의 양극형 τ₁ ⊗ τ₂, 자연수, 부울값 — 이런 타입의 값은 “이미 다 만들어져 있다”. 음극 타입은 요청에 응답하는 행위가 의미인 타입이다. 함수 τ₁ → τ₂, 음극 곱 τ₁ & τ₂ — 이들은 “무엇을 묻느냐에 따라 답이 나오는” 인터페이스다. 양극은 데이터, 음극은 코데이터 (codata)다.

형식: 양극과 음극의 행렬

각 극에는 자체적인 형성 규칙과 도입·제거 규칙이 있다. 양극 도입은 “값 만들기”, 양극 제거는 “패턴 분기”. 음극 도입은 “관찰에 답하는 추상”, 음극 제거는 “관찰을 적용하기”다. 두 극을 연결하려면 다리가 필요하다.

↓τ⁻는 음극 타입을 양극으로 “얼리는” 지연 (thunk),
↑τ⁺는 양극 값을 음극 행위로 “녹이는” 강제 (force).

이 두 시프트 연산자는 36장의 susp/force의 순수 추상이다. 게으른 평가는 사실상 ↓가 풍부한 언어를, 엄격한 평가는 ↑ 쪽이 자연스러운 언어를 선호한다.

예시: 페어를 두 가지로 보기

곱의 양극형 A ⊗ B의 값은 짝 (a, b)이고 제거는 패턴 매칭이다 — 두 부분이 모두 미리 만들어진다. 음극형 A & B의 “값”은 “왼쪽을 묻거나 오른쪽을 묻는다”는 두 관찰에 대한 응답이며, 묻지 않은 쪽은 평가될 필요가 없다. 같은 “페어”라는 일상어 뒤에 두 개의 형식론이 숨어 있던 셈이다.

메타이론: 평가 전략의 자유

양극화의 보상은 평가 전략의 명료성이다. 양극 값은 어디서 평가되든 같은 답을 주는 강한 정규형을 가지며, 음극 값은 관찰에 의해서만 진행된다. 결과적으로 호출-by-value와 호출-by-name은 같은 언어 안에 평화롭게 공존한다. 이는 컴파일러가 일관된 호출 규약을 결정하는 데에도, 의미론자가 등식 이론을 깔끔히 진술하는 데에도 큰 이득이다.

38장 중첩 병렬성 Nested Parallelism

스레드, 락, 데드락 — 동시성의 어두운 단어들. 그러나 본질적인 병렬성은 훨씬 단정하다. 두 식이 서로의 결과에 의존하지 않는다면, 동시에 평가해도 안전하다. 중첩 병렬성 (nested parallelism)은 이 단순한 통찰을 형식의 1급 시민으로 격상시킨다.

병렬 짝과 병렬 묶음

핵심 구성은 병렬 let이다.

par x ← e₁ ‖ y ← e₂ in e

이는 e₁과 e₂를 병렬로 평가하고, 둘 다 끝났을 때 그 결과를 x, y로 묶어 e를 진행한다. ‖는 “두 가지 일이 서로 모르는 채로 일어난다”는 약속이다. 분기는 다시 자신 안에서 또 분기할 수 있다 — 그래서 중첩이다. 결국 평가의 모양은 트리가 된다.

두 가지 비용 모형

중첩 병렬성의 멋진 점은 두 가지 비용을 동시에 측정한다는 것이다. 일 (work) W은 모든 단계의 총합 — 직렬 비용이다. 경로 (depth, span) D는 가장 긴 의존 사슬의 길이 — 무한 코어로 줄일 수 있는 한계이다. 병렬 짝의 D는 max(D(e₁), D(e₂)) + D(e)가 되어 두 가지 일의 길이가 합이 아니라 큰 쪽으로 잡힌다.

예시: 병렬 합산

리스트 합산을 둘로 쪼개 분할 정복하면 W는 여전히 선형이지만 D는 로그가 된다. 즉 n 코어를 충분히 줄 수 있다면 O(log n) 시간에 끝난다. 중요한 점은 코드가 변하지 않는다는 것 — par로 묶기만 하면 된다. 이 우아함이 중첩 병렬성의 마케팅 카피다.

메타이론: 결정성의 보존

병렬 평가가 직렬 평가와 같은 답을 줄 것인가? 식 부분이 순수하다면 그렇다. 병렬 의미론은 합류성 (confluence)을 만족하며, 어떤 스케줄로 코어에 일을 배분하더라도 결과는 동일하다. 효과를 도입하면 이 보증은 깨지지만, 적어도 순수 핵심에서는 “병렬은 빠를 뿐 다르지 않다”는 정리가 성립한다. 이것이 함수형 병렬화의 정신적 지주다.

39장 퓨처와 사변 실행 Futures and Speculations

중첩 병렬성이 “결과가 모두 필요하다”는 가정에 서 있다면, 퓨처 (future)와 사변 실행 (speculation)은 “필요할지도 모른다”의 세계로 한 걸음 들어선다. 미리 시작해 두고, 결과를 받아쓸 때 동기화하거나, 끝내 쓰지 않을 수도 있다.

퓨처: 비동기적 약속

퓨처는 “지금 평가를 시작했지만 값은 나중에”라는 약속이다. 두 연산이 짝을 이룬다.

fut(e) : τ fut — e의 평가를 별도 스레드에서 시작,
syn(e) : τ — 퓨처가 끝나길 기다려 값을 회수.

외형은 36장의 지연 (suspension)과 닮았지만 의미는 정반대다. 지연은 필요할 때까지 미루고, 퓨처는 가능할 때까지 앞당긴다. 컴파일러나 실행 시스템은 가용 코어가 있는 한 퓨처에 일을 분배한다.

사변 실행: 쓸지 모르는 일을 미리

사변 (speculation)은 한 발 더 나아간다. 결과가 쓰일지 미리 알 수 없는 식을 그래도 시작해 두고, 진짜로 필요해지면 결과를 회수하고, 아니면 조용히 폐기한다. 형식적으로는 “쓰지 않으면 효과도 없는 것처럼”을 보장하기 위해, 사변할 식은 순수 (pure) 핵심에 한정하는 것이 안전하다. 이는 양극화의 음극 행위와 결이 같다 — 관찰될 때만 의미를 갖는다.

예시: 분기 예측의 메아리

if cond then syn(fut e₁) else syn(fut e₂)라고 쓰면, cond를 평가하는 동안 e₁과 e₂를 모두 시작해 둘 수 있다. 사용된 가지의 결과만 회수되고 다른 쪽은 버려진다. 하드웨어의 분기 예측이 형식 언어로 올라온 모양새다. 이득은 지연 시간 단축, 비용은 잠재적인 일의 증가 — 우리가 38장에서 본 W와 D의 거래가 더 미묘해진다.

메타이론: 결정성과 자원성

퓨처와 사변이 추가되어도 순수 식의 결과는 결정적 (deterministic)이다. 즉 의미론적 정답은 동일하고, 비용만 달라진다. 안전성 정리는 “시작된 모든 퓨처는 동기화 시점에 형식이 보존된다”로 진술된다. 이것이 함수형 언어가 사변을 자연스럽게 환영할 수 있는 이유다 — 잘못 추측해도 답이 틀리지는 않는다. 손해는 오직 시간과 전력일 뿐, 진실 자체는 흔들리지 않는다.

40장 프로세스 계산 Process Calculus

계산이 더 이상 함수 한 줄의 결과가 아니라, 동시에 살아 움직이는 여러 행위자의 합주가 될 때 무엇이 변하는가. 프로세스 계산은 그 합주의 악보를 적기 위한 가장 작은 문법이다.

왜 새 추상이 필요한가

람다 항이 묻는 질문은 "이 식의 값은 무엇인가"였다. 그러나 두 모듈이 동시에 돌고, 서로 신호를 주고받으며, 완료가 아닌 지속이 정상 상태인 시스템에서는 질문이 바뀐다. "이 시스템이 어떤 상호작용 패턴을 보이는가." 값 대신 행동(behavior)이 일등 시민이 되어야 한다. 프로세스 계산은 이를 위해 항을 버리고 프로세스 P, Q를 도입한다.

형식: 작용과 합성

가장 단출한 어휘는 다음과 같다. 정지 프로세스 0, 액션 접두 a.P (먼저 a를 수행한 뒤 P로 진행), 병렬 합성 P ‖ Q, 비결정 선택 P + Q, 그리고 채널 이름 은닉 ν a. P. 액션 a는 송신 c⟨v⟩이거나 수신 c(x)이다. 동기 통신 규칙은 짝이 맞아 떨어졌을 때만 협주가 일어난다는 사실을 표현한다.

P —c⟨v⟩→ P′ Q —c(x)→ Q′P ‖ Q —τ→ P′ ‖ Q′[v/x]

여기서 τ는 외부에 보이지 않는 내부 동기이다. 외부 관찰자는 두 프로세스가 무언가 했다는 사실만 알고, 무엇을 주고받았는지는 모른다.

직관: 두 잔의 커피

카페 C = order(x). brew⟨x⟩. 0과 손님 K = order⟨"라떼"⟩. 0을 C ‖ K로 합성하면 τ 한 번 뒤 brew⟨"라떼"⟩. 0이 남는다. 같은 카페에 두 손님이 동시에 줄을 서면 비결정성이 끼어든다. 누가 먼저 주문하느냐는 +가 아닌 스케줄링이 결정한다.

메타이론: 행동 동치

두 프로세스가 "같다"는 것은 무엇인가. 구문 동치는 너무 강하고, 종료 결과 비교는 종료가 없는 세계에서 의미가 없다. 답은 이중모의(bisimulation)이다. P ≈ Q는 P가 어떤 액션 a로 P′이 되면 Q도 같은 a로 Q′이 되며 P′ ≈ Q′이고, 그 역도 성립함을 뜻한다. 즉 두 프로세스는 외부 관찰자에게 구별 불가능하다. 이중모의는 합동 관계이며 동시성 정리들의 추론 도구가 된다.

41장 동시성 알골 (CA) Concurrent Algol

순수한 프로세스 계산은 너무 헐벗었다. 우리는 함수도, 데이터 타입도, 가변 셀도 함께 쓰고 싶다. 동시성 알골은 명령형 알골 위에 채널과 병렬을 얹어 만든 하이브리드다.

설계 동기

실용 언어에서 동시성은 별개의 세계가 아니라 기존 표현식 안에 끼어든다. spawn(e)으로 새 프로세스를 띄우고, send·recv로 채널을 다루며, 그 모든 연산이 부수효과로 표현식의 평가에 섞여 든다. CA는 이를 위해 커맨드(command)라는 별도의 부호화를 두고, 표현식과 분리하지 않으면서도 효과의 자취를 타입에 새긴다.

형식: 커맨드와 시그널

타입 τ cmd는 "값을 돌려주는 동시성 작업"을 가리킨다. 핵심 구성자는 다음이다.

ret(e) : τ cmd, bnd(x.m₁; m₂) : τ cmd, spawn(m) : 1 cmd, send[c](e) : 1 cmd, recv[c] : τ cmd

채널 c : τ chan은 정적 선언으로 도입된다. 동기 의미론에서 send와 recv는 짝을 만나야 진행한다. 비동기 변형은 채널을 큐로 이해해 송신자를 차단하지 않는다. 두 의미론은 모두 작은 단계 전이로 정의되며, 전이의 라벨은 채널 액션을 외부에 노출시킬지 여부에 따라 달라진다.

직관: 워커 풀

요청 채널 req : task chan과 응답 채널 res : result chan이 있다고 하자. 워커는 본질적으로 μ. recv[req] ≫= λt. ret(do(t)) ≫= λr. send[res](r) ≫ μ의 무한 반복이다. 디스패처는 spawn(worker) ‖ spawn(worker) ‖ …로 풀을 만든다. CA의 매력은 이 모든 것을 타입이 잡힌 표현식으로 쓸 수 있다는 데 있다.

메타이론: 타입 안전과 진행

CA의 안전성 정리는 두 부분이다. 보존(preservation)은 어떤 전이가 일어나도 잘 타입된 프로세스 형상은 잘 타입된 형상을 낳는다는 것이다. 진행(progress)은 단일 스레드와 다르다. "막힌 채로 막혀 있는" 교착이 정상일 수 있다. 따라서 정리의 형태는 "잘 타입된 닫힌 시스템은 값으로 환원되거나, 외부 액션을 기다리는 형태이거나, 내부 τ로 한 걸음 갈 수 있다"가 된다. 즉 CA는 동시성을 합법화하면서도, 타입이 보장하는 안전 그물은 그대로 유지한다.

42장 분산 알골 (DA) Distributed Algol

동시성은 같은 메모리 공간을 공유하는 여러 활동에 관한 것이지만, 분산은 다른 가정 위에 선다. 노드는 떨어져 있고, 통신은 비싸며, 어떤 자원은 그 노드를 떠날 수 없다. 타입은 그 사실을 안다.

위치라는 일등 개념

DA의 출발점은 위치(site) w이다. 모든 표현식은 어떤 노드에서 실행되며, 어떤 값은 그 노드에 고정된다. 타입 τ@w는 "노드 w에 살고 있는 τ형 값"을 뜻한다. 함수 호출이 노드를 넘어가면 의미는 더 이상 단순한 베타 환원이 아니라 이주(migration) 또는 원격 호출이 된다.

이동 가능성

핵심 구분은 어떤 값이 노드를 옮길 수 있는가이다. 정수는 어디든 갈 수 있다. 그러나 파일 핸들이나 잠긴 셀은 옮길 수 없다. DA는 이를 위해 이동 가능 타입(mobile type) 술어 τ mobile을 두고, 송신·수신은 이동 가능한 값에 한해서만 허용된다. 이동성은 구문이 아니라 의미적 보장이며, 타입 시스템이 그것을 정적으로 강제한다.

Γ ⊢ e : τ@w τ mobile Γ ⊢ w′ : siteΓ ⊢ at[w′](e) : τ@w′

직관: 데이터 가까이로

데이터베이스가 db 노드에 있고, 로그 디스플레이가 ui 노드에 있다고 하자. db에서 무거운 질의를 돌려 요약된 결과만 ui로 보내는 패턴은 at[ui](recv(c))와 at[db](send(c, summarize(query())))로 표현된다. 핵심은 무거운 데이터가 채널을 넘지 않는다는 사실이며, 타입이 그것을 보증한다. 분산 시스템의 정설 "코드를 데이터에 보내라"가 타입 규칙으로 새겨진다.

메타이론: 위치 보존과 단절

DA의 안전성은 보존·진행 외에 위치 보존이 추가된다. τ@w로 타입된 값은 평가 후에도 정말로 w에 머문다. 부분 실패도 모형의 일부다. w 노드가 사라지면 at[w](e)는 정상 종료될 수 없으며, 이는 예외 또는 영구 차단으로 처리된다. 분산 알골이 가르치는 교훈은 단순하다. 위치는 부주의한 메타데이터가 아니라 타입의 일부여야 하며, 그래야만 시스템이 거짓말하지 않는다.

43장 모듈성과 링킹 Modularity and Linking

큰 프로그램은 작은 프로그램들의 그저 합이 아니다. 부품들 사이의 약속을 어떻게 정의하고, 어떻게 따로 만들고, 어떻게 함께 묶는가가 본질이다. 모듈은 약속의 단위이고, 링킹은 약속의 검증이다.

분리 컴파일의 두 얼굴

모듈을 따로 컴파일한다는 말은 두 가지를 동시에 의미한다. 첫째, 한 모듈을 작성·검사할 때 다른 모듈의 구현을 알 필요가 없다. 둘째, 합쳐진 결과는 모든 약속이 일관할 때만 정상 동작한다. 모듈 시스템은 이 두 가지를 형식화하기 위해 시그니처(signature)와 스트럭처(structure)의 구분을 도입한다. 시그니처는 약속, 스트럭처는 이행이다.

형식: 시그니처와 봉인

시그니처 σ는 일종의 인터페이스 타입이며, 스트럭처 M : σ는 그 인터페이스를 구현하는 항이다. 핵심 연산은 봉인(sealing)이다.

M ▷ σ ≡ "M을 σ로 가린다"

봉인 후에는 σ가 노출하지 않은 정의는 외부에서 볼 수 없다. 추상 타입은 시그니처에 type t로만 선언되고 스트럭처가 그것을 어떤 구체 타입으로 정의했는지는 봉인 너머로 새지 않는다. 이로써 표현 독립성이 정적으로 보장된다.

직관: 두 가지 자료구조

스택을 list로 구현한 StackL과 배열로 구현한 StackA가 있다고 하자. 둘 다 시그니처 STACK = sig type t; val empty : t; val push : … end로 봉인하면, 사용자는 t의 모양을 알 수 없고 두 구현은 치환 가능해진다. 링킹이란 사용 측의 빈자리에 어떤 봉인된 구현을 끼울지 결정하는 행위이며, 검사는 시그니처 매칭으로 환원된다.

메타이론: 합성성과 정합

모듈 시스템의 메타이론은 두 가지를 증명한다. 합성성: 각 모듈이 자기 시그니처를 만족하면, 링킹된 결과도 전체 시그니처를 만족한다. 정합성: 시그니처 매칭은 결정 가능하며, 추상 타입은 봉인 이후 외부의 어떤 항으로도 식별되지 않는다. 후자가 깨지면 모듈성은 이름뿐이다. 이후 장들은 이 정합성을 떠받칠 종류 시스템과 추상 메커니즘을 차곡차곡 쌓는다.

44장 싱글턴 종류와 서브카인딩 Singleton Kinds and Subkinding

모듈을 다루다 보면 "이 추상 타입은 사실 저 타입과 똑같다"라고 잠깐 인정해야 할 때가 온다. 싱글턴 종류는 그 잠깐의 진실을 종류 수준에서 정확하게 새기기 위한 도구다.

왜 종류에 동등성이 새겨야 하는가

모듈 시그니처가 type t를 추상으로 선언했다고 해도, 어떤 클라이언트는 M.t가 구체적으로 int임을 알면서 사용해야 할 수 있다. 봉인은 강한 추상이고, 투명한 어센션(transparent ascription)은 약한 추상이다. 둘을 통일된 틀에서 다루기 위해, 종류 시스템에 "이 종류는 단 하나의 타입만 포함한다"라는 진술을 더한다. 이것이 싱글턴 종류 S(τ)이다.

형식: S(τ)와 서브카인딩

S(τ)는 τ와 동일한 모든 타입을 원소로 가지는 종류이다. 즉 τ′ : S(τ)는 본질적으로 τ′ ≡ τ를 의미한다. 서브카인딩 κ₁ <: κ₂는 종류 사이의 포함 관계이다.

S(τ) <: T (싱글턴은 일반 타입 종류의 부분이다)

서브카인딩이 있는 까닭에 "정의가 노출된 타입"은 자연스럽게 "추상 타입"의 자리에 들어갈 수 있다. 반대 방향은 허락되지 않는다. 추상은 구체보다 일반적이다.

직관: 동등성을 가르쳐 주기

스트럭처 M = struct type t = int; … end를 시그니처 sig type t : S(int); … end로 어센드하면, 외부에서 M.t는 int와 동일하게 다뤄진다. 같은 스트럭처를 sig type t; … end로 봉인하면 M.t는 새 추상 타입이 된다. 같은 구현, 다른 시그니처, 다른 동등성. 싱글턴 종류는 이 차이를 종류 수준에서 일관되게 표현한다.

메타이론: 정합성과 결정성

싱글턴이 들어오면 종류 동등성은 더 이상 구문 비교만으로 결정되지 않는다. η-확장과 싱글턴 단순화를 함께 다뤄야 한다. 핵심 결과는 결정 가능 동등성: 모든 잘 형성된 종류 판단은 알고리즘적으로 비교될 수 있다는 것이다. 이는 모듈 시스템의 타입 검사가 끝나는 검사가 되도록 보장한다. 싱글턴 종류는 표현력과 검사가능성 사이에서 외줄을 타는 우아한 균형이다.

45장 타입 추상화와 타입 클래스 Type Abstractions and Type Classes

"같은 인터페이스를 만족하는 여러 타입"을 다루는 두 전통이 있다. 모듈은 인터페이스를 명시적으로 끼워 넣고, 타입 클래스는 인터페이스를 암묵적으로 추론한다. 둘 다 표현력 있는 추상의 길이며, 한 뿌리에서 갈라진다.

두 갈래의 추상

타입 추상화의 가장 근본적인 형태는 존재 타입 ∃α. τ이다. "어떤 타입 α가 있어 그것이 τ를 만족한다." 모듈은 이 존재 타입을 이름이 있는 패킷으로 사용자가 직접 다루도록 한다. 타입 클래스는 같은 존재성을 컴파일러의 어깨 위에 얹는다. 사용자는 그저 "Eq α ⇒ α → α → bool"이라 적고, 어떤 사전(dictionary)이 들어갈지는 컴파일러가 찾아낸다.

형식: 사전 전달과 제약

타입 클래스 선언 class Eq α { eq : α → α → bool }는 본질적으로 사전 타입 Eq α = { eq : α → α → bool }이다. 인스턴스 선언 instance Eq int { eq = … }는 그 사전의 값을 제공한다. 다형 함수의 시그니처 (Eq α) ⇒ α → α → bool은 함수 화살표 앞에 사전 인자를 끼워 넣는 것과 같다.

(Eq α) ⇒ α → α → bool ↦ Eq α → α → bool

해법(resolution)은 컴파일러가 호출 지점의 α를 보고 적합한 인스턴스 사전을 자동으로 채워 주는 과정이다.

직관: 같은 노래 두 가락

모나드 Monad m은 모듈로 쓰면 functor Monad(M : MONAD)가 되고, 타입 클래스로 쓰면 do 구문 뒤에 숨는다. 전자는 명시성과 일대다 인스턴스화를 허락하고, 후자는 간결함과 자동성을 준다. 어느 쪽이 우월한가는 잘못된 질문이다. 일관성(coherence) — 같은 타입에 대해 항상 같은 사전이 선택되는가 — 가 타입 클래스의 원죄이며, 모듈은 사용자에게 그 부담을 떠넘긴다.

메타이론: 일관성과 번역

타입 클래스의 메타이론은 전역 일관성을 핵심 정리로 둔다. 인스턴스 사전은 단 하나로 결정되어야 하며, 이는 인스턴스 중복을 막는 정적 규칙으로 보장된다. 또 하나의 결과는 번역(translation): 모든 타입 클래스 프로그램은 명시적 사전 전달 형태로 번역 가능하며, 두 형태는 등식적으로 동치이다. 즉 마법은 없다. 모든 암묵성은 컴파일 시점에 명시성으로 풀려 나간다.

46장 계층과 매개변수화 Hierarchy and Parameterization

모듈은 단지 큰 레코드가 아니다. 모듈이 모듈을 받아 모듈을 돌려주는 함수, 즉 functor가 있어야 비로소 모듈러리티가 합성성으로 자란다.

왜 functor인가

"순서가 있는 집합 위에 정렬을 구현하라." 이 한 줄은 매개변수화이다. 임의의 ORD 시그니처를 받아 SORT 시그니처를 반환하는 모듈 수준 함수 Sort(O : ORD) : SORT가 functor이다. functor는 약속 위에 약속을 쌓는다. 클라이언트는 어떤 ORD 인스턴스든 끼워 넣을 수 있고, 결과의 안전성은 functor의 시그니처가 보증한다.

형식: 의존 함수 종류

functor 타입은 보통의 함수 타입과 다르다. 결과의 시그니처가 인자에 의존할 수 있기 때문이다. 이를 위해 종속 곱(dependent product) Π(X : σ₁). σ₂이 도입된다.

Sort : Π(O : ORD). SORT(O.t)

여기서 SORT(O.t)의 t는 인자 모듈 O의 타입 컴포넌트이다. 결과 시그니처가 인자의 타입을 참조한다. 이 의존성이야말로 functor가 단순한 일등 시민 함수와 구별되는 지점이다.

직관: 적용성 vs. 생성성

같은 인자로 functor를 두 번 적용했을 때 결과의 추상 타입이 같은가, 다른가? 적용성(applicative) functor는 같다고 답하고, 생성성(generative)은 다르다고 답한다. 적용성은 추론과 등식 추론이 매끄럽지만, 부수효과가 끼어 있을 때 의미가 흐려진다. 생성성은 매번 새 추상을 만들어 안전하지만, 같은 결과를 두 번 만드는 비용을 부른다. 실제 시스템은 둘을 섞어 쓴다. 순수 functor는 적용성, 효과를 가진 functor는 생성성으로.

메타이론: 계층의 안정성

functor의 합성, 즉 F ∘ G는 의존 시그니처를 정확히 따라가야 한다. 핵심 정리는 인장(seal) 보존: functor 본문에서 봉인한 추상 타입은 결과 모듈에서도 봉인되어 외부에 새지 않는다. 또한 매개변수성의 모듈 버전이 자연스럽게 따라온다. functor는 인자의 추상 타입에 대해 균일하게 동작해야 하며, 그 균일성이 모듈 계층 전체의 안전을 떠받친다. 작은 약속들의 덧셈이 큰 신뢰가 되는 곳, 그곳이 functor의 자리다.

47장 T에 대한 등식 추론 Equational Reasoning for T

언어 T는 자연수와 함수, 그리고 원시 재귀만 가진 단정한 세계이다. 모든 프로그램이 종료한다는 사실 하나로 등식 추론은 거의 자명해 보인다. 그러나 "거의"가 그 무게의 전부다.

등식이 의미하는 것

두 항 e₁과 e₂가 같다는 말은 무엇인가. 가장 단순한 답은 관찰적 동치(observational equivalence): 어떤 프로그램 문맥 C[·]에 넣어도 같은 자연수로 평가된다. 이것이 정의로는 좋지만 증명에는 끔찍하다. 모든 문맥을 양화해야 하기 때문이다. 등식 추론의 임무는 이 정의와 실제로 다룰 수 있는 판정 시스템을 잇는 것이다.

형식: 판단 Γ ⊢ e₁ ≡ e₂ : τ

등식 판단은 베타·에타 규칙, 합동성, 그리고 원시 재귀의 풀어 쓰기 규칙으로 구성된다.

(λx.e)(e′) ≡ e[e′/x], λx. f x ≡ f (단 x ∉ FV(f)), rec(z; x.y.s; 0) ≡ z, rec(z; x.y.s; succ(n)) ≡ s[n, rec(…)/x, y]

이 규칙들은 평가 단계와 일치하지 않는 더 일반적인 등식까지 포함한다. 예컨대 λx. e의 본문이 닫혀 있다면 두 개의 다른 본문이 외연적으로 같은 함수일 수 있다.

직관: 외연성의 무게

add(0, m)과 add(m, 0)은 구문상 다르고, 한 단계 평가에서도 다르다. 그러나 모든 자연수 m에 대해 같은 결과를 낸다. T의 등식 추론은 이 사실을 외연성 원칙으로 인정한다. 함수에 대해서는 에타·베타로, 자연수에 대해서는 원시 재귀의 풀이로. 모든 프로그램이 종료하기에 외연성은 위험하지 않다. 무한 루프라는 함정이 없는 평지에서 수학은 본래 모습을 유지한다.

메타이론: 건전성과 완전성

핵심 정리는 두 가지다. 건전성: Γ ⊢ e₁ ≡ e₂ : τ이면 e₁과 e₂는 관찰적으로 동치이다. 완전성(부분적): 닫힌 자연수 항에 대해서는 평가 결과가 같으면 등식이 도출된다. 함수 항에 대해서는 외연성 덕에 모든 인자에서 같다는 사실이 등식의 도출로 이어진다. T는 등식 추론이 가장 잘 작동하는 모범적 풍경이다. 다음 장에서 우리는 이 평지를 떠나 부분성의 산악 지대로 들어선다.

48장 PCF에 대한 등식 추론 Equational Reasoning for PCF

PCF는 fix를 가진 순간 종료를 잃는다. 그리고 종료를 잃는 순간 외연성은 더 이상 공짜가 아니다. 등식 추론은 이제 부분성과 정면으로 마주해야 한다.

왜 더 어려워지는가

모든 항이 종료하던 T에서는 "두 함수가 모든 인자에서 같다"가 안전한 진술이었다. PCF에서는 f x가 발산할 수 있다. 두 함수가 같다는 말은 이제 "값으로 환원되면 같은 값을 주고, 발산하면 둘 다 발산한다"가 된다. 관찰의 단위가 종료/비종료 여부까지 포함하도록 확장되어야 한다.

형식: 종결 보존과 등식

관찰 동치 e₁ ≅ e₂ : τ의 정의는 다음으로 다듬어진다. 모든 닫힌 문맥 C[·] : nat에 대해 C[e₁] ⇓ n이면 C[e₂] ⇓ n이고 그 역도 성립한다. 발산도 관찰이다. 등식 판단도 이에 맞춰 조정된다. 부동점 풀이 규칙은 다음과 같다.

fix(x.e) ≡ e[fix(x.e)/x]

그러나 이 한 번의 풀이만으로는 무한 행동을 비교할 수 없다. 최소 부동점을 다루기 위해 등식 추론은 승인 원리(admissibility)를 필요로 한다. 술어가 사슬에 대해 닫혀 있으면 부동점에서도 성립한다는 원리.

직관: 두 무한 루프

loop = fix(x.x)와 loop′ = fix(x. (λy.x) 0)은 모두 발산한다. 둘은 같은가? 답은 "그렇다, 모든 자연수 문맥에서 둘 다 같은 방식으로 발산한다." 이 단순한 사실을 등식 시스템이 직접 도출하기는 쉽지 않다. 구문 등식만으로는 무한 행동의 동치를 다 잡지 못하기 때문이다. 그래서 다음 장의 도구가 필요하다 — 논리적 관계.

메타이론: 건전성과 한계

건전성은 살아남는다. 등식 판단이 도출하는 모든 등식은 관찰 동치이다. 그러나 완전성은 무너진다. 관찰 동치이지만 구문 등식 시스템이 도출하지 못하는 짝이 존재한다. 이것은 결함이 아니라 풍부함의 증거이다. PCF의 의미론은 단순한 구문 변환보다 깊고, 그 깊이를 측정하려면 더 강력한 의미론적 도구가 필요하다. 다음 장의 주인공은 그 도구이다.

49장 논리적 관계 Logical Relations

관찰 동치를 직접 다루는 것은 어렵다. 논리적 관계는 그것을 타입에 의해 유도되는 관계로 우회해 다룬다. 단순한 관계가 합성에 의해 풍부한 결과를 낳는 — 의미론의 가장 우아한 무기 중 하나.

아이디어: 타입을 따라 관계를 짠다

핵심 발상은 단순하다. 타입 τ마다 관계 R_τ를 정의하되, 합성 타입에서는 부분 타입의 관계로부터 만들어 낸다. 자연수 타입은 동일성, 함수 타입은 "관계된 인자에 관계된 결과", 곱 타입은 성분별 관계. 관계는 타입 구조를 따라 자동으로 자란다.

R_nat(n, m) ⇔ n = m, R_(τ→σ)(f, g) ⇔ ∀(a, b). R_τ(a, b) ⇒ R_σ(f a, g b)

이 정의는 작은 베이스 케이스로부터 모든 타입 수준에 자동으로 의미를 부여한다.

형식: 기본 정리

논리적 관계의 운영 원리는 기본 정리(Fundamental Theorem)이다. 모든 잘 타입된 항 e는 자신과 관계된다. R_τ(e, e)가 항상 성립한다. 이것이 자명해 보이지만, 합성 타입의 정의에 따라 풀어 쓰면 강력한 결론이 따라 나온다. 함수에 대해 "어떤 두 관계된 인자에든 관계된 결과를 낸다"가 거저 얻어진다는 뜻이다.

직관: 두 가지 응용

첫째, 강한 정규화의 증명. R_τ를 "닫혀서 종료한다"로 풀이하면 모든 잘 타입된 항이 종료한다는 결과가 따른다. 둘째, 관찰 동치 분석. R_τ를 두 항 사이의 관계로 잡으면 관찰 동치를 의미론적으로 다룰 수 있다. PCF에서는 부동점 때문에 정의를 스텝 인덱스(step-indexed)로 정교화해야 하지만, 발상은 동일하다. 단순한 베이스 → 합성에 의한 자동 확장 → 강력한 결론.

메타이론: 한계와 확장

논리적 관계의 한계는 참조나 존재 타입에서 드러난다. 가변 셀이 들어오면 시간이 흐르며 관계가 깨질 수 있고, 단순 정의로는 잡히지 않는다. 이를 위해 월드(world)나 스텝 인덱싱을 도입한 정교한 변형이 발전해 왔다. 그러나 모든 변형은 같은 영혼을 공유한다. 의미를 타입의 구조에 따라 짜라. 그 한 줄이 의미론의 절반을 낳았다.

50장 매개변수성 Parametricity

다형 함수는 균일하게 행동해야 한다는 직관이 있다. 매개변수성은 그 직관을 정리로 바꾼다. 그리고 그 정리는 — 누군가의 표현을 빌리자면 — 타입을 보는 것만으로 정리를 거저 얻게 해 준다.

다형성의 약속

함수 f : ∀α. α → α가 있다. 이 함수의 행동을 우리가 무엇을 알 수 있는가? α가 무엇이든 같은 코드가 작동해야 하므로, f는 자신의 인자에 의존할 수밖에 없다. 인자를 변형할 어떤 도구도 가지고 있지 않다 — α가 무엇인지 모르기 때문이다. 결론은 강하다. f는 항등 함수일 수밖에 없다. 이것이 "타입이 정리를 낳는다"(theorems for free)의 가장 작은 사례이다.

형식: 관계적 해석

매개변수성은 논리적 관계의 다형 버전이다. 타입 변수 α를 임의의 관계 R로 해석한다. 다형 타입 ∀α. τ의 해석은 "어떤 관계 R를 주든 결과가 τ에서 관계된다"이다.

R_(∀α. τ)(f, g) ⇔ ∀ R : Rel(A, B). R_τ[α↦R](f[A], g[B])

이 한 줄에서 모든 매개변수성 결과가 흘러나온다. 자유 정리, 추상 데이터 타입의 표현 독립성, 그리고 다형 인코딩의 정확성까지.

직관: 자유 정리들

몇 가지 사례. f : ∀α. α list → α list이면 f는 원소를 만들어 낼 수 없으므로 결과는 입력 원소들의 어떤 재배열·삭제일 수밖에 없다. g : ∀α. (α → α) → α → α이면 g는 본질적으로 처치 수(Church numeral) 형태로, 입력 함수를 일정 횟수 합성한 것이다. 어떤 구체 코드를 보지 않고 타입만으로 이런 결론이 나온다. 매개변수성은 정적 분석의 비밀 무기이다.

메타이론: 추상화의 정당화

매개변수성은 단순한 트릭이 아니다. 표현 독립성의 형식적 기반이다. 추상 타입 τ를 두 가지 다른 표현 τ₁과 τ₂로 구현해도, 그 두 구현이 적절한 관계로 묶여 있다면 클라이언트 코드는 차이를 알아챌 수 없다 — 그것이 매개변수성의 약속이다. 모듈성과 추상화의 메타이론이 결국 한 점에서 만난다. 다형성, 추상, 모듈은 같은 원리의 세 얼굴이다. 그 원리의 이름이 매개변수성이고, PFPL의 긴 여정이 마지막에 도달하는 산정상이다.