과제6. 정적 타입 시스템 구현하기

제출방법 : 작성한 프로젝트를 ‘{학번}’라는 이름으로 저장한 후 압축하여 Uclass 과제 게시판에 업로드해주세요. 채점은 스크립트로 자동으로 이루어지기에 폴더 이름이 잘못되어서 채점되지 못하면 0점을 받게 됩니다.
- 예시: 학번이 202448015인 학생은 다음과 같은 프로젝트를 202448015.zip으로 압축해서 제출해야 합니다.
```
  202448015
  ├── dune-project
  └── src
      ├── ast.ml
      ├── dune
      ├── interpreter.ml
      ├── lexer.mll
      ├── parser.mly
      ***└── type.ml***
```
제출기한 : 6월 13일 금요일 11:59pm

과제 진행 시 어려운 점이 있으면 Ed Discussion 게시판을 이용해 질문하세요. 게시판을 통해 하기 어려운 질문이라면 아래 TA 이메일을 통해 문의하시기 바랍니다.

TA 이메일: seongminkim16@gmail.com

이번 과제에서는 정적 타입 시스템을 공부하고 구현합니다.

개요

지금까지 프로그래밍 언어의 실행 의미를 정의하고 실행기를 구현했습니다. 이번 과제에서는 프로그램을 실행시키지 않고 프로그램의 실행 의미를 예측하는 방안을 구현합니다. 일반적으로 정적 프로그램 분석(static program analysis) 또는 정적 분석(static analysis)이라 불리는 기술입니다. 정적 분석의 여러 갈래 중에서 정적 타입 시스템(static type system)의 원리를 이해하고 구현해봅니다. 타입 시스템(type system)이란 어떤 표현식(expression)이 타입 오류(ill-typed)인지 혹은 올바른 타입(well-typed)인지, 그리고 올바른 타입이라면 그 표현식의 타입이 무엇인지를 결정하는 방법에 대한 수학적인 설명입니다. 타입 체커(type checker)는 이러한 타입 시스템을 구현한 프로그램으로 해당 언어의 정적 의미론(static semantics)을 구현한 프로그램이라고 할 수 있습니다. 정적 타입 시스템의 목표는 타입 오류를 가지는 프로그램을 실행 전에 미리 모두 걸러내는 것입니다. 정적 타입 시스템은 타입 오류를 자동으로 모두 찾아 줌으로써 안전한 프로그램을 쉽게 개발할 수 있게합니다. 정적 타입 시스템이 장착된 언어에서 프로그램은 아래와 같이 실행됩니다.

예를 들어 다음의 프로그램들은 모두 타입 오류를 가지고 있고 타입 체커에 의해 걸러져야 합니다.

let x = 2 <= 3 in x + 3
if 3 then 88 else 99
(fun x -> (3 x)) 1

타입 정의

먼저 타입을 정의합니다. 타입은 특정 값들의 집합을 의미합니다. 타입이란 프로그램에서 사용되는 값들을 종류별로 요약(abstraction)한 것으로 모든 정수들의 집합 int, 집합 {true, false}를 뜻하는 bool, 그리고 type1에서 type2로 가는 모든 함수들의 집합type1 → type2등이 존재합니다. 함수 타입의 몇 가지 예를 보겠습니다.

int → int: 정수를 입력으로 받아서 정수를 반환하는 함수들의 집합

fun n -> (n + 1)
fun n -> (let x = 1 in x + n)

bool → int: 부울 값을 입력으로 받아서 정수를 반환하는 함수들의 집합

fun b -> (if b then 0 else 1)

int → (int → bool): 정수를 입력으로 받아서 int → bool 타입의 함수를 반환하는 함수들의 집합

fun n -> (fun m -> m <= n)

타입 환경

식 e의 타입은 e에 속한 자유 변수들의 타입을 알아야 결정할 수 있습니다. 예를 들어 x + 1의 타입은 변수 x의 타입이 int일 경우에는 int지만 다른 경우에는 정의되지 않습니다. 그렇기에 일반적으로 타입 시스템은 $\Gamma \vdash e: \tau$라는 3항 관계(ternary relation)으로 표현됩니다. 이 식의 의미는 정적 환경(static environment) $\Gamma$에서 표현식 $e$가 타입 $\tau$를 갖는다는 것입니다. 정적 환경은 타이핑 컨텍스트(typing context)라고도 불리며, 변수에서 타입으로의 매핑입니다. 정적 환경은 어떤 변수가 현재 유효 범위(scope)에 있고 그 변수들의 타입이 무엇인지를 기록하는 데 사용됩니다. 여기서 ⊢ (턴스타일) 기호는 “증명한다(proves)” 또는 “보여준다(shows)”로 읽을 수 있습니다. 즉, ‘정적 환경 Γ는 표현식 e가 타입 τ를 가짐을 보여준다’는 의미가 됩니다.

