[프언] #13. Automatic Type Inference

2023-2학기/프로그래밍언어

[프언] #13. Automatic Type Inference

AlriC 2023. 12. 10. 02:29

지난 글에서 Type Checker를 구현하는 과정에서, Proc Expression을 단순 Recursion으로 구현할 수 없는 문제가 있었습니다. 그 문제를 해결하기 위해 프로시져를 정의할 때, 프로시져에 들어가는 인수의 Type을 미리 지정하는 방식인 Type Annotation을 사용했었고요. 이번 글에서는 다른 방식인 Type Inference를 이용해 이 문제를 해결해보도록 하겠습니다.

Automatic?

Type Annotation은 프로그래머가 필요한 Type을 직접 지정하도록 하는 방식이었다면, Type Inference는 알려지지 않은 Type을 프로그램이 자동으로 추리해 내는 방식입니다.

Examples of Type Inference

if x then x-1 else 0

위와 같은 코드가 있다고 가정합시다. 코드라고 말했지만 이 코드는 사실 큰 ITE (If Then Else) Expression과 같습니다. 저희는 이 큰 ITE Expression의 Type을 알아내는게 목적이겠죠. 저희가 알아내고자 하는 Type을 $t_0$라고 정의하겠습니다.

ITE Expression에서 저희는 조건문, 그러니까 If 다음에 들어가는 Exprssion은 Bool이라는 사실을 알고 있습니다. If 다음에 오는 Expression은 x이죠. 근데 아직 저희는 x의 Type을 모르기 때문에 이를 $t_x$라고 하겠습니다. 그러면, $t_x=bool$ 라고 적을 수 있습니다.

그다음으로 Then과 Else 다음에 들어가는 Expression은 전체 Expression의 Type임도 알고 있죠. Then 다음에 오는 Expression은 x-1인데, 저희는 아직 이것의 Type을 모르기 때문에 이를 $t_1$이라고 두겠습니다. 그러면 $t_1=t_0$ 이죠. $t_0$가 Expression 전체의 Type이니깐요.

Else 다음에 들어가는 Expression은 0 역시 $t_0$일텐데, 저희는 0이 Int Type이라는 걸 알고 있죠. 따라서, $int=t_0$ 입니다.

그다음으로는 아직 분해되지 않은 Expression인 x-1을 보겠습니다. Subtraction Expression에서, - 기호 양쪽에 오는 Expression의 Type은 모두 Int여야 합니다. 따라서 $t_x=int$, $t_1=int$ 임을 알 수 있습니다.

지금까지 나온 식들을 전부 나열하면 아래와 같습니다.

$$t_x=bool$$

$$t_1=t_0$$

$$int=t_0$$

$$t_x=int$$

$$t_1=int$$

이런 식들을 Type Equation이라고 합니다. 이제 주어진 프로그램에서 얻을 수 있는 Type Equation을 전부 적고 나면, 이제 이를 전부 만족하는 근이 있는지를 체크해 보면 됩니다.

다들 아시다시피, 첫 번째 식과 네 번째 식은 동시게 참이 될 수 없습니다. 따라서 이 Type Equations를 만족하는 근이 없으므로 Type Error가 발생하게 됩니다.

proc f (f 11)

위 코드도 같은 방법으로 풀어보겠습니다. 먼저 전체 Expression의 Type을 $t_0$로 정의합니다. 이 Expression은 Proc Expression이며 Proc Expression의 Type은 f와 (f 11)에 의해 정해집니다. 저희는 아직 이 두 Expression의 Type을 모르기 때문에, f의 Type을 $t_f$, (f 11)의 Type을 $t_1$이라고 정의해 두겠습니다. 그러면 $t_0=t_f \to t_1$ 입니다.

그리고 (f 11)은 프로시져 f에 11을 넣어 나오는 값을 의미합니다. 11은 Int이고 (f 11)의 Type은 $t_1$이므로 저희는 프로시져 f의 Type이 $int \to t_1$ 임을 알 수 있습니다. 따라서, $t_f=int \to t_1$ 입니다.

위 코드를 통해서는 아래와 같은 Type Equation들을 얻을 수 있었습니다.

$$t_0=t_f \to t_1$$

$$t_f=int \to t_1$$

위 식들을 만족하는 근은 존재할까요? 존재합니다. $t_1$에 대한 조건이 없으므로 아래와 같은 근을 도출할 수 있습니다.

$$\left ( t_0,t_1,t_f \right )=\left ( \left ( int \to t \right ) \to t, t, int \to t \right )\; for \; \forall t \in T$$

따라서 Type Error가 발생하지 않습니다.

이렇게 차근차근 저희가 정의해 왔던 문법을 짚어가며 Type Equation을 도출할 수도 있지만, 각 Expression을 정의할 때 사용했던 Inference Rule을 이용해서 Type Equation을 도출할 수도 있습니다.

한 예시로, 더하기 기호를 정의할 때 위와 같은 형태의 Inference Rule을 사용했었습니다. 위 Inference Rule을 통해 아래와 같은 Type Equation을 만들 수 있습니다.

같은 방식으로, 아래와 같은 관계식을 적을 수 있습니다.

Formalizing Type Inference

각각의 Type Equation들을 나타내는 기호로 $TyEqn$을 사용하겠습니다. 그리고 이 Type Equation들을 만드는 알고리즘을 아래와 같이 정의하겠습니다.

$\nu \left ( \Gamma ,e,t \right )$는 $\Gamma$의 Environment 내부에서 $e$가 Type $t$를 가진다는 것을 의미합니다. 간단한 예시를 들자면, $\nu \left (\left [ x\mapsto int \right ],x+1,\alpha \right) =alpha \doteq int$ 입니다.

이제 이런 식으로 정의된 $\nu$를 통해 Type Equation을 만들어낼 수 있습니다.

이를 이용해 어떤 프로그램이든 Recursive 하게 Type Equation을 얻어낼 수 있습니다. 아래는 간단한 예시입니다.

Solving Type Equations

이제 코드를 보고 Type Equation들을 얻어내는 알고리즘은 만들었으므로, 만들어진 Type Equation을 보고 이를 해결하는 과정이 필요합니다.

proc f proc x ((f 3) - (f x))

위 식을 통해서 아래와 같은 Type Equation들을 얻었다고 생각해 봅시다.

위 Type Equation을 해결하기 위해 다음과 같은 방법을 사용할 겁니다. 먼저 Equation, Substitution 이렇게 2가지 구역을 만든 뒤 모든 Type Equation들을 Equation 영역에 넣습니다.

그리고 이제 Equation 영역에 있는 식들을 하나하나 Substitution으로 넘겨줄 건데요,

일단 첫 번째 식을 Substitution으로 넘기면 이런 모습이 됩니다. 다음으로는 두 번째 식을 옮길 건데요, 옮기는 식의 좌변이 $t_1$이잖아요? 이때 Substitution 영역에 있는 식에 $t_1$이 존재하면, 그걸 $t_x\to t_2$로 바꿔치기해 줍니다.