다형성과 시스템 F(Polymorphism and System F)

리스트를 뒤집는 함수⁠(function)⁠ reverse를 생각해 봅시다. [3, 1, 4]를 넣으면 [4, 1, 3]이, ["가", "나"]를 넣으면 ["나", "가"]가 나옵니다. 원소⁠(element)⁠가 정수⁠(integer)⁠이든 글자이든 코드는 한 글자도 다르지 않습니다. 원소를 들여다보지 않고 자리만 옮기기 때문입니다. 단순 타입 람다 계산⁠(simply typed lambda calculus)⁠에서는 이런 함수에 타입 하나를 줄 수 없어서, 정수용 reverse와 글자용 reverse를 따로 써야 합니다. 이 함수의 참된 타입은 $\forall X.\,\mathrm{List}\,X\to\mathrm{List}\,X$, 곧 '어떤 타입 X를 주든 X의 리스트를 받아 X의 리스트를 돌려준다'입니다. 한 프로그램이 모든 타입에서 같은 방식으로 일하는 성질을 매개변수 다형성⁠(parametric polymorphism)⁠이라 하고, Java와 C#의 제네릭, Rust, Haskell, ML이 모두 이것을 씁니다.

이것을 계산 체계로 다듬은 것이 시스템 F입니다. 프랑스 논리학자 장이브 지라르는 1972년 2차 산술의 증명을 연구하다가, 미국의 존 레이놀즈는 1974년 프로그래밍 언어를 연구하다가, 서로 모르고 같은 체계에 이르렀습니다. 단순 타입 람다 계산에 타입 변수 X와 타입 $\forall X.\,T$, 그리고 규칙 두 개를 더합니다. $\Lambda X.\,t$는 '타입 X를 받아 t를 돌려주는 것'이고, $t\,[A]$는 거기에 타입 A를 넘기는 것입니다.

$$\frac{\Gamma \vdash t : T \qquad X \text{ 가 } \Gamma \text{ 에 자유롭게 나오지 않음}}{\Gamma \vdash \Lambda X.\,t : \forall X.\,T}\qquad\qquad \frac{\Gamma \vdash t : \forall X.\,T}{\Gamma \vdash t\,[A] : T[X := A]}$$

예를 들어 $\mathit{id} = \Lambda X.\,\lambda x{:}X.\,x$의 타입은 $\forall X.\,X\to X$이고, $\mathit{id}\,[\mathrm{Int}]\,3 = 3$입니다. 첫 규칙의 조건은, t가 X에 대해 아무것도 가정하지 않았을 때만 '모든 X'라고 말할 수 있다는 뜻입니다. 시스템 F⁠(System F)⁠에서는 X 자리에 ∀가 붙은 타입까지 넣을 수 있습니다(비술어성⁠, impredicativity⁠). id에 자기 자신의 타입을 넘긴 $\mathit{id}\,[\forall X.\,X\to X]\,\mathit{id}$에도 타입이 붙습니다. ∀만 있으면 자연수⁠(natural number)⁠, 참·거짓, 쌍, 리스트를 따로 넣지 않아도 모두 타입으로 정의되고, 비술어성 덕분에 그렇게 정의한 타입끼리 자유롭게 섞어 쓸 수 있습니다. 자연수의 타입은 $\forall X.\,(X\to X)\to X\to X$이고, 그 원소가 람다 계산⁠(lambda calculus)⁠의 처치 수입니다. 그런데도 지라르는 시스템 F의 모든 항이 계산을 끝낸다(강정규화⁠, strong normalization⁠)는 것을 증명했고, 시스템 F로 정의할 수 있는 자연수 함수가 정확히 2차 산술에서 '모든 입력에 값이 있다'고 증명할 수 있는 계산 가능한 함수라는 것도 보였습니다. 이것은 매우 넓은 범위여서, 원시 재귀⁠(recursion)⁠가 아닌 아커만 함수도 들어갑니다. 대가는 타입 추론입니다. 타입을 적지 않은 식의 시스템 F 타입을 찾는 문제는 판정 불가능하고(조 웰스, 1994), 그래서 실용 언어는 힌들리–밀너처럼 다형성⁠(polymorphism)⁠을 제한하거나 프로그래머에게 타입을 적게 합니다.

