[이중호]

교재 181쪽에 보면

타입 치환 S와 타입틀 sigma에 대해서 S sigma = A b.S{a->b}t 라고 나와있는데요

여기서 뒤쪽에 S{a->b}t의 의미가 무엇인가요

S에 있는 모드 TypeVar a를 새로운 TypeVar b로 바꾸고 t를 치환하라는 뜻인가요?

또, 그 뒤에 b^(itv(S)Uftv(sigma)) = NULL 인 경우라는건 b는 새로운 TypeVar라고 보아도 되는 건지요

[허기홍]

네 맞습니다. 모든 알파를 베타로 바꾸라는 뜻이고

그 베타는 완전히 새로운 놈이라는 뜻입니다.

[이중호]

S sigma = A b.S{a->b}t

예를 들어sigma가 A {a1,a4}. a1 -> a2 -> (a3,a4) 이고

S에 a1=>int, a3=>bool 이라면

S의 a1을 b1으로 치환하고 a4는 S에 없으니 치환하지 않으니까

S{a->b}는 b1=>int, a3 => bool이 되고

이를 a1 -> a2 -> (a3,a4) 에 적용하면 a1 -> a2 -> (bool,a4)

라서 결과값이 S sigma = A {b1,b4}. a1->a2->(bool,a4)가 되는게 아닌지요,,,

a1은,,,,

a1을 b1으로 치환할때 t에서도 같이 치환해 주는것인가요?

그럼 S sigma = A {b1,b4}.int -> a2 -> (bool,b4)가 되는데 이 결과가 맞는것 같네요

그럼 S sigma = A b.S{a->b}t{a->b} 이렇게 써져 있어야 하지 않나요,,,

[허기홍]

아.. 오해의 소지가 있었군요.

그게 아니라

S{어쩌고}t

라고 하면 우선 t를 어쩌고에 적용하고 그 결과를 S에 적용하는 겁니다.

t에 있는 알파 중에 for all에 묶여있는 놈을 다 새로운 베타로 치환한 후
S를 적용하고
for all beta를 붙여줍니다.

이유는 일반화된 타입변수를 보존하기 위하여.
이렇게 하지 않으면 타입이 고정되어버리기 때문에.