빈 정적 환경은 {}로 표기하고, x : t는 x가 타입 t에 바인딩(bound)되었음을 의미합니다. 따라서 {foo : int, bar : bool}은 foo가 int 타입을 갖고 bar가 bool 타입을 갖는 정적 환경을 나타냅니다. {x : t}env는 env의 모든 바인딩을 포함하면서 추가로 x를 t에 바인딩하는 정적 환경을 의미합니다. 만약 x가 이미 env에 바인딩되어 있었다면, {x : t}env에서는 x의 이전 바인딩이 새로운 타입 t로의 바인딩으로 대체됩니다. 마지막으로 env(x)는 변수 x가 타입 환경에서 가지는 타입을 의미합니다.

참고로, 타입이 값들의 집합을 의미하듯이 타입 환경은 실행 환경들의 집합을 뜻합니다. 예를 들어 타입 환경 {foo : int, bar : bool} 은 다음과 같이 무한히 많은 실행 환경을 유한하게 요약한 것입니다.

{foo : 0, bar : true}
{foo : 1, bar : true}
{foo : 2, bar : true}
...

이러한 관점에서 정적 타입 시스템을 타입이라고 하는 요약된 값을 가지고 프로그램을 실행시키는 요약 실행기(abstract interpreter)라고 할 수 있습니다. 예를 들어 식 1 + 2에 대한 실제 실행은 3을 계산하지만, 요약 실행은 정수 1과 2를 각각 타입 int로 요약한 후에 타입의 세계에서 덧셈을 수행하며 그 결과를 int로 계산하는 것입니다. 프로그램의 실제 실행 의미를 실행 전에 정확하게 계산하는 것은 불가능하지만 타입으로 요약한 후 계산하는 것은 가능할 수 있습니다.

이 모든 준비 과정을 통해, 드디어 올바른 타입(well-typed)이라는 것이 무엇인지 정의할 수 있게 되었습니다: 정적 환경 env에서 표현식 e가 올바른 타입을 갖는다는 것은 env |- e : t를 만족하는 타입 t가 존재한다는 의미입니다. 따라서 타입 검사기의 목표는 주어진 초기 정적 환경에서 시작하여 이러한 타입 t를 찾아내는 것입니다.

실제 프로그램들은 초기 정적 환경으로 빈 정적 환경을 사용하지 않습니다. 예를 들어 OCaml에서는 Stdlib 모듈 같이 항상 유효 범위에 있는 많은 내장 식별자(built-in identifiers)들이 있습니다. 하지만 이번 과제에서는 초기 정적 환경이 비어있다고 가정하겠습니다.

타입 추론 규칙

타입을 추론하는 규칙들을 정의합니다.

정수 n의 타입은 타입 환경과 상관없이 int입니다.
\[\Gamma \vdash n : \mathtt{int}\]
부울 b의 타입은 타입 환경과 상관없이 bool입니다.
\[\Gamma \vdash b : \mathtt{bool}\]
변수 x의 타입은 타입 환경에 의해 결정됩니다.
\[\Gamma \vdash x : \Gamma(x)\]
이항 연산자는 두 피연산자가 모두 int일때만 정의됩니다.
\[\frac{ \Gamma \vdash E_1 : \mathtt{int} \quad \Gamma \vdash E_2 : \mathtt{int}} {\Gamma \vdash E_1 + E_2 : \mathtt{int}}\] \[\frac{ \Gamma \vdash E_1 : \mathtt{int} \quad \Gamma \vdash E_2 : \mathtt{int}} {\Gamma \vdash E_1 - E_2 : \mathtt{int}}\] \[\frac{ \Gamma \vdash E_1 : \mathtt{int} \quad \Gamma \vdash E_2 : \mathtt{int}} {\Gamma \vdash E_1 * E_2 : \mathtt{int}}\] \[\frac{ \Gamma \vdash E_1 : \mathtt{int} \quad \Gamma \vdash E_2 : \mathtt{int}} {\Gamma \vdash E_1 / E_2 : \mathtt{int}}\] \[\frac{ \Gamma \vdash E_1 : \mathtt{int} \quad \Gamma \vdash E_2 : \mathtt{int}} {\Gamma \vdash E_1 <= E_2 : \mathtt{bool}}\]
if 표현식은 guard의 타입이 bool이고 then branch와 else branch의 타입이 같을 때만 정의됩니다.
\[\frac{\Gamma \vdash E_1 : \mathtt{bool} \quad \Gamma \vdash E_2 : t \quad \Gamma \vdash E_3 : t}{\Gamma \vdash \mathtt{if}~E_1~\mathtt{then}~E_2~\mathtt{else}~E_3 : t}\]
let x = e1 in e2의 타입은 현재 환경 env에서 e1의 타입이 t1이고 {x → t1}env에서 e2의 타입이 t2일 때, t2가 됩니다.
\[\frac{\Gamma \vdash E_1 : t_1 \quad [x \mapsto t_1]\Gamma \vdash E_2 : t_2}{\Gamma \vdash \mathtt{let}~x = E_1~\mathtt{in}~E_2 : t_2}\]
함수 호출식 e1 e2의 경우 e1이 t1 → t2 꼴의 함수 타입이고 e2가 t1 타입을 가질때 t2의 타입을 가집니다.
\[\frac{\Gamma \vdash E_1 : t_1 \rightarrow t_2 \quad \Gamma \vdash E_2 : t_1}{\Gamma \vdash E_1~E_2 : t_2}\]
함수 정의식 fun x → e의 경우 x의 타입이 t1이라고 가정하고 e의 타입이 t2일 때, t1 → t2 타입을 가집니다.
\[\frac{[x \mapsto t_1]\Gamma \vdash E : t_2}{\Gamma \vdash \mathtt{fun}~x \rightarrow~E : t_1 \rightarrow t_2}\]
재귀 함수 정의식 let rec f x = e1 in e2의 경우 다음과 같이 정의됩니다. 재귀 함수의 인자와 결과 타입을 각각 t2, t1이라고 하고 인자 x의 타입을 t2라고 가정한 상황에서 함수의 몸통식 e1의 타입을 t1으로 추론할 수 있다고 할때, 그러한 t1, t2에 대해서 f가 t2 → t1 타입임을 가정한 후 e2의 타입을 t로 추론할 수 있다고 하면, 전체식의 타입을 t로 결론지을 수 있습니다.
\[\frac{ [x \mapsto t_2, f \mapsto (t_2 \rightarrow t_1)]\Gamma \vdash E_1 : t_1 \quad [f \mapsto (t_2 \rightarrow t_1)]\Gamma \vdash E_2 : t}{ \Gamma \vdash \mathtt{let\ rec}~f~x = E_1~\mathtt{in}~E_2 : t}\]