타입이 프로그램을 센다. 타입이 $\forall X.\,X\to X$인 함수는 몇 개나 될까요? 이 함수는 X가 무엇인지 모릅니다. X의 값을 새로 만들 수도, 받은 값을 들여다볼 수도 없습니다. 손에 있는 X는 받은 값 하나뿐이니 그것을 돌려주는 수밖에 없습니다. 그래서 (끝나는 순수한 프로그램 가운데, 계산해서 같아지는 것을 같게 보면) 이 타입의 함수는 항등 함수 하나뿐입니다. 같은 이유로 $\forall X.\,X\to X\to X$에는 '첫째를 돌려주기'와 '둘째를 돌려주기' 둘만 있는데, 이것이 처치의 참과 거짓입니다. $\forall X.\,(X\to X)\to X\to X$에는 'f를 n번 적용하기'가 n = 0, 1, 2, …마다 하나씩, 곧 자연수만큼 있습니다. 모르는 타입 X는 제약이면서 보증입니다. 함수가 할 수 있는 일이 줄어들수록 타입만 보고 알 수 있는 것이 늘어납니다.

매개변수성⁠(parametricity)⁠과 공짜 정리⁠(free theorem)⁠. 레이놀즈는 1983년 이 직관을 정리로 만들었습니다(추상화 정리⁠, abstraction theorem⁠). 다형 함수를 두 타입 A와 B에서 쓸 때, A의 원소와 B의 원소 사이에 어떤 관계를 잡든 관계된 입력은 관계된 출력으로 간다는 것입니다. 1989년 필립 와들러는 여기서 타입만 보고 정리를 뽑아내는 방법을 보이고, 이를 '공짜 정리'(Theorems for free!)라 불렀습니다. 예를 들어 r의 타입이 $\forall X.\,\mathrm{List}\,X\to\mathrm{List}\,X$이면, r이 무슨 코드이든 모든 함수 $f : A\to B$와 모든 리스트 xs에 대해 다음이 성립합니다.

$$\mathrm{map}\,f\,(r\,xs) \:=\: r\,(\mathrm{map}\,f\,xs)$$

원소를 먼저 f로 바꾸고 r을 하든, r을 먼저 하고 원소를 바꾸든 같습니다. r은 리스트의 길이만 보고 어느 자리를 남기고 버리고 되풀이할지 정할 수 있을 뿐, 원소의 값에 따라 행동을 바꿀 수 없기 때문입니다. 증명의 뼈대는 한 줄입니다. A와 B 사이의 관계로 'b = f(a)'를 잡으면, 두 리스트가 원소별로 관계된다는 것은 둘째가 첫째에 map f를 한 것이라는 뜻입니다. 추상화 정리는 r의 두 출력도 그렇게 관계된다고 말해 주고, 그것이 위의 등식입니다. 같은 방법으로 $\forall X.\,X\to X$의 함수 g가 항등 함수뿐임도 증명됩니다. 원소가 하나(∗)뿐인 타입과 A 사이에 '∗와 a만 잇는' 관계를 잡으면, g는 ∗를 ∗로 보낼 수밖에 없으므로 g(a)도 ∗와 이어져야 하고, 곧 g(a) = a입니다.

r은 , f는 입니다.

그림의 네모는 범주론⁠(category theory)⁠의 말로 하면 자연성⁠(naturality)⁠ 사각형입니다. List는 타입 A를 List A로, 함수 f를 map f로 보내는 함자⁠(functor)⁠이고, 공짜 정리는 다형 함수 r이 함자 List에서 List로 가는 자연 변환⁠(natural transformation)⁠이라는 말과 같습니다. 정렬처럼 원소를 비교하는 함수는 타입이 $\mathrm{List}\,\mathrm{Int}\to\mathrm{List}\,\mathrm{Int}$일 뿐 모든 X에 대한 함수가 아니어서 이 정리를 누리지 못합니다. 그림에서 r을 '정렬하기'로, f를 x mod 3으로 두면 두 길이 어긋납니다. f를 x²로 바꾸면 두 길이 맞지만, 그것은 x²가 0 이상의 수에서 크기 순서를 지키기 때문이지 타입이 보증한 것이 아닙니다. 공짜 정리는 모든 f에 대해 성립한다는 주장이므로, 몇몇 f에서 맞는 것으로는 부족합니다. 또 공짜 정리가 그대로 성립하는 것은 모든 계산이 끝나는 순수한 언어에서입니다. Haskell에는 끝나지 않는 값과 seq 같은 연산이 있어 'f가 엄격해야 한다' 같은 조건이 붙고, Java처럼 실행 중에 값의 실제 타입을 물어볼 수 있는(instanceof) 언어에서는 '제네릭' 메서드도 X의 값을 들여다보고 행동을 바꿀 수 있어 매개변수성이 깨집니다.

