10. Automatic Type Inference

자동 타입 추론 문제

자동 타입 추론은 주어진 프로그램 E에 대해 가장 일반적인 타입을 추론하는 문제이다. E가 타입을 가질 수 있는 경우 이를 결정하는 타입을 찾아내고, 그렇지 않은 경우에는 타입을 가질 수 없음을 표시한다.

 

자동 타입 추론은 정적 분석(static analysis) 알고리즘으로, 표현식의 사용 방식을 관찰하여 타입을 추론한다. 이 알고리즘은 정확(sound)하고 완전(complete)하다. 즉, 분석이 표현식에 대해 타입을 찾는다면 그 표현식은 잘 타입된 것이고, 표현식이 타입 시스템에 따라 타입을 가지면 분석은 그 타입을 반드시 찾아낸다.

 

이 알고리즘은 아래 두 단계로 구성된다.

 

1. 프로그램 텍스트에서 타입 방정식 생성

2. 방정식 풀이

 

타입 방정식은 각 서브 표현식과 변수에 대해 타입 변수를 도입하고, 이들 타입 변수 사이의 방정식을 유도한다.

 

예를 들어, 위와 같은 표현식이 있을 때, 타입 단위로 위와 같이 t_i 형태로 나눌 수 있다.

 

표현식의 타입을 추론하는 방법은 아래와 같다.

t0 = t_f →  t1

t1 = t_x → t2

t3 = int

t4 = int

t2 = int

t_f = int → t3

t_f = t_x → t4

 

 

각종 표현식에서의 방정식

덧셈 표현식

 

iszero 표현식

 

if-then-else

 

프로시저 호출

 

프로시저 정의

 

let-in 구문

 

 

Type equations

T → int

    | int

    | bool

    | T → T

    | α (∈ Ty Var)

 

여기서 α는 타입 변수(type variables) 이다.

이는 특정 타입에 고정되지 않고 다양한 타입으로 대체될 수 있어, 다형성을 표현할 수 있다.

 

TyEqn → ∅  | T =. T ∧ TyEqn

TyEqn이 ∅라면, 타입 방정식이 비어있음을 뜻한다. 이는 더 이상 해결해야 할 방정식이 없는 경우이다.

T1 = T2 ∧ TyEqn은 두 타입 T1과 T2가 동등하다는 방정식과 추가적인 타입 방정식을 결합한 형태이다.

 

 V(Γ, e, t) = (Var → T) × E × T → TyEqn

이는 타입 환경 Γ, 표현식 E, 표현식 E가 가지기를 원하는 타입 T에서,

Γ ⊢ e : t 가 성립하기 위한 조건을 나타내는 타입 방정식을 생성한다.

 

예시 1. V([x ↦ int], x + 1, α)

- x의 타입은 Γ에서 int로 정의되어 있다.

- 상수 1의 타입은 항상 int이다.

- 덧셈 연산 +의 결과 타입은 두 피연산자가 int일 때 int이다.

- 따라서 타입 방정식은 α = int 이다.

 

예시 2. V(∅, proc(x)(if x then 1 else 2), α → β)

- Γ는 비어있다.

- 상수 1의 타입은 항상 int이다. 또한 2의 타입도 항상 int이다.

- if문의 조건식의 타입은 항상 bool이다. 따라서 x의 타입은 bool이다.

- 따라서 타입 방정식은 α = bool ∧ b = int 이다.

 

Unification Algorithm

타입 방정식을 해결하기 위해선 유니피케이션 알고리즘(일치화 알고리즘)을 사용한다.

이는 각 방정식을 하나씩 처리하고 대입을 통해 타입 변수를 구체적인 타입으로 대체한다.

 

 

다시, 위와 같은 표현식과 타입 방정식과 구체적인 타입으로 대체된 솔루션이 있다. 우리는 좌측에 있는 방정식으로 우측의 솔루션을 만드는 것이 목표이다.

 

방정식과 대입(substitution)칸을 나눈다. 초기 대입 칸은 비어있다.

맨 처음 방정식, t0 = t_f → t1을 대입 칸으로 옮긴다.

 

다음 방정식을 대입 칸으로 옮긴다.

