의존 타입(Dependent types)

리스트의 첫 원소⁠(element)⁠를 꺼내는 함수⁠(function)⁠ head는 빈 리스트를 받으면 줄 것이 없습니다. 보통의 타입 $\mathrm{List}\,A\to A$로는 이 사정을 적을 수 없어서, 많은 언어에서 빈 리스트의 head는 실행 중에 오류를 냅니다. 이제 타입에 수를 넣을 수 있다고 해 봅시다. $\mathrm{Vec}\,A\,n$을 'A의 원소가 정확히 n개인 리스트'의 타입이라 하면 $\mathrm{head} : \mathrm{Vec}\,A\,(n+1)\to A$라고 적을 수 있고, 빈 리스트 $[\,] : \mathrm{Vec}\,A\,0$에 head를 적용하는 코드는 실행하기 전에 타입 검사에서 거부됩니다. 0은 어떤 자연수⁠(natural number)⁠ n에 대해서도 n + 1이 아니기 때문입니다. 이처럼 값(여기서는 길이 n)에 따라 달라지는 타입을 의존 타입이라 합니다.

의존 타입⁠(dependent type)⁠에는 두 가지 기본 구성이 있습니다. Π 타입 $\prod_{x:A} B(x)$는 입력 x마다 출력의 타입 B(x)가 달라지는 함수의 타입입니다. 길이를 받아 그 길이만큼 0으로 채운 벡터를 만드는 함수는 $\mathrm{zeros} : \prod_{n:\mathbb N} \mathrm{Vec}\,\mathbb N\,n$입니다. Σ 타입 $\sum_{x:A} B(x)$는 첫 성분 a와, 그 a가 정하는 타입 B(a)의 원소를 묶은 쌍의 타입입니다. $\sum_{n:\mathbb N} \mathrm{Vec}\,A\,n$은 '길이 하나와 그 길이의 벡터'이니, 길이를 미리 모르는 보통의 리스트와 원소가 하나씩 짝지어집니다. B가 x에 의존하지 않으면 Π는 보통의 함수 타입 A → B로, Σ는 곱 타입⁠(product type)⁠ A × B로 돌아갑니다. 곱과 합의 기호를 쓰는 까닭은 원소를 세어 보면 드러납니다. 밑 A의 점 x마다 그 위에 섬유 B(x)가 놓여 있다고 그리면, Σ의 원소는 섬유들 가운데 아무 점 하나이고, Π의 원소는 섬유마다 점을 하나씩 고른 것(단면)입니다.

그림의 Fin n은 원소가 0, 1, …, n − 1의 n개인 타입입니다. 섬유는 입니다. Π의 원소 수는 , Σ의 원소 수는 입니다. 지금 고른 단면은 이고, 분홍 고리의 점은 Σ의 원소 입니다.

섬유의 크기가 모두 |B|로 같으면 곱은 $|B|^{|A|}$, 합은 $|A|\cdot|B|$이 되어 대수적 자료형⁠(algebraic data type)⁠의 셈 $|A\to B| = |B|^{|A|}$, $|A\times B| = |A|\,|B|$로 돌아갑니다. 섬유 하나가 비어 있으면 합에는 아무 일이 없지만 곱은 0입니다. 빈 섬유에서는 고를 점이 없기 때문입니다.

명제가 타입이 된다. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠에서 A → B가 'A이면 B'였다면, 의존 타입에서는 Π가 '모든 x에 대해 B(x)'가, Σ가 'B(x)인 x가 있다'가 됩니다. Σ의 원소는 증인 x와 그 x가 조건을 만족한다는 증명의 쌍이므로, 이 '있다'는 증인을 내놓아야 하는 직관주의 논리⁠(intuitionistic logic)⁠의 '있다'입니다. 여기에 같음을 뜻하는 타입 $a = b$(동일성 타입⁠, identity type⁠)를 더합니다. 이 타입의 원소를 만드는 기본 방법은 $\mathsf{refl}_a : a = a$ 하나뿐입니다. 이제 'n + 0 = n'이나 '소수⁠(prime number)⁠는 무한히 많다' 같은 수학의 명제가 타입으로 적히고, 그 타입의 원소를 만드는 프로그램이 증명이 됩니다.

