타입 이론(Type theory)

3 + true를 계산하라고 하면 어떻게 될까요? 파이썬은 실행하다가 그 줄에 닿아서야 오류를 냅니다. 타입이 있는 언어는 실행하기 전에 거절합니다. 덧셈의 규칙이 'a가 자연수⁠(natural number)⁠이고 b가 자연수이면 a + b는 자연수다'로 적혀 있는데, true는 자연수가 아니므로 이 규칙을 쓸 수 없고 다른 어떤 규칙도 맞지 않기 때문입니다. 검사기는 식을 계산해 보지 않고 모양만 보고 이 결론을 냅니다. 여기서 타입은 '이 값을 어떤 연산에 쓸 수 있는가'를 적은 꼬리표입니다. 타입 이론은 'a는 타입 A의 원소다'라는 판단 $a : A$를 정해진 규칙으로만 이끌어 내는 체계들을 연구합니다.

$a : A$는 집합⁠(set)⁠론의 $a \in A$와 닮았지만 성격이 다릅니다. 집합론⁠(set theory)⁠에서 $3 \in \mathbb N$은 이미 있는 대상 3과 집합 ℕ에 대한 명제라서 참이거나 거짓이고, 부정할 수도 있습니다. 한 대상이 여러 집합에 속하는 것도 자연스럽습니다. 3은 ℕ에도, $\{3, 7\}$에도 속합니다. 타입 이론에서는 항이 처음 만들어질 때부터 타입과 함께 태어납니다. $a : A$는 체계 안에서 참·거짓을 따지는 명제가 아니라, 규칙으로 이끌어 낼 수 있거나 없는 판단입니다. 판단은 보통 가정과 함께 적습니다. $x : \mathbb N \vdash x + 1 : \mathbb N$은 'x가 자연수라고 두면 x + 1은 자연수다'라는 뜻이고, ⊢ 왼쪽의 가정 목록을 문맥이라 부르며 흔히 Γ로 씁니다.

판단을 명제가 아니라 '규칙으로 이끌어 내는 것'으로 두는 까닭은 기계가 따질 수 있게 하려는 데 있습니다. 많은 체계에서 판단이 성립하는지는 기계적으로 가릴 수 있어서, 타입 검사는 반드시 끝나는 알고리즘⁠(algorithm)⁠이 됩니다. 늘 그런 것은 아닙니다. 예를 들어 두 항이 같다는 증명을 곧바로 판단의 같음으로 쓰는 '외연적' 마르틴뢰프 타입 이론에서는 타입 검사를 결정할 수 없습니다.

타입은 역설을 막는 장치로 태어났습니다. 1901년 러셀은 '자기 자신을 원소⁠(element)⁠로 갖지 않는 집합들의 집합'이 모순을 낳는다는 것을 알아냈고(러셀의 역설), 1903년 『수학의 원리』 부록에서 유형 이론을 처음 스케치한 뒤 1908년 논문에서 본격적으로 내놓았습니다. 가장 단순한 형태로 말하면 생각은 이렇습니다. 개체는 0층, 개체들의 모임은 1층, 1층 모임들의 모임은 2층으로 나누고, 'x ∈ y'는 y가 x보다 정확히 한 층 위일 때만 문장으로 인정합니다. 그러면 'x ∈ x'는 거짓인 문장이 아니라 문법에 맞지 않는 글자열이 되고, 러셀의 집합 $\{x : x \notin x\}$는 적을 수조차 없습니다. 러셀과 화이트헤드의 『수학 원리』(1910–1913)는 층을 더 잘게 나눈 분지 유형 이론을 썼고, 1920년대에 램지 등이 이것을 단순 유형 이론⁠(simple theory of types)⁠으로 다듬었습니다. 1940년 처치는 단순 유형 이론을 자신의 람다 계산⁠(lambda calculus)⁠ 위에 다시 세웠습니다. 모든 변수에 타입을 붙인 이 체계가 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠입니다.

