타입에도 타입이 필요하다. 정확히 말하면 — 타입을 분류하는 어떤 메타 단계의 표지가 필요한데, 우리는 이를 종류(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장의 진짜 보상이다.
"이 자리에 저 값을 넣어도 되는가?" — 부타입 관계 τ <: σ는 그 질문에 답한다. 본질은 단순하다. τ의 값이 어디서나 σ의 값처럼 행세할 수 있다면 τ <: σ다.
부타입을 시스템에 들이는 표준 통로는 포섭(subsumption)이다.
Γ ⊢ e : τ τ <: σΓ ⊢ e : σ이 규칙이 들어오면 타입은 더 이상 유일하지 않다 — 한 항이 여러 타입을 가질 수 있다. 그래서 알고리즘적 타이핑은 "주어진 항의 최소 타입"을 추론하고, 필요한 자리에서만 부타입 점검을 호출하는 방식으로 재구성된다.
합성 타입에서 부타입은 위치마다 다르게 흐른다. 곱 타입은 양쪽 모두 공변이다.
τ₁ <: σ₁ τ₂ <: σ₂ ⇒ τ₁ × τ₂ <: σ₁ × σ₂
함수 타입은 결과는 공변, 인자는 반변이다.
σ₁ <: τ₁ τ₂ <: σ₂ ⇒ τ₁ → τ₂ <: σ₁ → σ₂
가변 참조 셀은 양쪽이 모두 일치해야 하므로 불변(invariant)이다. 이 차이를 직관으로 말하면 — 받는 입장에서는 더 좁아도 되지만, 주는 입장에서는 더 넓어야 한다.
레코드 부타입은 두 축으로 갈라진다. 필드를 더 가지면 좁다 (폭 부타입), 같은 필드에서 각 타입이 좁으면 좁다 (깊이 부타입). 객체 지향 언어가 부타입을 사랑하는 이유가 여기 있다 — "더 많은 메서드를 가진 객체는 더 적게 요구하는 자리에 들어갈 수 있다"는 직관이 깔끔히 형식화된다. 메타이론에서는 일관성(coherence)을 챙겨야 한다. 같은 항을 같은 타입으로 유도하는 두 경로가 의미상 일치해야 한다는 요구다.
종류 단계에 "이 생성자는 정확히 저 생성자와 같다"라는 사실을 새겨 넣을 수 있을까? 싱글턴 종류 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)로 진행되며, 결정 가능성·소거 가능성을 보장한다. 표면은 작아 보여도, 모듈 시스템 메타이론의 절반이 이 한 가지 종류 위에 서 있다.
"같은 메시지에 대해 객체마다 다르게 반응한다." — 객체 지향의 핵심 마법이지만, 사실은 매우 보수적인 형식 장치다. 디스패치를 떼어내 보면 결국 태그된 합 + 람다 테이블일 뿐이다.
한 객체를 클래스 태그와 인스턴스 상태의 짝으로 본다. 메서드 호출은 두 단계로 일어난다. 첫째, 태그를 보고 적절한 메서드 본문을 골라낸다. 둘째, 그 본문을 인스턴스 상태에 적용한다. 메서드 모음을 클래스 벡터 cls : { c₁ ↦ m₁, ..., cₙ ↦ mₙ }로 두면, 호출 의미는
(c, s) ⇐ msg ⇓ cls(c).msg(s)
로 깨끗이 적힌다. 즉, 디스패치는 분기일 뿐이다 — 하지만 분기 키가 컴파일 시점이 아닌 실행 시점의 객체에 박혀 있다는 점이 다르다.
같은 디스패치를 두 갈래로 조직할 수 있다. 클래스 우선은 클래스 본문 안에 메서드 케이스를 모은다(전형적인 OO 언어). 메서드 우선은 메서드 이름별로 모든 클래스 케이스를 한 곳에 모은다(다중 메서드의 출발점). 두 표현은 행렬의 행과 열처럼 서로의 전치(transpose)다. 어느 쪽이 더 "자연"한가는 — 어떤 차원으로 확장할 일이 잦은가에 달려 있다(표현 문제).
이 시점에서 부타입은 자연히 등장한다. 메시지 집합이 더 많은 클래스 태그는 더 적게 요구하는 자리에 들어갈 수 있다 — 폭 부타입의 정확한 재현이다. 진보(progress)와 보존(preservation)은 표준 합 타입의 경우와 평행하게 증명된다. 마법은 사라지고, 형식만 남는다.
상속은 단지 코드 공유가 아니다. 자기 참조(self-reference)와 덮어쓰기(override)의 결합이며, 그래서 의외로 미묘한 고정점 의미론을 끌어들인다.
상속을 깨끗이 다루려면 클래스와 객체를 분리해야 한다. 클래스는 — 슈퍼 클래스의 메서드 표를 받아 새 메서드 표를 돌려주는 함수다.
cls : (self → super) → (self → own)
여기서 self는 아직 결정되지 않은 "자기 자신"의 메서드 표를 가리키는 자리다. 객체 생성은 이 함수에 고정점을 취하는 일이다.
obj ≡ fix self. cls(self) ⊕ super(self)
self는 항상 최종 객체를 가리킨다 — 그래서 서브클래스에서 덮어쓴 메서드도 슈퍼클래스가 호출했을 때 자동으로 새 버전이 불려나온다(이른바 open recursion). 반면 super는 덮어쓰기 직전의 표를 가리키므로, 자식에서 부모 구현을 명시적으로 호출할 수 있다. 이 두 자리의 분리가 상속의 의미를 결정한다.
타입 측면에서 — 리스코프 치환 원리는 결국 부타입의 한 그림자다. 자식 클래스의 메서드는 부모 메서드의 자리에 들어가야 하므로, 인자에는 반변, 결과에는 공변이라는 같은 분산 규칙이 적용된다. 그러나 자기 참조 때문에 허약한 기반 클래스 문제(fragile base class)가 발생한다 — 부모를 살짝 바꿨을 뿐인데 자식이 깨진다. 메타이론은 이를 정직히 인정한다. 상속은 모듈성을 끊는다(breaks abstraction). 그래서 PFPL은 클래스를 모듈 위의 편의 표기로 격하시키고, 진짜 추상화는 시그너처가 담당하게 둔다.
평가 문맥(evaluation context)을 명시적인 자료 구조로 빼내면 — 그것이 곧 제어 스택이다. 이 단순한 변환이 예외, 연속, 코루틴 같은 모든 제어 효과의 출발점이 된다.
큰-단계 의미론은 평가 문맥을 메타 단계에 숨긴다. 작은-단계로 가도 평가 문맥은 여전히 메타 표기다. 제어 스택은 그 문맥을 항(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′)임을 보인다. 보존성과 진보는 세 모드 각각에 대해 따로 진술되며, 스택 자체에도 타입을 매겨 — 스택 타입 τ ⇒ σ이라는 새로운 분류 도구를 얻는다. 이 도구가 다음 장들의 기반이다.
정상 흐름이 어긋났을 때 우리는 호출 사슬의 임의의 지점까지 한 번에 빠져나가고 싶다. 예외는 — 제어 스택을 표지점까지 잘라내는 비국소 점프의 형식적 정수(精髓)다.
두 가지 새 항이 들어온다. throw(e)와 try e₁ ow x. e₂(예외 발생 시 x로 결박된 값과 함께 핸들러로 분기). K-기계 위에서 의미는 깔끔하다.
k ▷ throw(v) ↦ unwind(k, v)
여기서 unwind는 가장 가까운 try 프레임을 찾을 때까지 스택을 팝하고, 찾으면 핸들러로 진입하는 함수다. 만약 끝까지 핸들러가 없다면 — 프로그램은 비정상 종료한다.
예외 값에는 타입이 있어야 한다. 단순한 길은 전역 예외 타입 exn을 두고 throw : exn → τ로 두는 것이다. throw의 결과 타입이 임의의 τ일 수 있는 이유는 — 정상적으로 반환하지 않기 때문에 어떤 결과 타입에도 일치한다고 칭할 수 있어서다(보존성에는 무해하다). 좀 더 정밀하게는 효과(effect) 시스템으로 어떤 함수가 어떤 예외를 던질 수 있는지를 타입에 새기지만, 그쪽은 표현력과 사용성의 균형 문제다.
예외는 본질적으로 일방향이다. 한 번 빠져나가면 돌아올 수 없다. 이 비대칭이 — 다음 장의 연속과의 결정적 차이다. 보존성 증명은 unwind가 잘 정의되어 있고 핸들러의 결박 타입이 throw의 인자 타입과 일치함을 확인하는 일로 환원된다. 진보 명제는 "값이 아닌 항은 한 발 더 가거나, 처리되지 않은 예외를 던지거나" 둘 중 하나라는 살짝 확장된 형태로 진술된다. 예외가 있는 언어에서는 — "막다른 골목"도 정상적인 결과의 한 종류라는 사실을 메타이론이 인정해야 한다.
"여기서 끝까지 가면 무슨 일이 일어날까?"라는 질문 자체를 값으로 만들 수 있다면 — 그 값이 연속이다. 28장의 제어 스택에 일급 시민권을 부여한 결과다.
두 연산이 핵심이다. 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은 연속을 강력하지만 조심히 다뤄야 할 도구로 자리매김한다.
"그저 이름일 뿐인 이름"이 필요한 순간이 있다. 비교만 가능하고 내용은 없는 — 심볼은 언어가 새 이름을 동적으로 만들어내고 영원히 구분하게 해준다.
새 심볼을 도입하는 연산을 new a:τ in e로 적는다. 이 식은 — 완전히 새로운 이름 a를 하나 만들어 그 사용 범위를 e로 한정한다. 표면적으로는 let과 비슷해 보이지만 본질이 다르다. a는 값이 결박된 변수가 아니라, 식별자 그 자체다. 형식 판단은 심볼 환경 Σ를 추가해
Γ ⊢_Σ e : τ
로 적고, new는 Σ를 확장하면서 본문을 평가한다.
심볼만으로는 거의 아무것도 못한다. 같은가 다른가만 물을 수 있을 뿐이다(a == b). 그런데 이 약함이 곧 유용함이다 — 심볼을 키로 삼아 다른 자료 구조에 결합할 수 있다. 다음 장의 유동 바인딩, 동적 분류된 데이터(dynamic classification), 가변 셀의 식별자, 클래스 태그까지 — 심볼이 비공식적으로 깔리지 않은 자리가 거의 없다.
"전적으로 새로운"이라는 말을 형식화하기 위해서는 — α-동치를 매우 진지하게 다루어야 한다. new a in e와 new b in [b/a]e는 동치이고(이름의 선택은 의미가 아니다), 동시에 한 평가 시퀀스 안에서 두 번 도입된 심볼은 결코 같지 않다(이름의 동일성은 의미다). 이 두 직관이 모순처럼 보이지만 형식적으로는 깔끔히 양립한다 — 심볼은 구문 안에서는 묶여 있고, 실행 중에는 풀려 외부 환경 Σ에 등록되기 때문이다. 진보·보존성은 평소대로지만, 이제는 Σ가 단조 증가한다는 점을 추가로 챙겨야 한다.
정적 범위는 — 변수가 텍스트상의 결박에 묶인다. 유동 바인딩은 다르다. 변수의 값이 호출 시점의 동적 환경에 따라 결정된다. 강력하고, 위험하며, 그리고 여전히 진짜 쓸모가 있다.
심볼 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의 메시지가 분명해진다. 형식은 자유를 보장해 주지만, 자유는 절제와 짝을 이룰 때만 의미를 가진다.