타입 체커는 입력으로 주어진 프로그램 e가 추론 규칙에 의해서 어떤 타입 t를 가질 수 있는지를 분석합니다. 즉 {} ⊢ e : t 의 증명을 시도합니다. 이게 가능하다면, 프로그램 e의 타입이 t이고 타입 오류가 없다고 할 수 있습니다. 이 사실을 추론하는 데 실패한다면 타입 체커는 e가 타입을 가질 수 없고 타입 오류가 있을 수 있다고 결론 짓고 실행을 거부합니다. 이러한 관점에서 타입 체커는 프로그램 e가 주어졌을 때, 증명을 시도하는 자동 증명기(automatic theorem prover)라 할 수 있습니다.

지금까지 디자인한 타입 추론 규칙의 특징을 살펴보겠습니다.

타입 추론은 유일하지 않다.

프로그램 e가 주어졌을 때 위 규칙에 의해 결정되는 타입은 유일하지 않을 수 있습니다. fun x → x는 무한히 많은 타입이 가능합니다. 임의의 타입 t에 대해서 t → t 꼴의 타입이면 가능하다고 할 수 있습니다.
타입 추론은 안전(sound)하다.

즉, 타입 오류가 있는 프로그램은 절대로 타입이 추론되지 않고 프로그램이 실행되지 않습니다. 만약, 프로그램이 실행되었다면 절대 타입 오류가 발생하지 않습니다.
타입 추론은 완전(complete)하지 않다.

우리가 디자인한 타입 시스템은 안전하지만 완전하지는 않습니다(incomplete). 타입 오류 없이 잘 도는 프로그램이지만 타입을 추론하지 못 하는 경우가 있습니다. 표현력이 완전한 (Turing-complete) 일반적인 프로그래밍 언어를 대상으로 안전하고 완전한 정적 타입 시스템을 설계하는 것은 불가능합니다.

타입 체커 구현 방안

위에서 정의한 타입 추론 규칙에 따라, 타입 체커는 해당 규칙들을 재귀 함수 형태로 구현함으로써 구성될 수 있습니다. 이 방식은 실행기 구현 방식과 유사한 접근입니다. 대부분의 케이스에 대해서는 재귀 함수로 추론 규칙을 구현할 수 있지만 함수 정의 규칙에서 문제가 발생합니다. 그것은 함수의 인자 x의 타입을 알아낼 방법이 없다는 것입니다.

\[\frac{[x \mapsto t_1]\Gamma \vdash E : t_2}{\Gamma \vdash \mathtt{fun}~x \rightarrow~E : t_1 \rightarrow t_2}\]

재귀 함수에서도 똑같은 문제가 발생합니다. 함수의 인자 x와 함수 f의 타입을 알 수 없는 문제가 있습니다.