귀납법은 되부름이다. 자연수를 0과 succ(다음 수)로 짓고(페아노의 방식), 덧셈을 첫째 인자에 대한 되부름으로 정의합니다: $0 + m = m$, $\mathrm{succ}\,k + m = \mathrm{succ}\,(k + m)$. 그러면 $0 + n = n$은 증명할 것도 없습니다. 정의의 첫째 줄로 곧바로 계산되므로 refl이 증명입니다. 그러나 $n + 0 = n$은 다릅니다. n이 변수이면 n + 0은 더 계산되지 않습니다. 이것을 증명하는 것이 다음의 되부르는 함수입니다.

$$\begin{aligned} &\mathrm{pz} : \textstyle\prod_{n:\mathbb N}\: n + 0 = n \\ &\mathrm{pz}\:0 = \mathsf{refl} \\ &\mathrm{pz}\:(\mathrm{succ}\,k) = \mathrm{ap}_{\mathrm{succ}}\,(\mathrm{pz}\:k) \end{aligned}$$

첫째 줄에서 필요한 타입은 0 + 0 = 0인데, 0 + 0은 정의로 0이 되므로 refl이 맞습니다. 둘째 줄에서 필요한 타입은 succ k + 0 = succ k이고, 왼쪽은 덧셈 정의의 둘째 줄로 succ (k + 0)이 됩니다. 되부른 pz k는 k + 0 = k의 증명이고, 같은 것에 succ를 씌우면 같다는 $\mathrm{ap}_{\mathrm{succ}}$가 이것을 succ (k + 0) = succ k로 바꿔 줍니다. 첫째 줄은 수학적 귀납법⁠(mathematical induction)⁠의 기초 단계⁠(base case)⁠, 둘째 줄은 귀납 단계⁠(inductive step)⁠이고, 둘째 줄에서 k에 대해 되부르는 것이 곧 귀납 가정을 쓰는 것입니다. 되부름이 늘 더 작은 수로 내려가므로 계산은 반드시 끝나고, 그래서 이 '증명'은 순환 논증이 아닙니다. 의존 타입 언어가 되부름이 끝나는지 검사하는 까닭이 여기에 있습니다.

n = 으로 두고 pz n이 펼쳐지는 과정을 따라가 봅니다.

정의로 같음⁠(definitional equality)⁠과 증명해야 같음. 방금 본 비대칭은 우연이 아닙니다. 타입 검사기는 식을 계산해서 같아지는 것(정의로 같음)은 스스로 알아보고, 그렇지 않은 것(증명해야 같음)은 증명을 요구합니다. 두 벡터를 잇는 함수 $\mathrm{append} : \mathrm{Vec}\,A\,m\to\mathrm{Vec}\,A\,n\to\mathrm{Vec}\,A\,(m+n)$를 첫째 벡터에 대한 되부름으로 쓰면, 빈 벡터의 경우 결과 타입 Vec A (0 + n)이 계산으로 Vec A n이 되고, x :: xs의 경우 Vec A (succ m + n)이 Vec A (succ (m + n))이 되어 검사가 그대로 통과합니다. 덧셈을 둘째 인자에 대한 되부름으로 정의했다면 같은 코드가 거부되고, 중간에 pz 같은 증명을 끼워 타입을 바꿔 주어야 합니다. 프로그램을 짜는 일과 증명하는 일이 한데 섞이는 것입니다. 또 검사기가 계산을 해야 하므로, 계산이 끝나지 않을 수 있다면 타입 검사 자체가 끝나지 않을 수 있습니다. 의존 타입 언어가 모든 함수가 끝나기를 요구하는 이유입니다. 그런데 정지 문제⁠(halting problem)⁠ 때문에 '끝나는 함수'를 빠짐없이 알아볼 수는 없으니, 구조적 되부름처럼 끝남이 눈에 보이는 모양만 받아들입니다.

