다음 함수에는 타입이 하나도 적혀 있지 않습니다: twice=λf.λx.f(fx). 그래도 사람은 타입을 짐작할 수 있습니다. f가 x에 적용되니 f는 함수여야 합니다. f가 내놓은 값이 다시 f에 들어가니, f가 내놓는 값의 타입은 f가 받는 값의 타입과 같아야 합니다. 그 타입을 α라 하면 x도 α이고, 전체의 타입은 (α→α)→α→α입니다. α에는 정수든 문자열이든 무엇이 와도 됩니다. 이 짐작을 기계가 규칙대로 해내는 것이 타입 추론입니다. ML, OCaml, Haskell, F# 같은 언어에서는 프로그래머가 타입을 거의 적지 않아도 컴파일러(compiler)가 모든 식의 타입을 찾아내고, 맞지 않으면 실행하기 전에 거부합니다. 이들이 쓰는 방법의 뼈대가 힌들리–밀너 타입 체계입니다. 찾아내는 타입은 단순 타입 람다 계산(simply typed lambda calculus)의 타입에 '무엇이든 올 수 있는 자리'인 타입 변수를 더한 것입니다.
방법은 두 단계입니다. 첫째, 타입을 모르는 곳마다 새 타입 변수를 붙이고 등식을 모읍니다. λx에는 새 변수 α를 붙이고, 몸통에서 x가 나오는 곳은 모두 α로 둡니다. λx.M의 타입은 'α → (M의 타입)'이라 등식이 따로 필요 없습니다. 새로 알게 되는 것은 모두 적용 M N에서 나옵니다. M의 타입이 τ, N의 타입이 σ이면, 결과에 새 변수 γ를 주고 등식 τ=σ→γ를 적습니다. 둘째, 모은 등식을 단일화로 풉니다. 단일화는 두 식을 똑같게 만드는 변수 대입을 찾는 일로, 1965년 영국 태생의 미국 철학자 J. A. 로빈슨이 기계로 정리를 증명하는 방법(분해 원리, resolution)의 핵심으로 내놓았습니다. 규칙은 넷입니다. 양쪽이 같으면 지웁니다. 한쪽이 변수 α이면, 아래의 발생 검사(occurs check)를 통과할 때 대입 α := (다른 쪽)을 적고 남은 등식 모두에 적용합니다. 양쪽이 화살표이면 앞끼리, 뒤끼리 같다는 두 등식으로 쪼갭니다. Int와 Bool처럼 모양이 다르면 실패, 곧 타입 오류입니다.
왼쪽은 식의 나무이고, 마디 옆의 타입에는 지금까지의 대입이 적용되어 있습니다. 오른쪽 위는 아직 풀지 않은 등식(노란 것을 다음에 풉니다), 아래는 대입 표입니다. 마디에 마우스를 올리면 그 마디의 역할이 보입니다.
추론할 식은 입니다. 다섯 가지 가운데 마지막 두 식은 타입이 없는 식입니다.
발생 검사. λx.xx를 넣으면 x : α에 대해 등식 α=α→β 하나가 나옵니다. 대입 α := α → β를 적으면 오른쪽의 α도 다시 바뀌어 (α→β)→β가 되고, 또 바뀌고, 끝이 없습니다. 어떤 타입을 넣어도 오른쪽이 왼쪽보다 기호가 많으니, 유한한 타입으로는 이 등식을 만족시킬 수 없습니다. 그래서 단일화는 변수를 대입하기 전에 그 변수가 반대쪽 안에 나오는지 검사하고, 나오면 실패합니다. 이것은 제멋대로 정한 규칙이 아닙니다. 자기 자신에게 적용하기는 람다 계산(lambda calculus)에서 끝나지 않는 계산 Ω = (λx.x x)(λx.x x)와, 되부름을 만드는 Y 조합자(Y combinator)의 씨앗입니다. 타입이 붙는 항은 모두 계산을 끝낸다는 강정규화(strong normalization) 정리가 성립하려면 바로 이 자리에서 막혀야 합니다. 타입을 끝없이 펼쳐 쓰는 것(재귀(recursion) 타입)을 허용하는 선택도 있지만, 그러면 Ω에도 타입이 붙어 정규화 보장이 사라집니다.
가장 일반적인 타입. twice는 (Int→Int)→Int→Int 타입도 가집니다. 하지만 이것은 (α→α)→α→α의 α에 Int를 넣은 것일 뿐입니다. 영국 논리학자 로저 힌들리는 1969년 조합 논리(combinatory logic)에서, 로빈 밀너는 1978년 프로그래밍 언어 ML을 위해 따로, 타입이 붙는 식에는 언제나 이런 주 타입(principal type)이 있음을 보였습니다. 식이 가질 수 있는 모든 타입이 주 타입의 변수에 무언가를 대입해 얻어진다는 뜻입니다. 1982년 밀너와 그의 학생 루이스 다마스는 밀너의 알고리즘(algorithm) W가, 타입이 있는 식에서는 반드시 주 타입을 찾고 없는 식에서는 실패한다는 것(건전성과 완전성)을 증명했습니다. 핵심은 단일화가 찾는 대입이 가장 일반적인 단일화자라는 데 있습니다. 등식을 만족시키는 다른 어떤 대입도, 이 대입을 먼저 한 뒤 무언가를 더 대입한 것입니다. 모든 해가 한 해를 거쳐 간다는 이 모양은 보편 성질(universal property)의 모양이고, 실제로 가장 일반적인 단일화자(most general unifier)는 대입들이 이루는 범주(category)에서 보편 성질로 정의할 수 있습니다. 위 그림은 등식을 먼저 다 모은 뒤 푸는 방식이고, 알고리즘 W는 나무를 훑으면서 모으기와 풀기를 번갈아 합니다. 얻는 답은 같습니다.
let 다형성(let-polymorphism). 힌들리–밀너의 두 번째 기둥은 이름을 붙일 때 타입을 일반화하는 것입니다. let id=λx.x in (id3, idtrue)에서는 id의 타입 α → α를 구한 뒤, α가 주변의 어떤 변수의 타입에도 묶여 있지 않으므로 ∀α.α→α로 일반화해 둡니다. 쓸 때마다 α를 새 변수로 바꿔 끼우므로 첫 번째 id는 Int → Int, 두 번째는 Bool → Bool이 됩니다. 반면 거의 같아 보이는 (λid.(id3, idtrue))(λx.x)는 거부됩니다. λ로 받은 id는 타입 변수 하나 α로만 다뤄지는데, α가 Int이면서 Bool일 수는 없기 때문입니다. 함수의 인자까지 다형적으로 받게 하면 시스템 F(System F)가 되지만, 시스템 F에서 타입을 적지 않은 식의 타입을 찾는 문제는 판정 불가능하다는 것을 1994년 미국의 조 웰스가 증명했습니다. ∀를 let으로 붙인 이름의 맨 바깥에만 허용하는 힌들리–밀너는, 추론이 언제나 결판나는(주 타입을 찾거나 타입이 없다고 알리는) 범위 안에서 다형성(polymorphism)을 넉넉히 들여온 절충입니다.
비용과 한계. 실제 프로그램에서는 추론이 대개 식의 크기에 거의 비례하는 시간에 끝납니다. 최악의 경우는 다릅니다. let x1=(x0,x0) in let x2=(x1,x1) in ⋯처럼 쌍을 겹겹이 만들면 let이 하나 늘 때마다 타입이 두 배로 길어져, 타입을 그대로 적는 데만 기호가 2n개쯤 필요합니다. 1990년 해리 메어슨이, 그리고 따로 아사프 크포우리·예지 티우린·파베우 우르지친이 ML 식에 타입이 있는지 판정하는 문제가 지수 시간 완전(DEXPTIME-완전)임을 보였습니다(이런 문제는 점근 표기로 쓴 어떤 다항식 시간(polynomial time) 안에도 풀 수 없음이 증명되어 있습니다). 또 ML과 Haskell은 let rec로 되부름을 허용합니다. 이것은 타입이 ∀α.(α→α)→α인 고정점(fixed point) 연산자(operator)를 하나 더하는 것과 같아서, 추론은 여전히 되지만 '타입이 붙으면 계산이 끝난다'는 보장은 사라집니다. 밀너가 1978년 논문에 적은 구호 '타입이 맞는 프로그램은 잘못될 수 없다'(Well-typed programs cannot go wrong)에서 '잘못됨'은 정수(integer)를 함수처럼 호출하는 것 같은 타입 오류를 말할 뿐, 무한 루프까지 막는다는 뜻이 아닙니다.
흔한 오해. 타입 추론(type inference)은 동적 타이핑이 아닙니다. 파이썬처럼 실행하면서 값의 종류를 확인하는 방식과 달리, 여기서는 실행하기 전에 모든 식의 타입이 정해지고, 프로그래머가 그것을 적지 않았을 뿐입니다. 또 추론이 언제나 되는 것은 체계를 좁게 잡았기 때문입니다. 연산자 하나가 타입마다 다르게 일하는 오버로딩, 하위 타입(subtype), 인자까지 다형적인 함수, 의존 타입(dependent type)이 들어오면 추론은 일부만 되거나 판정 불가능해지고, 프로그래머가 곳곳에 타입을 적어 주어야 합니다. Haskell은 1989년 필립 와들러와 스티븐 블롯이 내놓은 타입 클래스(type class)로 '덧셈이 되는 타입 a'(Num a) 같은 조건을 힌들리–밀너 위에 얹었습니다. 마지막으로 단일화는 모순이 드러나는 곳에서 멈추므로, 오류가 보고되는 곳이 실제로 잘못 쓴 곳에서 멀 수 있습니다.
이어지는 곳. 추론하는 대상인 타입과 타입 규칙은 단순 타입 람다 계산에 있습니다. twice의 타입 (α→α)→α→α는 람다 계산의 처치 수(Church numeral) 2가 가지는 타입이기도 해서, 두 페이지가 여기서 만납니다. 커리–하워드 대응(Curry–Howard correspondence)으로 읽으면 주 타입을 찾는 일은 '이 프로그램이 증명하는 가장 일반적인 명제'를 찾는 일입니다. 그림에서 λx.λy.λz. x z (y z)의 주 타입 (α→β→γ)→(α→β)→α→γ는 명제 논리(propositional logic)의 공리(axiom) 하나와 글자까지 같습니다. ∀를 let 이름의 바깥에만 붙이는 제한을 풀면 시스템 F로 가고, 거기서 타입만 보고 얻는 공짜 정리(free theorem)가 다형성의 힘을 보여 줍니다. ML은 원래 밀너가 에든버러에서 만든 증명 보조기(proof assistant) LCF의 증명 전술을 적는 언어로 태어났으니, 타입 추론과 증명 검사는 처음부터 한집에서 자랐습니다. 가장 일반적인 단일화자가 모든 해를 거쳐 가게 한다는 성질은 보편 성질의 한 예입니다. 식의 나무 자체는 문맥 자유 문법(context-free grammar)으로 파싱해 얻고, 단일화는 두 나무를 겹쳐 맞추는 알고리즘이라, 발생 검사를 빼먹으면 나무에 되부름하는 고리가 생겨 버립니다. 하위 타입이 끼어들면 같음의 방정식 대신 부등식 X≤Y를 풀어야 해서 가장 일반적인 타입이 깔끔하게 나오지 않는데, 그 어려움은 하위 타입과 변성(variance)에서 이어집니다.