\[\frac{ [x \mapsto t_2, f \mapsto (t_2 \rightarrow t_1)]\Gamma \vdash E_1 : t_1 \quad [f \mapsto (t_2 \rightarrow t_1)]\Gamma \vdash E_2 : t}{ \Gamma \vdash \mathtt{let\ rec}~f~x = E_1~\mathtt{in}~E_2 : t}\]

이 문제를 해결하는 방안은 두 가지가 존재합니다.

타입 추론을 프로그래머에게 맡기는 방식

C, C++, 그리고 Java처럼 함수의 타입과 인자의 타입을 명시적으로 작성해주어야 하는 방식입니다. 이 경우에 우리는 문법을 다음과 같이 수정해야 합니다.
```
     | fun (x : t1) -> e
     | let rec t1 f (x : t2) = e1 in e2
```
알고리즘을 통해서 자동으로 타입을 추론하는 방식

OCaml, Haskell 등의 언어에서 사용하는 방식입니다. 이런 언어에서는 함수 타입을 생략해도 타입 시스템이 자동으로 적절한 타입을 추론해줍니다.

자동 타입 추론 알고리즘

주어진 프로그램으로부터 타입 방정식을 생성하고 이를 풀어 함수의 인자 및 결과 타입을 추론하는 알고리즘을 작성해봅시다.

타입 방정식 생성

첫 단계에서는 프로그램의 각 부분식과 변수들에 대해서 타입 변수를 도입하고 이들이 만족해야 하는 조건을 방적식으로 표현합니다. 예를 들어 아래 프로그램을 생각해봅시다.

\[\text{fun}\ f \rightarrow \text{fun}\ x \rightarrow ((f\ x)\ +\ (f\ 1))\]

프로그램의 각 부분식과 변수들에 대해서 다음과 같이 타입 변수를 도입합니다.

예를 들어, $t_f$는 변수 $f$의 타입을 뜻하는 타입 변수이고, $t_0$는 전체 프로그램의 타입을 뜻하는 타입 변수입니다. 이와 같이 각 부분식과 변수들에 대하여 타입 변수들을 도입한 후에 이들이 만족해야 하는 조건들을 찾습니다. 타입 변수들이 만족해야 하는 조건은 타입 추론 규칙으로부터 얻어집니다. 위의 프로그램은 함수 정의식이고 인자의 타입을 $t_f$, 결과 타입을 $t_1$이라고 하였으므로 타입 변수 $t_0, t_1, t_f$ 사이에 다음과 같은 관계가 성립해야 합니다.

\[t_0 = t_f \rightarrow t_1\]

비슷하게 $t_1, t_x, t_2$ 사이에 다음과 같은 관계가 성립해야 합니다.

\[t_1 = t_x \rightarrow t_2\]

또한 식 $((f\ x) + (f\ 1))$이 타입을 가지기 위해서는 그 타입이 $int$이어야 하고, 부분식 $(f\ 3)$와 $(f\ x)$가 모두 $int$ 타입이어야 합니다. 이를 방정식으로 표현하면 다음과 같습니다.

\[t_2 = int, \quad t_3 = int, \quad t_4 = int\]

또한 함수 호출식 $(f\ 1)$을 보면 $f$가 함수 타입을 가져야 하고 그 인자 타입이 $int$, 결과 타입이 $t_4$여야 함을 알 수 있습니다.

\[t_f = int \rightarrow t_4\]

마지막으로 함수 호출식 $(f\ x)$에 의하면 $t_f, t_x, t_3$ 사이에 다음과 같은 관계가 성립합니다.

\[t_f = t_x \rightarrow t_3\]

지금까지 생성한 제약 조건들을 모두 모으면 다음과 같은 연립 방정식이 됩니다. 이때 타입 변수와 방정식의 개수가 동일하므로 해가 존재한다면 모든 타입 변수들의 값을 결정할 수 있습니다.

타입 방정식

\[t_0 = t_f \rightarrow t_1\\ t_1 = t_x \rightarrow t_2\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow t_4\\ t_f = t_x \rightarrow t_3\\\]

타입 방정식의 해

\[t_0 = (int \rightarrow int) \rightarrow (int \rightarrow int)\\ t_1 = int \rightarrow int\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow int\\ t_x = int\]

타입 방정식 생성 알고리즘

앞서 정의한 타입 정의에 타입 변수를 추가합니다.

\[\begin{array}{rl}T \;\; \rightarrow & \texttt{int} \\ | & \texttt{bool} \\ | & T \rightarrow T \\ | & \alpha \quad (\in TyVar)\end{array}\]

타입 방정식은 다음과 같이 정의합니다. 두 타입이 같음을 의미하는 방정식들이 and로 연결되어 있습니다.

\[\begin{align*}TyEqn &\rightarrow \emptyset \\ &\mid T_1 = T_2 \land TyEqn\end{align*}\]

