[PL] Type Unification

🌳 Type Unification

type varaible t1, t2가 있을 때, type을 추론하기 위한 방법중 하나가 'type unification'이다.

common type을 찾을 수 있다.
type unification은 compliation process에 일어나며, type error을 일찍 발견함으로써 runtime error을 방지한다.

1) 주어진 타입 t1, t2에 대하여 먼저 이를 resolve한다.

2) 몇 가지 possible cases가 존재한다.

possibility (1) 이중 최소한 하나는 type variable이다.
t1이 type variable이다. or t2가 type variable이다. or 둘 다 type variable이다.
possibility (2) 둘 다 type variable이 아니다.

🌳 3가지 케이스

1) t1이 type variable T이다.

a. 만약 t2가 T이면, SUCCEED.

둘 다 T이므로 Common Type을 찾은 것!
예시) x y
함수호출문이므로 x는 arrow type(function type)이다.
x가 T는 T -> Num 타입이다. y는 T타입이다.
=> Unify T AND T => SUCCEED

b. If T occurs in t2, fail.

예시) x x (x:T)
Function Call 인데, T와 T->T'를 Resolve할 수 없다.

c. Otherwise, set T to t2 and succeed.

예시) x + 1 (x:T)
1은 NUM 타입이다. Unify T and NUM -> T= NUM, and succeed.

2) t2이 type variable T이다.

위와 동일하다.

3) 둘 다 type variable이 아니다.

a. If both are num, succeed.

둘다 num이라면, succeed이다.

b. If 𝜏1 is 𝜏3 —> 𝜏4 and 𝜏2 is 𝜏5 —> 𝜏6 , unify 𝜏3 with 𝜏5 ,and unify 𝜏4 with 𝜏6

이렇게 unify하기 위해서는 t3, t5와 t4, t6이 각각 같은 파라미터 타입인지 확인해야 한다.

c. Otherwise, fail.