힌들리-밀너 타입 시스템

람다 대수에 매개변수 다형성 (Parametric Polymorphism)을 구현한 전형적인 타입 시스템이다. J. Roger Hindley에 의해 처음 연구되었고 이후에 Robin Milner에 의해 재발견되었다. Luis Damas가 나중에 박사 학위 논문에서 증명했다.

HM의 뛰어난 성질 중 놀라운 점은 완전성(completeness)과 가장 일반적인 타입 (Most General Type; 또는 Principal Type이라고 함)을 프로그래머의 도움(타입 어노테이션) 없이 추론할 수 있는 능력이다. 알고리즘 W를 통해 실제로 효율적인 타입 추론 방법을 구현할 수 있으며 이론적으로는 높은 복잡도를 갖고 있지만 아주 큰 코드베이스에서도 잘 동작한다. HM은 함수형 언어에서 자주 사용된다. HM은 ML 프로그래밍 언어의 타입 시스템의 일부로 최초 구현되었다. 그 이후로 하스켈의 타입 클래스처럼 다양한 방법으로 확장되었다.

소개

타입 추론 방법으로써, HM은 타입이 전혀 적혀있지 않은 프로그램의 변수, 표현식, 함수의 타입을 추론(연역; deduce)할 수 있다. 범위에 민감하기 때문에, 소스 코드의 작은 부분의 타입을 추론하는 것에 한정되지 않고 완전한 프로그램이나 모듈에서 추론하는 것도 가능하다. 또한 매개변수 타입에 대응할 수 있기 때문에, 수많은 함수형 프로그래밍 언어의 타입 시스템의 핵심이다.

단순 타입 람다 대수를 위한 타입 추론 알고리즘의 기원은 1958년 Haskell Curry와 Robert Feys까지 거슬러 간다. 1969년에는 J. Roger Hindley가 이 타입 추론이 항상 가장 일반적인 타입(프린시펄 타입)을 추론한다는 것을 증명한다. 1978년에는 Robin Milner가 Hindley의 작업과는 독립적으로 동일한 알고리즘인 알고리즘 W를 만들었다. 1982년에 Luis Damas는 마침내 밀너의 알고리즘이 완전하다는 것을 증명하고 이를 확장하여 다형성을 추가하였다.

단형성과 다형성

단순 타입 람다 대수에서는 타입 T는 하나의 원자 타입 상수이거나 T -> T 형태의 함수 타입이다. 이런 타입을 단형성(monomorphic)이라고 한다. 산술 계산에 사용된 타입이 대표적이다.

3        : Number
add 3 4  : Number
add      : Number -> Number -> Number

이와 반대로, 타입이 없는 람다 대수는 완전히 타입 중립적이고 많은 함수들이 모든 타입의 아규먼트에 유효하게 적용될 수 있다. 항등 함수(Identity function)가 대표적이다.

id = \x. x

다형성(polymorphism)이란 일반적으로 어떤 연산이 하나 이상의 타입의 값을 받아들인다는 뜻인데, 위 예시의 다형성에서는 매개변수화 되어 있다. 단어 뜻 그대로 타입 스킴(Type Schemes)이라는 용어를 쓰기도 하는데, 다형성의 매개변수적 특성을 강조한다. 추가적으로 상수는 양화된(Quantified) 타입 변수와 함께 타입되기도 한다.

cons :  forall a. a -> List a -> a
nil  :  forall a. List a
id   :  forall a. a -> a

다형 타입은 타입 변수의 일관적인 대입을 통해 단형 타입이 될 수도 있다. 단형 인스턴스의 예시는 다음과 같다.

id'  : String -> String
nil' : List Number

좀더 일반적으로, 타입은 타입 변수를 포함하고 있을 때 다형성을 가지고, 그렇지 않으면 단형성을 갖는다.

단형 타입만을 지원하는 파스칼이나 C에서 사용된 타입 시스템과는 반대로, HM은 매개변수 다형성을 위해 태어났다. C++와 같은 이후에 나온 언어는 다른 형태의 다형성에 집중하고 있는데 객체 지향 프로그래밍에서의 서브 타이핑과 오버로딩이다. 서브 타이핑은 HM과 호환될 수 없는 반면, 오버로딩의 변종들은 하스켈의 HM 기반 타입 시스템에서 사용할 수 있다.

Let-다형성

단순 타입 람다 대수를 위한 타입 추론을 다형성을 갖도록 확장할 때, 언제 값의 인스턴스를 추론해야 하는지를 정의해야 한다. 이상적으로는 묶인(bound) 변수는 모두 허용되어야 할 것 같다.

(\ id. .... (id 3)  .... (id "text") ...  ) (\ x. x)

안타깝지만, 다형 타입 람다 대수에서의 타입 추론은 결정 불가능(Undecidable)이다. 대신, HM은 다음과 같은 형태의 Let-다형성을 제공한다.

let id = \ x. x
  in ... (id 3) ... (id "text") ...

문법의 표현식을 확장해서 변수가 묶이는 메커니즘을 제한한다. 오직 let 생성자로 묶인 값만이 인스턴스화의 대상이 되는데, 이것이 곧 다형성이며, 람다 추상화 안의 매개변수는 단형성으로 취급된다.

힌들리-밀너 타입 시스템

타입 시스템은 표현식, 타입 등에 대한 언어를 수정하는 문법 규칙을 통해 형식적으로(formally) 설명할 수 있다. 여기서는 너무 형식적으로 설명하진 않는다. 그 후 타입 규칙을 통해 어떻게 표현식과 타입이 연관되는지를 정의한다.