이제 프로그램으로부터 방정식을 도출하는 알고리즘을 정의합니다. 이 알고리즘은 세 가지 인자를 받습니다. 표현식 $e$가 환경 $\Gamma$에서 타입 $t$를 가지기 위해서 성립해야 하는 조건들을 생성합니다.

\[\mathcal{V}(\Gamma,e,t)\]

타입 방정식 생성 알고리즘을 재귀적으로 정의하면 다음과 같습니다.

$\mathcal{V}(\Gamma, n, t) = t \doteq \textit{int}$; 어떤 환경에서든 정수 $n$이 타입 $t$를 가지려면 $t$가 $int$여야 합니다.
$\mathcal{V}(\Gamma, b, t) = t \doteq \textit{bool}$; 어떤 환경에서든 부울 $b$가 타입 $t$를 가지려면 $t$가 $bool$여야 합니다.
$\mathcal{V}(\Gamma, x, t) = t \doteq \Gamma(x)$; 타입 환경 $\Gamma$에서 변수 $x$가 타입 $t$를 가지려면 $t$가 $\Gamma(x)$와 같아야 합니다.
이항 연산자 표현식이 타입 $t$를 가지기 위해서는 피연산자가 모두 $int$타입이여야 하고 타입 $t$가 연산 결과 타입과 같아야 합니다.
\[\mathcal{V}(\Gamma, e_1 + e_2, t) = t \doteq \textit{int} \land \mathcal{V}(\Gamma, e_1, \textit{int}) \land \mathcal{V}(\Gamma, e_2, \textit{int})\\ \mathcal{V}(\Gamma, e_1 - e_2, t) = t \doteq \textit{int} \land \mathcal{V}(\Gamma, e_1, \textit{int}) \land \mathcal{V}(\Gamma, e_2, \textit{int})\\ \mathcal{V}(\Gamma, e_1 * e_2, t) = t \doteq \textit{int} \land \mathcal{V}(\Gamma, e_1, \textit{int}) \land \mathcal{V}(\Gamma, e_2, \textit{int})\\ \mathcal{V}(\Gamma, e_1 / e_2, t) = t \doteq \textit{int} \land \mathcal{V}(\Gamma, e_1, \textit{int}) \land \mathcal{V}(\Gamma, e_2, \textit{int})\\ \mathcal{V}(\Gamma, e_1 <= e_2, t) = t \doteq \textit{bool} \land \mathcal{V}(\Gamma, e_1, \textit{int}) \land \mathcal{V}(\Gamma, e_2, \textit{int})\\\]
조건식의 경우에는 guard의 타입이 $bool$이어야 하고 then branch와 else branch의 타입이 $t$로 같아야 합니다.
\[\mathcal{V}(\Gamma, \textit{if } e_1\text{ then } e_2\text{ else } e_3, t) = \mathcal{V}(\Gamma, e_1, \textit{bool}) \land \mathcal{V}(\Gamma, e_2, t) \land \mathcal{V}(\Gamma, e_3, t)\]
l$et$식은 먼저 식 $e_1$에 대해서 새로운 타입 변수를 생성하여 마지막 인자로 줍니다. 재귀적으로 이 새로운 타입 변수가 만족해야 하는 조건들을 생성할 것입니다. 그 다음 현재 타입 환경을 확장하여 식 $e_2$가 전체 식의 타입 $t$와 같도록 하는 조건을 생성합니다.
\[\mathcal{V}(\Gamma, \textit{let } x = e_1 \textit{ in } e_2, t) = \mathcal{V}(\Gamma, e_1, \alpha) \land \mathcal{V}([x \mapsto \alpha]\Gamma, e_2, t)\]
함수 정의식은 $e$가 함수 타입을 가져야 합니다. 이때, 함수의 인자와 결과 타입이 만족해야 하는 조건이 없으므로 새로운 타입 변수들을 생성합니다.
\[\mathcal{V}(\Gamma, \textit{fun } x \rightarrow\ e, t) = t \doteq \alpha_1 \to \alpha_2 \land \mathcal{V}([x \mapsto \alpha_1]\Gamma, e, \alpha_2)\]
재귀 함수 정의식은 재귀 함수의 타입과 인자의 타입을 만족하는 조건이 없으므로 새로운 타입 변수들을 생성합니다.
\[\mathcal{V}(\Gamma, \textit{let rec } f\ x = e_1 \textit{ in } e_2, t) = t_f \doteq \alpha_1 \to \alpha_2 \land \mathcal{V}([f \mapsto t_f, x \mapsto \alpha_1]\Gamma, e_1, \alpha_2) \land \mathcal{V}([f \mapsto t_f]\Gamma, e_2, t)\]
함수 호출식은 e_1이 함수 타입이어야 하기에 새로운 타입 변수를 도입합니다.

\[\mathcal{V}(\Gamma, e_1\ e_2, t) = \mathcal{V}(\Gamma, e_1, \alpha \to t) \land \mathcal{V}(\Gamma, e_2, \alpha)\]