그 뒤 타입 체계는 여러 방향으로 넓어졌습니다. 단순 타입 람다 계산에서는 항이 항에만 의존합니다. 함수⁠(function)⁠ $\lambda x.\, x + 1$은 수를 받아 수를 돌려줍니다. 여기에 의존의 방향을 셋 더할 수 있습니다. 타입을 받는 항(모든 타입 X에 대해 X → X인 항등 함수처럼, 다형성⁠(polymorphism)⁠), 타입을 받는 타입(타입 A를 받아 'A들의 리스트' 타입을 만드는 List처럼, 타입 연산자⁠(type operator)⁠), 항을 받는 타입(수 n을 받아 '길이가 n인 벡터⁠(vector)⁠' 타입을 만드는 것처럼, 의존 타입⁠(dependent type)⁠)입니다. 네덜란드 논리학자 헹크 바렌드레흐트는 1991년 이 세 방향을 정육면체의 세 축으로 그렸습니다. 이것을 람다 큐브라 부릅니다.

타입이 주는 첫째 이득은 안전입니다. 영국 컴퓨터 과학자 로빈 밀너는 1978년 '타입이 맞는 프로그램은 잘못될 수 없다'고 썼습니다. 오늘날 이 말은 보통 두 정리로 정확히 적습니다(라이트와 펠라이센, 1994). 타입이 붙는 항은 이미 값이거나 한 걸음 더 계산할 수 있고(진행), 한 걸음 계산해도 타입이 그대로입니다(보존). 둘을 합치면 3 + true처럼 규칙이 없어 멈춰 버리는 상태에는 결코 닿지 않습니다. 흔한 오해는 여기서 '타입이 맞으면 프로그램이 옳다'로 건너뛰는 것입니다. 받은 리스트를 무시하고 빈 리스트를 돌려주는 '정렬' 함수도 $\mathrm{List}\,\mathbb N \to \mathrm{List}\,\mathbb N$ 타입을 통과합니다. 0으로 나누기나 끝나지 않는 되풀이도 대부분의 언어에서 타입으로 걸러지지 않습니다. 타입이 무엇을 보장하는지는 타입이 무엇을 말할 수 있는지에 달려 있습니다. 의존 타입에서는 '출력은 입력을 정렬한 것이다'까지 타입에 적을 수 있고, 그때 타입 검사는 곧 증명 검사가 됩니다.

둘째는 논리입니다. 타입 $A \to B$를 'A이면 B'로 읽으면, 그 타입의 항은 그 명제의 증명처럼 행동합니다. A의 증명을 받아 B의 증명을 내놓는 방법이기 때문입니다. 이 대응이 커리–하워드 대응⁠(Curry–Howard correspondence)⁠이고, 여기서 증명은 무엇을 어떻게 만드는지 보여 주는 구성이므로 논리는 직관주의 논리⁠(intuitionistic logic)⁠가 됩니다. 타입 검사기가 증명 검사기가 되는 까닭에, 오늘날의 증명 보조기⁠(proof assistant)⁠는 대부분 타입 이론 위에 서 있습니다. 셋째는 끝남입니다. 단순 타입 람다 계산과 시스템 F⁠(System F)⁠에서는 타입이 붙는 항이 모두 끝까지 계산됩니다. 그 대가로 모든 계산을 표현하지는 못합니다. 자연수 같은 자료에 끝나지 않을 수도 있는 되부름까지 넣으면 튜링 기계⁠(Turing machine)⁠만큼 강해지지만, 끝남의 보장과 논리로서의 무모순성⁠(consistency)⁠을 함께 잃습니다.

