[프언] #14. Let-Polymorphic Type System

Limitation of Our Type System

지금까지 구현한 저희의 Type System은 Polymorphism을 지원하지 않습니다. Polymorphism이란, 프로그램의 특정 부분이 서로 다른 부분에서 다른 Type으로 사용되는 일종의 메커니즘입니다.

let f = proc (x) x in
	if (f (iszero (0))) then (f 11) else (f 22)

위 코드에서 f는 어떤 값을 받아 그 값을 그대로 리턴하는 프로시져입니다. 두 번째 줄에서, ITE (If Then Else)의 조건부에 f (iszero (0))이 들어갔는데 이때 f는 Bool을 입력받아 Bool을 출력하는 프로시져입니다. 그러나 다음에 f는 Int를 받아 Int를 출력하는 프로시져로 사용되었죠. 이런 것이 바로 Polymorphism입니다.

그러나 이 코드를 이전 글에서 구현한 알고리즘에 대입하면, proc (x) x 부분에서 아래와 같은 Type Equation이 도출됩니다.

그리고 프로시져 f가 Call 될 때를 생각해 봅시다. f (iszero (0)) 에서, 저희 알고리즘은 f의 Type을 Bool → Bool로 추측할 것입니다. 그리고 그다음 Call인 f 11에서, 알고리즘은 f의 Type을 Int → Int로 추측하겠죠. 따라서, 알고리즘은 Type Error가 발생한다고 추측할 겁니다. 실제로 위 코드는 잘 작동하는데 말이죠.

 

Type Checking After Substitution

이 문제점을 해결하기 위해서, Type Checking 전에 한 가지 수를 쓸 겁니다.

if ((proc (x) x) (iszero (0)))
then ((proc (x) x) 11) else ((proc (x) x) 22)

위 코드는 아까 봤던 코드와 정확히 동일하게 작동하며, 작동 원리도 완벽하게 같습니다. 그러나 위 프로그램에 대해 Type Checking 알고리즘을 적용하면 Type Checking이 올바르게 작동합니다. 각각의 프로시져가 전부 구분되어 있기 때문에, 서로 다른 Type을 가질 수 있기 때문이죠.

원래 저희는 Let에 대한 Typing Rule을 아래와 같이 사용했었습니다.

이걸 아래와 같이 살짝만 변형해 보겠습니다.

($ [x\mapsto E_1]E_2$는 $E_2$ 안에 있는 $E_1$을 전부 $x$로 교체한 Expression을 의미합니다.)

위 Typing Rule에 맞게 Type Equation Generator의 알고리즘도 아래와 같이 수정해 줍니다.

 

Another Limitation

하지만 이 방법 역시 문제가 있습니다. 

let f = true + 1 in 5

이런 코드의 경우 f = true + 1을 5에 대입해 버리면 코드가 사라지기 때문에 Type Checker가 오류를 검사하지 못합니다. 그래서 Type Rule을 다시 바꿔줍니다.

이렇게 $E_2$에 있는 $E_1$을 $x$로 교체할 뿐만 아니라, $E_1$의 타입까지 한번 검사해 줌으로써 문제를 해결할 수 있습니다.

 

또 다른 문제점은 불필요하게 연산이 너무 늘어난다는 것인데요.

let a = <complex code> in
let b = a + a in
let c = b + b in
let d = c + a in ...

이렇게 코드가 작성되면 <complex code>가 코드 내부에 아주 많이 등장하게 되고, 이는 비효율을 만들어냅니다. 이 문제를 해결하기 위해 조금 다른 Type Checking 알고리즘을 사용해야 합니다.

(이 문제에 대한 해결법은 추후 추가하겠습니다)

 

감사합니다.

---

이 글은 컴퓨터공학과 학부생이 개인 공부 목적으로 작성한 글이므로, 부정확하거나 틀린 내용이 있을 수 있으니 참고용으로만 봐주시면 좋겠습니다. 레퍼런스 및 글에 대한 기본적인 정보는 이 글을 참고해 주세요.