타입 방정식 풀이

이제 앞서 세운 타입 방정식의 해를 구하는 과정을 살펴봅니다. 아래 프로그램을 예로 설명합니다.

\[\underbrace{\text{fun}\ \underbrace{f}_{t_f} \rightarrow \underbrace{\text{fun}\ \underbrace{x}_{t_x} \rightarrow \underbrace{(\underbrace{(f\ x)}_{t_3}\ +\ \underbrace{(f\ 1))}_{t_4}}_{t_2}}_{t_1}}_{t_0}\] \[t_0 = t_f \rightarrow t_1\\ t_1 = t_x \rightarrow t_2\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow t_4\\ t_f = t_x \rightarrow t_3\\\]

타입 방정식의 해를 치환(substitution)이라고도 부르는데 해의 왼쪽에 있는 타입 변수를 오른쪽의 타입으로 치환해주는 함수로 볼 수 있기 때문입니다. 그러한 함수를 타입 방정식의 각 타입 변수에 적용하면 각 방정식의 왼쪽, 오른쪽 항들이 동일해집니다. 예를 들어 $t_0 = t_f \rightarrow t_1$에서 각 타입 변수를 해로 치환하면 ($int \rightarrow int) \rightarrow (int \rightarrow int) = (int \rightarrow int) \rightarrow (int \rightarrow int)$로 양변이 같아집니다. 그렇기에 타입 방정식의 해를 구하는 알고리즘을 동일화 알고리즘(unification algorithm)이라고 부릅니다. 동일화 알고리즘은 빈 치환($\emptyset$)에서 시작하여 각 방정식을 순차적으로 치환으로 옮기는 방식으로 동작합니다.

먼저 가장 상단의 방정식을 치환으로 옮깁니다.

방정식

\[t_1 = t_x \rightarrow t_2\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow t_4\\ t_f = t_x \rightarrow t_3\\\]

치환

\[t_0 = t_f \rightarrow t_1\]

두번째 방정식을 옮깁니다. 이때, 옮겨지는 방정식의 왼쪽에 해당하는 변수가 치환에 존재하는 경우 그 변수들을 방정식의 오른쪽으로 변경합니다.

방정식

\[t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow t_4\\ t_f = t_x \rightarrow t_3\\\]

치환

\[t_0 = t_f \rightarrow (t_x \rightarrow t_2)\\ t_1 = t_x \rightarrow t_2\\\]

동일한 방식으로 나머지 방정식들도 모두 치환으로 옮겨줍니다. 이때, $t_2, t_3, t_4$를 옮긴 상태는 다음과 같습니다.

방정식

\[t_f = int \rightarrow t_4\\ t_f = t_x \rightarrow t_3\\\]

치환

\[t_0 = t_f \rightarrow (t_x \rightarrow int)\\ t_1 = t_x \rightarrow int\\ t_2 = int\\ t_3 = int\\ t_4 = int\\\]

이때, 옮기려는 방정식에 치환에 해가 존재하는 타입 변수가 존재합니다. 이때는 그 변수를 해로 바꾼 상태로 옮깁니다.

방정식

\[t_f = t_x \rightarrow t_3\\\]

치환

\[t_0 = (int \rightarrow int) \rightarrow (t_x \rightarrow int)\\ t_1 = t_x \rightarrow int\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow int\]

이제 남은 방정식을 처리하기 위해 먼저 치환을 적용하면 방정식이 다음과 같이 변경됩니다.

\[int \rightarrow int = t_x \rightarrow int\]

이와 같이 방정식의 왼쪽과 오른쪽이 모두 변수가 아닌 경우에는 방정식을 쪼갭니다. 양쪽이 모두 함수 타입이고 이 둘이 서로 같으려면 두 인자의 타입과 결과 타입이 각각 같아야 합니다. 쪼갠 방정식은 다음과 같습니다.

\[t_x = int\\ int = int\\\]

마지막 방정식은 당연히 항상 성립하는 경우이기에 무시하고 이 방정식을 치환으로 옮기면 최종적으로 다음과 같은 치환을 얻어냅니다. 전체 프로그램의 타입뿐만 아니라 모든 부분식과 변수들의 타입이 추론되어 있음을 볼 수 있습니다.

\[t_0 = (int \rightarrow int) \rightarrow (int \rightarrow int)\\ t_1 = int \rightarrow int\\ t_2 = int\\ t_3 = int\\ t_4 = int\\ t_f = int \rightarrow int\\ t_x = int\]

타입 방정식 풀이 알고리즘

타입 방정식의 해를 구하는 과정을 기술하면 다음과 같습니다. 타입 방정식에 있는 개별 방정식에 대해 아래 과정을 거쳐 치환으로 옮기는 작업을 반복합니다.