항에 타입을 적는 방식은 둘입니다. 처치식은 $\lambda x{:}\mathbb N.\, x + 1$처럼 변수의 타입을 항 안에 적고, 커리식은 $\lambda x.\, x + 1$처럼 타입 없이 쓴 뒤 맞는 타입을 찾습니다. 커리식에서 '이 항에 타입을 붙일 수 있는가, 있다면 가장 일반적인 타입은 무엇인가'를 묻는 것이 타입 추론⁠(type inference)⁠입니다. ML과 하스켈이 쓰는 힌들리–밀너 체계에서는 이것을 기계적으로 풀 수 있지만, 시스템 F에서는 풀 수 없다는 것이 증명되어 있습니다(조 웰스, 1994).

러셀의 층은 현대 타입 이론에서 다른 모습으로 돌아옵니다. 타입들을 원소로 갖는 타입 Type이 있으면 편리한데, $\mathrm{Type} : \mathrm{Type}$을 허용하면 모순이 나옵니다. 1972년 프랑스 논리학자 장이브 지라르가 찾은 역설입니다. 순서수⁠(ordinal number)⁠ 전체를 모으면 모순이 생기는 부랄리포르티 역설⁠(Burali-Forti paradox)⁠을 타입으로 옮긴 것으로, '너무 큰 모임'이 모순을 낳는다는 점에서 러셀의 역설과 같은 계열입니다. 그래서 Coq(지금 이름 Rocq)·Lean·Agda 같은 증명 보조기는 $U_0 : U_1 : U_2 : \cdots$처럼 층을 쌓은 우주(universe)를 둡니다. 한편 스웨덴 논리학자 페르 마르틴뢰프가 1970년대에 세운 타입 이론은 ZFC 공리⁠(axiom)⁠ 위의 집합론과 나란히 설 수 있는 수학의 기초⁠(basics)⁠가 되었고, 2000년대 후반 보예보츠키 등은 여기서 같음을 공간 속의 길로 읽는 호모토피 타입 이론⁠(homotopy type theory)⁠을 끌어냈습니다.

이어지는 곳. 타입 이론의 출발점은 단순 타입 람다 계산이며, 규칙 세 개로 항의 타입을 이끌어 내는 과정과 모든 계산이 끝나는 이유를 거기서 볼 수 있습니다. 규칙에서 항을 지우면 논리 규칙만 남는다는 것이 커리–하워드 대응이고, 그 논리가 배중률⁠(law of excluded middle)⁠을 쓰지 않는 까닭은 직관주의 논리에서 다룹니다. 타입을 +, ×, 거듭제곱으로 셈하면 생성함수⁠(generating function)⁠와 미분⁠(differentiation)⁠까지 이어지는데, 이것이 대수적 자료형⁠(algebraic data type)⁠입니다. 람다 큐브⁠(lambda cube)⁠의 세 축은 각각 다형성과 시스템 F, 타입 연산자, 의존 타입으로 이어집니다. 타입과 함수가 이루는 구조를 따로 떼어 보면 범주론⁠(category theory)⁠이 되고, 곱 타입⁠(product type)⁠을 갖춘 단순 타입 람다 계산이 데카르트 닫힌 범주⁠(cartesian closed category)⁠의 내부 언어라는 사실이 두 세계를 잇습니다. 타입 이론으로 수학을 적고 기계로 확인하는 일은 증명 보조기에서 일어납니다. 다만 산술을 담을 만큼 강하고 모순이 없는 형식 체계라면 무엇이든 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠의 한계를 받으며, 타입 이론도 예외가 아닙니다. 하위 타입⁠(subtype)⁠과 변성⁠(variance)⁠은 하위 타입과 변성에서, 자원을 정확히 한 번씩 쓰는 타입은 선형 논리⁠(linear logic)⁠에서, 재귀⁠(recursion)⁠로 정의한 프로그램이 무엇을 뜻하는지는 영역 이론⁠(domain theory)⁠에서, 프로그램 옆에 조건을 적어 명세를 증명하는 다른 길은 호어 논리⁠(Hoare logic)⁠에서 이어집니다.