문법

타입될 표현식은 람다 대수를 let 표현식으로 확장한 것과 정확히 일치한다. 괄호는 표현식의 모호함을 해결하는데 쓰인다. 함수 적용은 왼쪽부터 묶이며 추상화나 let 생성자보다 우선순위가 높다.

e = x                    variable
  | e1 e2                application
  | \x. e                abstraction
  | let x = e1 in e2     let-binding

타입은 문법적으로 모노 타입과 폴리 타입으로 나뉘어진다.

모노 타입

모노 타입은 항상 구체적인 타입을 지정한다. 모노 타입 t는 문법적으로는 터미널로 표현된다.

모노 타입의 예시는 타입 상수인 int나 string, 그리고 매개변수화 타입인 Map (Set string) int 등이 있다. 후자의 타입은 타입 함수의 적용의 한 예시로, 집합 \(\{Map^2, Set^1, string^0, int^0, \rightarrow^2\}\) (윗첨자는 타입 매개변수의 개수를 뜻함)의 원소이다. 타입 함수 C의 완전한 집합은 HM에서 반드시 함수 타입인 \(\rightarrow^2\)를 포함해야 한다는 것만 빼면 임의로 만들 수 있다. 예를 들면 정수를 문자열로 맵핑하는 함수는 int -> string 타입을 갖는다. 여기서도 괄호를 이용해서 타입 표현식의 모호함을 없앨 수 있다. 타입 함수의 적용은 중위 화살표 연산자 ->보다 우선 순위가 높으므로 우측부터 묶인다.

타입 변수는 모노 타입으로 취급된다. 모노 타입을 단형 타입과 헷갈릴 수 있는데, 단형 타입은 타입 변수가 없고 오직 터미널만 허용한다.

두 모노 타입이 동일한 터미널을 가지면 같다.

폴리 타입

폴리 타입, 또는 타입 스킴은 0개 이상의 보편 양화사(Universal Quantifier, \(\forall\))를 통해 묶인 타입 변수를 포함하는 타입이다. 예를 들면 \(\forall a. a \rightarrow a\)과 같이.

폴리 타입 \(\forall a. a \rightarrow a\)을 갖는 함수는, 같은 타입을 갖는 모든 값을 스스로에게 맵핑할 수 있고, 항등 함수가 이 타입을 갖는다.

또 다른 예시로, \(\forall a. (Set\,a) \rightarrow int\) 는 모든 타입의 유한 집합을 받아서 정수로 맵핑하는 함수의 타입이다. 집합의 기수를 계산하는 함수가 이 타입을 갖는다.

양화사는 오직 최상위 레벨에서만 나타날 수 있다. 예를 들어, 타입 \(\forall a. a \rightarrow \forall a. a\) 는 제외된다. 또한 정의에 따라 모노 타입은 폴리 타입에 포함되는데, 따라서 타입은 일반적인 형태인 \(\forall a_1. ... \forall a_n. \tau, n \ge 0\)를 갖는다. 이때 \(\tau\)는 모노 타입이다.

폴리 타입의 동일함은 양화의 순서와 양화된 변수의 이름을 바꾸는(알파 변환) 일에 달려 있다. 게다가 모노 타입에 나타나지 않는 양화된 변수는 버릴 수 있다.

컨텍스트와 타이핑

여전히 서로소인 두 부분을 의미있게 합칠려면, 세 번째 부분이 필요하다: 바로 컨텍스트이다. 문법적으로, 컨텍스트는 x: a 쌍의 리스트로, 대입, 가정, 또는 바인딩이라고 부른다. 각각의 쌍이 뜻하는 것은 값의 변수 x는 타입 a를 갖는다는 것이다. 여기까지 세 가지 부분을 합치면 타이핑 판단이라는 것을 할 수 있는데, \(\Gamma \vdash e: a\)의 형태이며, 이는 “어떤 가정 \(\Gamma\) 하에 표현식 e는 타입 a를 갖는다”를 말한다.

자유 타입 변수

타입 \(\forall a_1. ... \forall a_n. \tau\) 에서, 심볼 \(\forall\)은 타입 변수 \(a_i\)를 모노 타입 \(\tau\) 에 묶는(바인딩) 양화사이다. 변수 \(a_i\) 는 양화되었다고 하며, \(\tau\) 안에서 등장하는 모든 양화된 타입 변수는 묶였다(bound)고 하고, \(\tau\) 안에 묶이지 않은 모든 타입 변수는 자유롭다(free)고 한다. 폴리 타입에서의 양화사 \(\forall\)과 더불어 타입 변수는 컨텍스트를 통해서도 묶일 수 있다. 이런 변수는 타입 상수처럼 행동한다. 마지막으로, 타입 변수는 타이핑 도중에 안묶여도 괜찮은데, 이런 경우 암묵적으로 모두 양화된 것으로 본다.

묶인 타입 변수와 안묶인(자유) 타입 변수의 존재는 프로그래밍 언어에서는 흔하지 않다. 때때로 모든 타입 변수는 암묵적으로 모두 양화된 것으로 취급된다. 예를 들면, 프롤로그에서는 자유 변수가 있는 클로즈는 없다. 하스켈에서처럼, 모든 타입 변수는 암묵적으로 양화되어 등장하는데, 즉 하스켈 타입 a -> a는 \(\forall a. a \rightarrow a\)를 뜻한다.