이 때, t1에 대한 정보가 갱신되었으므로 앞서 대입 칸에 있던 우항의 t1 정보를 바꿔준다.

 

위 방식을 반복한다.

또한, 새로운 방정식 t_f = int → t3가 들어올 때 t3에 대한 정보가 대입 칸에 있으므로 이를 대입하고 옮긴다.

 

t_f = t_x → int 가 들어올 때, 먼저 t_f는 int → int이므로 int → int = t_x → int 로 대입된다.

식의 양변이 모두 변수가 아니므로, 두 개의 새로운 식을 산출하여 단순화한다. 즉, int = t_x ∧ int = int로 단순화한다.

따라서 t_x = int 가 된다.

 

 

Occurrence Check

위 표현식에서, 타입 방정식 t_f = t_f → int 는 항상 우항이 더 크다. 따라서 단순화 할 수 없다.

따라서 우리는 해가 없다는 결론을 내려야 한다.

이것을 발생 검사(occurrence check)라고 한다.

 

 

Unification Algorithm

유니피케이션 알고리즘은 다음과 같은 단계로 이루어진다.

 

1. 현재 대입을 방정식에 적용
2. 항상 참인 방정식을 버린다. (ex) int = int
3. 좌변과 우변이 모순되면 알고리즘은 실패한다. (ex) int = bool
4. 양변 모두 변수가 아니라면 방정식을 단순화한다. (ex) int → t1 = t2 → bool  ⇒  int → t2 ∧ t1 → bool
5. 좌변이 변수가 아닌 경우, 좌변과 우변을 바꾼다.
6. 좌변 변수가 우변에 나타나면 알고리즘은 실패한다. (ex) t_x = t_x → int
7. 그렇지 않다면 이를 대입에 추가하고 대입에서 변수의 모든 우변으로 갱신한다.

 

 

Substitution Function

타입 추론에서 타입 방정식의 해는 대입으로 표현된다.

 

S ∈ Subst = TyVar → T

대입 함수는 타입 변수를 타입으로 매핑한다.

 

1. S(int) = int
2. S(bool) = bool
3. S(α) = {t if α ↦ t ∈ S else α}
4. S(T1 → T2) = S(T1) → S(T2)

 

여기서, (t1 → t2) → (t3 → int)는,

⇒ S((t1 → t2) → (t3 → int))

⇒ 4번에 따라, S(S(t1 → t2) → S(t3 → int))

⇒ 4번에 따라, S(S(S(t1) → S(t2)) → S(S(t3) → S(int)))

⇒ 1, 3번에 따라, (int → (int→int)) → (t3 → int)

 

Unification Function

unify : T × T × Subst → Subst

unification 함수는 두 타입과 현재 대입을 받고 대입을 업데이트한다.

 

1. unify(int, int, S) = S, unify(bool, bool, S) = S, unify(α, α, S) = S
2. unify(α, t, S) = fail if (α occurs in t) else [α = t]S
3. unify(t, α, S) = unify(α, t, S) // t에는 타입 변수가 포함되지 않음
4. unify(t1 → t2, t'1 → t'2, S) =
           let S' = unify(t1, t'1, S) in
           let S'' = unify(t2, t'2, S') in S''
5. unify(_, _, _) = fail

 

 

Solving Equations

unifyall : TyEqn → Subst → Subst

unifyall 함수는 주어진 타입 방정식을 순차적으로 처리하고 최종적인 대입을 반환한다.

 

unifyall(∅, S) = S

unifyall((t1 = t2) ∧ v, S) = 
        let S' = unify(S(t1), S(t2), S) 
        in unifyall(u, S')

 

U(v) = unifyall(v, ∅) 으로 최종적인 unification algorithm으로 호출한다.

 

typeof(E) =
    let S = U(V(0, E, a))
    in S(a)

위 typeof 함수로써 표현식 E의 타입을 알 수 있다.

V(∅, E, α)로 E로써 발생하는 타입 방정식의 집합 v을 구하고, U(v)로 unification algorithm으로써 대입되며 도출된 타입의 집합 S를 얻는다. 여기서 α는 E에 대한 타입 방정식이다.

S(α)로, E에 대한 타입을 구한다.