먼저 현재 치환을 방정식에 적용하여 이미 알고 있는 타입 변수의 내용을 갱신합니다.
그 결과 현재 방정식이 $int = int$와 같이 항상 성립하는 꼴이 된다면, 이를 무시하고 다음 방정식으로 넘어갑니다.
그렇지 않고 $bool = int$와 같이 모순이 생긴 경우에는 타입 추론에 실패하는 경우이므로 알고리즘을 종료합니다.
현재 방정식의 양쪽항이 $int \rightarrow t_1 = t_2 \rightarrow bool$과 같이 모두 변수가 아닌 경우, 어느 한쪽 항이 변수가 될 때까지 방정식을 간략화 시킵니다.
만약 왼쪽항이 변수가 아니면 양쪽항을 바꿉니다.
만약 왼쪽항의 변수가 오른쪽에 등장하면 타입 추론에 실패하고 알고리즘을 종료합니다.
그렇지 않은 경우, 현재 방정식을 치환으로 옮기고 치환에 존재하는 방정식의 왼쪽에 해당하는 변수를 오른쪽 항으로 바꿉니다.

이제 위 과정을 정확하게 알고리즘으로 기술합니다. 치환은 타입 변수에서 타입으로 가는 함수로 정의합니다. 치환 $S$를 타입에 적용하는 과정은 다음과 같이 귀납적으로 정의됩니다.

\[\begin{align*}S(\text{int}) &= \text{int} \\S(\text{bool}) &= \text{bool} \\S(\alpha) &= \begin{cases}t & \text{if } \alpha \mapsto t \in S \\\alpha & \text{otherwise}\end{cases} \\S(T_1 \to T_2) &= S(T_1) \to S(T_2)\end{align*}\]

이제 하나의 타입 방정식을 치환으로 옮기는 함수인 unify를 정의합니다. $\text{unify}(T_1, T_2, S)$는 방정식 $T_1 = T_2$를 처리하여 치환 $S$로 옮깁니다.

\[\begin{align*} \text{unify}(\text{int}, \text{int}, S) &= S \\ \text{unify}(\text{bool}, \text{bool}, S) &= S \\ \text{unify}(\alpha, \alpha, S) &= S \\ \text{unify}(\alpha, t, S) &= \begin{cases} \text{fail} & \text{if } \alpha \text{ occurs in } t \\ \text{extend } S \text{ with } \alpha \doteq t & \text{otherwise} \end{cases} \\ \text{unify}(t, \alpha, S) &= \text{unify}(\alpha, t, S) \\ \text{unify}(t_1 \to t_2, t_1' \to t_2', S) &= \text{let } S' = \text{unify}(t_1, t_1', S) \text{ in} \\ &\quad \text{let } S'' = \text{unify}(S' (t_2), S' (t_2'), S') \text{ in} \\ &\quad S'' \\ \text{unify}(-,-,-) &= \text{fail} \end{align*}\]

$\text{unify}(\alpha \rightarrow \beta, int \rightarrow \alpha, \emptyset) = {\alpha \rightarrow int, \beta \rightarrow int}$와 같은 경우를 처리하기 위해서 $\text{unify}(t_1 \to t_2, t_1’ \to t_2’, S)$를 처리할 때, $t_2$와 $t_2’$에 대해서 $S’$을 먼저 적용합니다.

타입 방정식 전체를 받아서 해를 구하는 함수를 unify_all이라고 정의합니다.

\[\begin{align*} \textbf{unify\_all}(\emptyset, S) &= S \\ \textbf{unify\_all}((t_1 = t_2) \land u, S) &= \text{let } S' = \textbf{unify}(S(t_1), S(t_2), S) \\ &\quad \text{in } \textbf{unify\_all}(u, S') \end{align*}\]

이제 이 unify_all 함수를 빈 치환과 함께 사용하면 방정식을 입력 받아서 해를 계산할 수 있습니다.

\[\mathcal{U}(u) = \textbf{unify\_all}(u, \emptyset)\]

최종 타입 추론 알고리즘

이제 타입 방정식 생성 알고리즘과 타입 방정식 풀이 알고리즘을 활용하여 타입 체킹 알고리즘 typecheck를 정의할 수 있습니다. 먼저 새로운 타입 변수를 생성하고 이를 주어진 프로그램의 타입으로 가정한 후에 방정식을 생성한 후에 이를 풉니다. 방정식이 풀리는 경우 치환이 구해지고 이 치환에서 가정한 타입 변수의 타입을 찾아 반환할 수 있습니다.

\[\begin{align*}\text{typecheck}(E) =\ & \text{let } S = \mathcal{U}(\mathcal{V}(\emptyset, E, \alpha)) \text{ in } S(\alpha)\end{align*}\]

다형 타입 시스템 (참고)