역사. 네덜란드의 N. G. 더 브라위언은 1967년 무렵부터 수학 증명을 기계로 검사하는 언어 Automath를 만들며 의존 타입을 썼고, 윌리엄 하워드는 1969년 원고에서 ∀와 ∃까지 대응시키려면 의존 타입이 필요함을 보였습니다. 스웨덴의 페르 마르틴뢰프가 1971년 내놓은 첫 체계에는 모든 타입의 타입 Type이 있었고 Type : Type이 허용되었는데, 지라르가 1972년 이 체계에서 모순을 끌어냈습니다(지라르의 역설⁠, Girard's paradox⁠). '너무 큰 모임'이 모순을 낳는 러셀의 역설⁠(Russell's paradox)⁠ 계열의 역설(정확히는 순서수⁠(ordinal number)⁠ 전체에 관한 부랄리포르티 역설⁠(Burali-Forti paradox)⁠)이 타입의 모습으로 되돌아온 것입니다. 해결책도 러셀의 유형 이론⁠(type theory)⁠을 닮았습니다. 타입의 모임을 층층의 우주 $\mathcal U_0 : \mathcal U_1 : \mathcal U_2 : \cdots$로 나누어, 어떤 우주도 자기 자신의 원소가 되지 않게 합니다. 마르틴뢰프는 1972년 이렇게 고친 체계를 내놓았고 1984년 책 『직관주의⁠(intuitionism)⁠ 타입 이론』으로 정리했습니다. 프랑스의 티에리 코캉과 제라르 위에가 내놓은 구성의 계산(1988년 논문)은 Coq(지금의 Rocq)의 바탕이 되었고, 오늘날 Agda, Idris, Lean이 의존 타입을 씁니다.

흔한 오해. '타입이 값에 의존한다'는 말은 실행 중에 값을 확인한다는 뜻이 아닙니다. head의 타입 안의 n은 변수 그대로 다뤄지고, 모든 검사는 실행 전에 끝납니다. 실행 중에 들어온 리스트의 길이를 미리 모를 때는 Σ 타입으로 '어떤 길이 n과 그 길이의 벡터'를 받은 뒤 n이 0인 경우와 아닌 경우를 나누어 다루면, 검사기가 두 경우 모두 올바른지 확인합니다. 또 의존 타입을 쓴다고 모든 것을 증명해야 하는 것도 아닙니다. 타입을 얼마나 자세히 적을지는 쓰는 사람이 고릅니다. List A라고만 적으면 보통의 언어와 같고, Vec A n이라 적으면 길이까지, '정렬된 벡터'라고 적으면 정렬까지 보증받는 대신 그만큼 증명을 해야 합니다.

이어지는 곳. Π와 Σ가 명제의 '모든'과 '있다'가 되는 것은 커리–하워드 대응을 1차 논리⁠(first-order logic)⁠까지 넓힌 것이고, Σ의 '있다'가 증인을 요구한다는 점은 직관주의 논리의 태도 그대로입니다. 되부르는 증명 pz는 수학적 귀납법이 프로그램으로 모습을 바꾼 것이고, 자연수를 0과 succ로 짓는 방식은 페아노의 공리⁠(axiom)⁠에서 왔습니다. 동일성 타입 a = b의 원소가 정말 refl뿐인지 묻는 데서 호모토피 타입 이론⁠(homotopy type theory)⁠이 시작되고, 이런 체계를 실제로 돌려 증명을 검사하는 도구가 증명 보조기⁠(proof assistant)⁠입니다. 섬유를 세는 그림은 대수적 자료형의 셈을 넓힌 것입니다. 우주를 층으로 나누는 방법은 러셀의 역설을 피하려던 러셀의 유형 이론을 닮았고, 그 흐름 전체는 타입 이론에서 볼 수 있습니다. 모든 함수가 끝나야 한다는 조건은 정지 문제 때문에 보수적으로만 검사할 수 있고, 이런 체계가 스스로의 무모순성⁠(consistency)⁠을 증명할 수 없다는 것은 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠가 말해 줍니다. 명세를 타입에 적는 대신 프로그램 옆에 전조건⁠(precondition)⁠과 후조건⁠(postcondition)⁠을 적어 증명하는 길은 호어 논리⁠(Hoare logic)⁠이고, 귀납적으로 정의한 타입마다 생기는 재귀자⁠(recursor)⁠가 결과의 타입이 입력에 따라 달라지도록 fold를 넓힌 것이라는 점은 시작 대수에서 볼 수 있습니다.