0) 기본지식:
* 타입: simply typed lambda calculus에서 가산 무한 정렬 순서 집합 TV가 타입변수들의 집합으로 주어졌을 때 type의 정의는 다음과 같다:
1. TV의 모든 원소는 타입이다.
2. 임의의 타입 sigma, tau에 대하여 sigma → tau는 타입이다.
3. 타입을 구성하는 방법은 이상의 두 가지 방법 밖에 없다.
* 치환: substitution이란 자유변수를 표현식으로 바꾸는 규칙이다.
* 타입문맥: type context란 assumption들의 집합으로 개체변수(term variable)에 타입을 할당하는 규칙이다. 타입문맥 TC 아래에서 항 M에 타입 sigma를 할당할 수 있음을 TC |- M: sigma로 나타낸다.

1) principal type이란?
타입 sigma, tau에 대하여, sigma에 어떤 치환을 취하여 tau를 얻을 수 있을 때, tau를 sigma의 instance라고 한다.
항 M이 주어졌을 때, 다음을 만족하는 타입 sigma를 M의 principal type이라 한다:
임의의 타입 tau에 대하여 tau를 M에 할당할 수 있으면 tau가 sigma의 instance이다.
simply typed lambda calculus에서는 타입을 할당할 수 있는 항의 principal type이 유일하게 존재한다.

2) principal type을 구하는 법:
항 M이 주어졌을 때 M의 princaple type이 Gamma 아래에서 sigma일 때, 타입문맥 Gamma와 타입 sigma를 구하는 방법은 다음과 같다:
alpha를 전에 사용하지 않은 첫 번째 타입변수라 하자.
1. M이 x인 경우: { x: alpha } |- M: alpha.
2. M이 P Q인 경우: TC1 |- P: sigma이고 TC2 |- Q: tau이라면 TC1' union TC2'' |- M: alpha''이다.
이때 sigma' == (tau → alpha)''이고, '와 ''는 치환이며, TC1'과 TC2''는 융합가능하다.
3. M이 lambda x. N인 경우: TC |- N: sigma일 때 TC' - { x: alpha'' } |- M: alpha'' → sigma'이다.
이때 '와 ''는 치환이며, TC'와 { x: alpha'' }는 융합가능하다.
여기서 치환 '과 치환 ''을 구하는 법을 설명하지 않았는데,
설명하기 힘들어서 그런 것이다.
most general unifier를 구하는 법을 이용하면 된다.
솔직히 설명이 개떡 같은데, 더 엄밀하고 자세히 설명할 수 있었다면 코드로 말했을 것이다.

3) 마치며:
더 알고 싶은 사람은 Basic Simple Type Theory라는 책을 보시면 되겠습니다.
구현하고 싶은데 잘 안 되어서 정리를 해봤습니다.