다형성의 세 갈래. 영국의 크리스토퍼 스트레이치는 1967년 강의 노트에서 매개변수 다형성과 임시(ad hoc) 다형성을 나누었습니다. 임시 다형성⁠(ad hoc polymorphism)⁠은 + 하나가 정수에서는 덧셈을, 문자열에서는 이어 붙이기를 하듯 타입마다 다른 코드가 불리는 오버로딩입니다. Haskell의 타입 클래스⁠(type class)⁠는 이것을 규칙 있게 만든 것입니다. 객체 지향 언어의 하위 타입⁠(subtype)⁠ 다형성은 '개는 동물이다'처럼 더 구체적인 타입의 값을 더 일반적인 타입의 자리에 쓰는 것입니다. 이름은 같아도 약속이 다릅니다. 공짜 정리 같은 보증은 '모든 타입에서 같은 코드'라는 매개변수 다형성의 약속에서만 나옵니다.

존재 타입⁠(existential type)⁠과 논리. ∀의 짝은 ∃입니다. $\exists X.\,T$의 값은 어떤 타입 X와 T의 값을 묶되 X가 무엇인지는 숨긴 꾸러미입니다. 예를 들어 $\exists X.\,X\times(X\to X)\times(X\to\mathrm{Int})$는 '처음 상태, 하나 늘리기, 읽기'를 가진 계수기인데, 쓰는 쪽은 속이 정수인지 리스트인지 알 수 없고 알 필요도 없습니다. 1985년 존 미첼과 고든 플롯킨은 이것을 '추상 자료형⁠(abstract data type)⁠은 존재 타입을 가진다'는 말로 정리했습니다. 시스템 F에서는 ∃도 ∀로 정의됩니다: $\exists X.\,T \:=\: \forall Y.\,(\forall X.\,T\to Y)\to Y$. 커리–하워드 대응⁠(Curry–Howard correspondence)⁠으로 보면 시스템 F는 명제 변수에 '모든'을 붙일 수 있는 2차 명제 논리⁠(propositional logic)⁠의 직관주의⁠(intuitionism)⁠ 판본이고, 위 정의는 'T인 X가 있다'가 '어떤 Y든, 모든 X에 대해 T이면 Y라면, Y이다'와 같다는 논리 법칙입니다.

이어지는 곳. 다형성의 출발점인 타입 규칙은 단순 타입 람다 계산에 있고, 실용 언어가 ∀를 어디까지 허용하고 어떻게 저절로 찾아 주는지는 힌들리–밀너 타입 추론⁠(type inference)⁠에서 이어집니다. 처치 수⁠(Church numeral)⁠와 처치의 참·거짓이 시스템 F에서 비로소 제 타입을 얻는다는 점에서 람다 계산과 다시 만납니다. 공짜 정리의 네모는 자연 변환의 정의 그 자체이고, map이 항등과 합성을 지킨다는 성질이 List를 함자로 만듭니다. 리스트 같은 타입을 1 + X × L처럼 세는 방법은 대수적 자료형⁠(algebraic data type)⁠에서 다룹니다. ∀가 타입뿐 아니라 값까지 받을 수 있게 하면 의존 타입⁠(dependent type)⁠이 되고, 거기서 ∀는 명제의 '모든'이 됩니다. 지라르는 타입의 타입을 허용하면(Type : Type) 체계가 모순이 된다는 것도 보였는데, 이것은 러셀의 역설⁠(Russell's paradox)⁠과 같은 계열의 '너무 큰 모임' 역설이 타입 이론⁠(type theory)⁠에서 다시 나타난 것입니다. 시스템 F의 강정규화는 2차 산술의 무모순성⁠(consistency)⁠을 함축하므로, 괴델의 불완전성 정리⁠(Gödel's incompleteness theorems)⁠에 따라 2차 산술 안에서는 증명할 수 없습니다. 타입 변수에 상한⁠(upper bound)⁠을 두는 한정 양화⁠(bounded quantification)⁠ $\forall X\le T$를 더한 F_<:에서는 하위 타입 판정조차 결정할 수 없게 되고(하위 타입과 변성⁠(variance)⁠), 시스템 F를 만든 지라르는 1987년 자원을 한 번씩만 쓰는 선형 논리⁠(linear logic)⁠를 내놓았습니다.