우리가 정의한 최종적인 타입 시스템은 단순 타입 시스템(simple type system)입니다. 단순 타입 시스템은 OCaml 등의 언어에서 실제로 쓰이는 타입 시스템에 비해서 정교함이 떨어지는데, 주된 차이점은 다형 타입(polymorphic type)을 지원하지 않는다는 것입니다. 예를 들어 아래 프로그램은 타입 오류가 없지만 우리가 정의한 타입 시스템은 받아들이지 못하고 OCaml의 타입 시스템은 받아들입니다.

let f = fun x -> x in if f (1 <= 2) then (f 1) else (f 2)

let f = fun x → x 부분에 대해서 $t_f = t_x \to t_x$와 같은 타입 방정식이 생성됩니다. 함수의 인자 타입과 결과 타입이 같아야 하는 제약이 생성됩니다. 직관적으로 이러한 제약 조건하에서 위의 프로그램은 타입 체크가 되어야 합니다. $f$가 사용될 때마다 위의 제약 조건을 지키면서 전체 프로그램이 타입을 가지도록 할 수 있기 때문입니다. 첫번째 함수 호출식에서는 $t_f = bool \to bool$이라고 하고 두 번째와 세 번째 호출식에서는 $t_f = int \to int$라고 하면 제약 조건이 만족되기 때문입니다. 그럼에도 불구하고 단순 타입 시스템은 타입 추론에 실패하는 데, 단순 타입 시스템은 $f$가 동일한 타입 변수 $t_x$를 공유하기 때문입니다. 이 문제를 해결하는 자연스러운 방법은 $f$가 사용되는 서로 다른 지점마다 새로운 타입 변수를 도입하는 것입니다. 이와 같이 서로 다른 함수 호출 지점을 구별하는 방식을 정적 분석에서 일반적으로 문맥 구분 분석(context sensitive analysis)라고 부르며, 타입 시스템의 경우에는 다형 타입 시스템(polymorphic type system)이라고 부릅니다. OCaml에서 사용하는 타입 시스템은 let 다형 타입 시스템(let-polymorphic type system)이라 부르는 것으로 let식에 의해 정의되는 함수만 다형 함수로 일반화합니다.

구현

정적 타입 시스템 구현을 위해 type.ml 파일을 새로 작성합니다. 타입 추론과 관련된 함수들은 파싱된 프로그램의 AST를 기반으로 동작하기 때문에, 파일 상단에 Ast 모듈을 open 하여 AST 타입들을 사용할 수 있도록 합니다.

open Ast

이제 타입에 대한 타입을 정의합니다.

type typ =
  | TyInt
  | TyBool
  | TyFun of typ * typ
  | TyVar of tyvar
and tyvar = string

추가로 타입 변수들을 동적으로 생성하기 위하여 타입 변수 생성기를 정의합니다. fresh_tyvar () 와 같이 호출하여 새로운 타입 변수를 생성할 수 있습니다.

let tyvar_num = ref 0
let fresh_tyvar () = (tyvar_num := !tyvar_num + 1; TyVar ("t" ^ string_of_int !tyvar_num))

변수, 타입 환경, 치환, 타입 방정식에 대한 타입을 정의합니다.

type var = string
type type_env = (var * typ) list
type subst = (tyvar * typ) list
type typ_eqn = (typ * typ) list

치환을 구현합니다.

let rec apply_subst x = function
  | [] -> TyVar x
  | (y, t) :: tl -> if x = y then t else apply_subst x tl

let rec substitute typ subst =
  match typ with
  | TyInt -> TyInt
  | TyBool -> TyBool
  | TyFun (t1, t2) -> TyFun (substitute t1 subst, substitute t2 subst)
  | TyVar x ->
      let t' = apply_subst x subst in
      if t' = TyVar x then t'
      else substitute t' subst

타입 변수가 특정 타입 안에 존재하는지 검사하는 헬퍼 함수를 정의합니다. 이는 아래 규칙을 확인하기 위해서 필요합니다.

이는 만약 왼쪽항의 변수가 오른쪽에 등장하면 타입 추론에 실패하고 알고리즘을 종료합니다.

let rec occurs x t =
  match t with
  | TyInt | TyBool -> false
  | TyVar y -> x = y
  | TyFun (t1, t2) -> occurs x t1 || occurs x t2

이제 타입 방정식을 생성하는 함수를 작성합니다.

let rec gen_equations tenv expr typ =
(*
	함수를 작성하세요.
*)

이 타입 방정식을 푸는 동일화 알고리즘을 작성합니다.

let rec unify eqns =
(*
	함수를 작성하세요.
*)

과제 (hw6)

gen_equations와 unify 함수를 완성하면 최종적인 typecheck 함수를 완성할 수 있습니다.

let typecheck s =
  let lexbuf = Lexing.from_string s in
    let ast = Parser.prog Lexer.read lexbuf in
      let new_type_var = fresh_tyvar () in
        let eqns = gen_equations [] ast new_type_var in
          let subst = unify eqns in
            substitute new_type_var subst