타입의 그늘에서 한 발 벗어나 보자. 모든 항이 동일한 자격으로 굴러다니는 세계, 즉 단 하나의 문법 범주만으로 계산을 흉내내는 자리에서 우리는 무엇이 가능하고 무엇이 잃어버려지는지를 가늠하게 된다.
타입 시스템은 의미 있는 항만 골라내는 검열관이다. 이 검열관을 잠시 해고하면 이상한 일이 벌어진다. 자기 자신을 인자로 받는 항도, 자신을 호출하는 함수도 모두 적법해진다. 이러한 자유에는 대가가 따른다. 항의 정상화는 보장되지 않으며, "값"의 개념은 함수 추상으로 축소된다. 그러나 이 축소된 세계가 충분히 풍부하다는 사실이 바로 이 장의 핵심 주장이다.
타입 없는 λ-계산 Λ의 항은 단 세 가지로 충분하다.
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)는 여기서 깨지고, 그 자리에 자기 적용이 들어온다. 다음 장에서 우리는 이 무정형의 세계를 다시 타입의 어휘로 흡수하는 한 가지 방법, 즉 동적 타이핑을 다룬다.
"타입이 없다"는 말은 사실 "타입이 하나뿐이다"라는 말의 다른 표현이다.
동적 언어가 "타입이 없다"는 통념은 절반만 맞다. 실제로는 모든 값이 자신의 종류를 표시하는 꼬리표를 달고 다닐 뿐, 그 꼬리표가 정적 단계가 아니라 실행 단계에서 검사된다. 이 장에서는 그 꼬리표 사고방식을 형식화한다.
동적 타입 언어 DPCF의 모든 항은 단일한 정적 타입 dyn을 가진다. 그러나 dyn 값은 내부적으로 클래스(class)로 구분된다. 자연수, 부울, 쌍, 함수 등은 각각의 생성자를 통해 dyn으로 주입(injection)되고, 사용 시점에 클래스 검사를 통해 사영(projection)된다. 이렇게 보면 동적 언어는 사실상 거대한 합 타입(sum type)을 등에 짊어지고 다니는 정적 언어다.
Γ ⊢ e : dynΓ ⊢ num!(e) : dyn여기서 num!은 자연수 클래스로의 주입자다. 반대로 사영은 검사를 동반한다.
Γ ⊢ e : dynΓ ⊢ num?(e) : dyn실행 시 num?(num!(v))는 v로 풀리지만, num?(fun!(v))는 클래스 불일치 오류로 정지한다. 즉 정적으로는 모두 dyn → dyn으로 통하던 호출이, 동적으로는 클래스 부조화를 만나면 실패한다.
동적 타이핑의 매력은 "지금은 모르겠다"를 합법화한다는 점이다. 프로토타이핑 단계에서 자료 구조는 자주 변하고, 정적 타이핑은 그때마다 부담을 지운다. 모든 값이 하나의 타입으로 통일되면, 컬렉션은 이질적이 되고 함수는 다형적으로 보이며, REPL은 즉시 응답한다. 이는 형식 체계의 결함이 아니라 의도적 결정이다 — 검사 시점을 늦춤으로써 표현의 자유를 사들인 것이다.
안전성 정리(safety)는 살아남는다. 다만 진보(progress) 진술이 약화될 뿐이다. 잘 타입된 항은 값이 되거나, 한 걸음 진행하거나, 클래스 불일치로 정지한다. 이 세 번째 출구가 정적 타입에는 없던 것이다. 결국 동적 타이핑이란 "타입 검사를 시간축 위에서 미루는 일"이며, 정적 타입과 동적 타입의 우열 논쟁은 이 시간축 위에서의 비용 분담 문제로 환원된다.
동적 언어는 타입을 잃은 것이 아니라, 타입을 항상 휴대하고 다닌다.
정적은 안전하나 답답하고, 동적은 자유로우나 불안하다. 그렇다면 두 세계를 한 언어 안에 동거시키되 그 경계를 형식적으로 그어두면 어떨까? 이 장에서 다루는 혼합 타이핑은 바로 그 동거 계약서다.
혼합 언어 HPCF에서는 정적으로 알려진 타입 τ와 만능 타입 dyn이 함께 산다. 이 둘 사이를 오가는 통로는 두 가지 변환자다. 하나는 정적 값을 동적 영역으로 띄우는 τ ⇒ dyn이고, 다른 하나는 동적 값을 정적 타입으로 끌어내리는 dyn ⇒ τ다. 후자는 본질적으로 불완전한 변환이다. 검사가 실패하면 실행은 정지한다.
혼합 언어의 핵심 조작은 다음 두 형태다.
e ⇑ τ : dyn e ⇓ τ : τ
위쪽 화살표는 안전한 주입이고, 아래쪽 화살표는 검사 동반 사영이다. 가령 τ = nat → nat일 때, 동적 영역에서 받은 값 e : dyn을 정적 함수로 쓰려면 e ⇓ (nat → nat)로 적어야 한다. 그러나 함수의 본문은 인자를 받기 전엔 검사할 수 없으므로, 실제로는 인자와 결과 양쪽에 대해 또 한 번씩 변환자가 끼어든다. 이른바 계약(contract) 또는 캐스트의 전파다.
이 형식은 점진적 타이핑(gradual typing)의 토대로도 익숙하다. 프로그램의 일부는 풍부하게 타입되어 있고, 다른 일부는 dyn으로 남아 있다. 두 영역의 접합점마다 캐스트가 자동으로 삽입되며, 정적 부분의 보장은 동적 부분에서 들어온 값이 캐스트 검사를 통과하는 한도 내에서 유지된다. 이것이 "점진적 보장"의 본질이다 — 정적 타입은 자신의 영역 내에서는 전통적 안전성을 누린다.
혼합 언어의 정연함은 캐스트가 일등 시민이라는 점에서 비롯된다. 캐스트는 단순한 어댑터가 아니라 의미를 생성하는 행위자다. nat → nat으로의 캐스트와 nat → bool로의 캐스트는 같은 동적 함수 위에 다른 운명을 부여한다. 후자는 호출되는 순간이 아니라 결과를 돌려주는 순간 무너진다. 이 지연 검사가 혼합 시스템 메타이론의 묘미이며, 정적/동적의 이분법이 사실은 연속체임을 일깨운다.
캐스트는 변환이 아니라 약속이다. 어길 때 비로소 의미가 드러난다.
"증명한다"와 "구성한다"가 한 단어가 되는 순간, 논리는 프로그래밍 언어가 된다. 직관주의 논리는 진리치가 아니라 증거에 무게를 두고, 증거는 항상 무언가를 만들어내는 절차여야 한다는 입장이다. 카리-하워드 대응이 자라나는 토양이 바로 여기다.
고전 논리에서 A ∨ ¬A는 무료로 주어진다. 직관주의 논리에서는 그렇지 않다. A ∨ B의 증거를 가지려면 A의 증거를 제시하거나 B의 증거를 제시해야 하며, 어느 쪽인지를 명시해야 한다. 즉 분리는 합 타입이고, 두 가지 도입 규칙은 inl과 inr에 대응한다. 마찬가지로 함의 A ⊃ B는 함수 타입 A → B이며, 그 증거는 A의 증거를 받아 B의 증거를 돌려주는 절차다.
직관주의 명제 논리의 도입·소거 규칙은 다음 짝으로 정리된다.
Γ ⊢ a : A Γ ⊢ b : BΓ ⊢ ⟨a, b⟩ : A ∧ BΓ, x : A ⊢ b : BΓ ⊢ λx:A.b : A ⊃ B거짓 ⊥은 도입 규칙이 없는 명제이며, 그 소거 규칙은 어떤 결론이든 끌어내는 폭발률(ex falso)이다. ¬A는 A ⊃ ⊥의 약어로 정의된다. 즉 부정은 별도의 연결자가 아니라 함의의 특수형이다.
"구성적"이라는 형용사는 단순한 신중함이 아니다. 그것은 모든 존재 진술이 증인을 동반해야 한다는 강한 요구다. ∃x.P(x)를 증명한다는 것은 그러한 x를 실제로 만들어내는 알고리즘을 제시한다는 의미다. 이 관점에서 보면 직관주의 산술의 모든 정리는 자동으로 프로그램이며, 그 프로그램은 증명에서 직접 추출된다.
증명의 정상화(normalization)는 프로그램의 평가에 정확히 대응한다. β-축약은 절단 제거(cut elimination)이며, 정상형은 직접 증명이다. 이 대응은 단순한 비유가 아니라 형식적 동치다 — 명제는 타입이고, 증명은 항이며, 증명의 단순화는 평가다. 그러므로 직관주의 논리를 공부하는 일은 곧 함수형 언어의 의미론을 공부하는 일이다.
고전논리가 "그렇다"를 말한다면, 직관주의 논리는 "어떻게 그러한지"를 보여달라고 요구한다.
배중률을 다시 가져오면 어떤 일이 벌어지는가? 놀랍게도 논리는 그대로 풍부해지지만, 대응되는 계산 모델은 함수가 아니라 제어(control)의 세계가 된다. 고전 논리는 곧 계속(continuation)의 논리다.
직관주의 논리에서는 도입과 소거가 좌우 대칭으로 균형 잡혀 있다. 고전 논리는 이 균형을 한쪽으로 기울인다. 이중 부정 제거 ¬¬A ⊃ A나 페어스 법칙 ((A ⊃ B) ⊃ A) ⊃ A는 직관주의에서는 증명되지 않으나 고전에서는 공리로 들어온다. 이러한 추가 원리들은 단순한 진리치 보충이 아니라, 계산적으로는 "지금까지의 맥락을 통째로 끌어다 쓰는 능력"으로 해석된다.
고전 자연 연역은 다중 결론(multiple-conclusion) 시퀀트로 가장 자연스럽게 표현된다.
Γ ⊢ Δ
여기서 Γ는 가정의 다중집합, Δ는 결론의 다중집합이다. 직관주의에서 Δ는 한 개로 제한되었지만, 고전에서는 여럿이 허용된다. 이 사소해 보이는 변화가 배중률을 돌려준다 — ⊢ A, ¬A는 두 결론을 동시에 후보로 두는 시퀀트로 즉시 도출된다.
카리-하워드 대응을 고전 논리로 끌어올리면 새로운 항이 등장한다. 그 대표가 callcc다. 페어스 법칙은 callcc의 타입이며, 이 항은 자신을 호출하는 시점의 계속을 포착해 변수에 묶는다. 즉 고전 증명은 계산적으로 백트래킹·예외·점프를 포함한 제어 흐름의 표현력을 갖는다. throw는 그렇게 묶어둔 계속에 값을 던져 흐름을 옮기는 행위다.
고전 논리의 정상화는 직관주의에 비해 까다롭다. β-축약 외에 계속에 관한 축약 규칙이 추가되며, 한 항의 정상형이 유일하지 않을 수도 있다(컨플루언스의 약화). 그러나 이것은 결함이라기보다 본성이다. 프로그램이 평가 순서에 따라 다르게 부수효과를 일으키는 현실을, 고전 증명의 비결정성이 그대로 담아낸다. 결국 고전 논리는 더 강한 논리가 아니라, 다른 종류의 계산을 드러내는 논리다.
고전 논리가 "지금까지의 맥락"을 일급 객체로 다룬다면, 이는 사실 운영체제가 스택을 다루는 일과 닮아 있다.
하나의 알고리즘이 여러 타입에서 작동해야 한다는 요구는 흔하다. 리스트의 길이를 재는 일에 원소의 종류는 무관하다. 이 무관함을 형식적으로 포착하는 장치가 타입에 대한 양화이며, 그 표준 무대가 시스템 F다.
시스템 F는 항 추상 λx:τ.e 위에 타입 추상 Λα.e를 한 층 더 얹는다. 후자는 "어떤 타입 α가 들어오든 본문 e를 그 α로 인스턴스화해 쓸 수 있다"는 약속이다. 대응하는 타입은 보편 양화 ∀α.τ이며, 적용은 e[σ]로 적는다. 이 두 단계의 추상이 시스템 F의 표현력을 폭발시킨다.
Δ, α type; Γ ⊢ e : τΔ; Γ ⊢ Λα.e : ∀α.τΔ; Γ ⊢ e : ∀α.τ Δ ⊢ σ typeΔ; Γ ⊢ e[σ] : [σ/α]τ항등 함수의 다형 버전은 Λα.λx:α.x : ∀α.α → α이다. 이 한 항이 자연수 항등, 부울 항등, 함수 항등 모두로 인스턴스화된다.
시스템 F는 명시적 자료 구조 없이도 곱·합·자연수·리스트를 모두 정의한다. 가령 자연수 타입은 ∀α.(α → α) → α → α로 인코딩되며, 이는 직관적으로 "어떤 결과 타입에서든, 후속자 함수와 시작값이 주어지면 답을 만들어내는 절차"다. 이 인코딩은 처치의 유산을 타입 위로 끌어올린 것이다. 차이는 분명하다 — 타입 없는 인코딩이 동음이의로 흐릿했다면, 시스템 F의 인코딩은 타입이 의미를 고정한다.
시스템 F는 강한 정상화 성질을 가진다 — 모든 잘 타입된 항은 정상형으로 환원된다. 그러나 이 정리의 증명은 더 이상 단순한 구조 귀납이 아니다. 타입 위의 양화가 자기 자신을 포함할 수 있기 때문이다(임프레디카티브 양화). 이 자기 참조의 위험을 다루는 표준 도구가 가환성 술어 또는 논리 관계 기법이다. 또 한 가지 — 시스템 F의 타입 추론은 결정 불가능하다. 따라서 실용 언어는 부분 다형성(예: 랭크-1 다형성)으로 절충한다.
"다형성"이라는 이름은 그리스어로 "여러 모양"이지만, 시스템 F에서는 "단 하나의 모양이 모든 타입을 견뎌낸다"는 뜻에 가깝다.
"이 모듈은 어떤 표현을 쓰는지 묻지 마라. 다만 약속된 인터페이스를 통해 쓰라." 이 모듈성의 격언이 형식 체계로 옮겨질 때, 우리는 존재 양화 ∃α.τ를 만난다. 보편 양화가 "임의의 타입에 대해"라면, 존재 양화는 "어떤 타입이 있어서"이다.
존재 타입의 도입은 패키징(packing)이다. 구현 타입 ρ와 그 위의 구현체 e : [ρ/α]τ를 묶어 pack {ρ; e} as ∃α.τ를 만든다. 외부에서 보이는 것은 ∃α.τ뿐이며, 내부 표현 ρ는 봉인된다. 이 봉인을 풀어 쓰는 일이 개봉(unpacking)이다.
open e₁ as ⟨α, x⟩ in e₂
여기서 α는 새로운 타입 변수로, e₂의 본문 안에서만 통한다. 이 범위 제한이 추상의 핵심이다 — 누설이 일어나면 추상은 무너진다.
Δ ⊢ ρ type Δ; Γ ⊢ e : [ρ/α]τΔ; Γ ⊢ pack {ρ; e} as ∃α.τ : ∃α.τΔ; Γ ⊢ e₁ : ∃α.τ Δ, α type; Γ, x:τ ⊢ e₂ : σ Δ ⊢ σ typeΔ; Γ ⊢ open e₁ as ⟨α, x⟩ in e₂ : σσ가 α를 포함해서는 안 된다는 마지막 조건이 표현 누설(representation leakage)을 막는 빗장이다.
스택의 추상 타입을 살펴보자. 인터페이스는 τ_stack ≡ {empty : α, push : nat × α → α, pop : α → (nat × α) opt}로 잡자. 한 구현은 리스트를 사용하고 다른 구현은 배열을 사용해도 좋다. 두 구현 모두 ∃α.τ_stack의 시민이며, 외부 코드는 어느 구현이 들어 있는지 알지 못한 채 동일한 함수 호출만으로 작업한다. 모듈 시스템의 시그니처 매칭은 본질적으로 이 패키징의 정교화다.
존재 타입의 안전성은 표현 독립성(representation independence) 정리로 이어진다. 두 구현이 인터페이스 위에서 관찰적으로 동등하다면, 어느 쪽으로 바꿔 끼워도 클라이언트 코드의 의미는 변하지 않는다. 이 정리는 모듈 교체·리팩터링·최적화의 형식적 근거다. 실용 언어의 모듈은 이 위에 함자(functor), 정련(refinement), 봉인(sealing) 같은 장식을 얹지만, 뼈대는 모두 ∃α.τ다. 그러므로 다음 부에서 다룰 더 풍부한 모듈 체계는 결국 존재 양화의 후예들이라고 보아도 좋다.
보편 양화는 너그러움이고, 존재 양화는 비밀주의다. 좋은 라이브러리는 두 미덕을 모두 갖춘다.