はじめに

本記事は、「QualiArts Advent Calender 2025」の6日目の記事になります。

QualiArtsでバックエンドエンジニアをしています。
今年のGo ConferenceでGoのジェネリクスの言語論的なお話をしたので、せっかくなら言語論で何か書きたいなと思ったので型推論について書こうと思います。

背景

普段何気なく使っている型推論ですが、実際どのようにコンパイラが型を決定しているか気になりませんか？？
型推論の仕組みを理解すれば自作言語に型推論が入れ放題となり幸せになれますし、コンパイラの気持ちもわかってハッピーになれます
今回はみなさんの馴染み深いであろうGo言語(っぽいサブセット)でお話ししようと思います。
ただ、Go言語の型推論は局所的な実装なので、現行のGoの型推論を理解しつつ、それを拡張するにはどんな感じになるのかで見ていきたいと思います。

型推論

まずは型推論についてのおさらいです。
Goでは変数宣言時に型推論を使うことができます。

型推論を使わない場合は以下のようなコードになると思います。

var i int = 10
var s string = "Hello, Gopher"
var m map[string]int = map[string]int{"a": 1, "b": 2}

これに対して、型推論を使った場合は以下のようになると思います。

var i = 10
s := "Hello..."
m := map[string]int{"a": 1}

このように型推論を使うと、型名をわざわざ書く必要がなくなりとてもスッキリしますね。

言語定義

では型推論の中身を見ていきたいと思いますが、そのまえに型推論のお話をする言語の定義をします。
Go言語をそのまま用いると複雑すぎるため、ここでは必要な最小限のGoっぽいサブセットを定義します。

項と型の定義

この言語は、以下の項と型を持ちます。

項

一般的に「式（Expression）」と呼ばれるものです。ここでは $e$ と表記します。

構文	説明
$x$	変数
$n$	整数リテラル
$true, false$	真偽値リテラル
$e + e$	加算
$if \ e \ \{ e \} \ else \ \{ e \}$	if式
$func(x) \ \{ return \ e \}$	関数定義
$e(e)$	関数呼び出し

ポイントは2点あります。

ifが式である: Goのifは「文」ですが、この言語では値を返す「式」として扱います
関数の引数に型がない: func(x int) ではなく func(x) と書きます。この省略された型 int を推論するように拡張します

型

型 $T$ は以下のいずれかの形を取ります。

表記	説明
$int$	整数型
$bool$	真偽値型
$func(T) \ T$	関数型（ $T \to T$ ）
$X$	型変数

ここで重要なのが 「型変数 $X$」 です。
「まだ型がわからないけれど、とりあえず $X$ と置いておこう」みたいな感じのものです。型推論ではこの $X$ が最終的に $int$ なのか $bool$ なのかを特定していく作業といえます。

文脈（Context）

変数の型推論を行う際、変数を見ただけでは、その型はわかりません。そこで、その変数がどのように使われているのかという情報が必要になります。

この情報を持ち回るための入れ物を文脈と呼び、一般的に $\Gamma$で表します。
文脈は「変数名」と「型」のペアとして定義されます。

$$
\Gamma ::= \emptyset \ | \ \Gamma, x:T
$$

$\emptyset$: 空の文脈
$\Gamma, x:T$: 文脈 $\Gamma$ に、変数 $x$ は型 $T$ であるという情報を追加したもの

例えば、x が int で y が bool であるという文脈は以下のようになります。

$$
x: int, \ y: bool
$$

実装上は、map[string]Type のようなデータ構造で管理することになります。
今後の推論規則では、「ある文脈 $\Gamma$ のもとで、式 $e$ が型 $T$ になる」という関係を以下のように記述しようと思います。

$$
\Gamma \vdash e : T
$$

制約型付けの規則

言語の定義ができたら、次は型を推論するルールを作っていきます。

ここでは型を確定させるのではなく、
「$x$ は $y$ と同じ型でなければならない」「$x$ は int でなければならない」といった方程式を作ることが目的です。

ちなみにこのような方程式を 制約型付け と呼びます。

型付け規則の構造

前節までは $\Gamma \vdash e : T$ （文脈 $\Gamma$ のもとで、式 $e$ は型 $T$ になる）という3つ組でした。
しかし、型推論を行うためには、これだけでは情報が足りません。以下の2つを追加して5つに拡張します。

使用済み型変数の集合 ($\mathcal{X}$):
- func(x) が出てくるたびに、「引数の型は $X_1$」「次の引数は $X_2$」...と新しい型変数を発行する必要があります。名前被りを防ぐために、すでに使った変数をメモしておくセット
制約集合 ($C$):
- 「$T_1 = int$」や「$T_1 = T_2$」といった、集めた方程式（等式）のセット

つまり、推論ルールは以下のような形になります。

$$
\Gamma \vdash e : T \mid_{\mathcal{X}} C
$$

読み方としては、
「入力 $\Gamma$ と未使用の変数を使って式 $e$ を解析した結果、型は $T$ っぽくて、使用済み変数は $\mathcal{X}$ に増えて、満たすべき制約 $C$ が見つかった」
という感じです。

それでは、各構文のルールを見ていきます。

リテラル (CT-Int, CT-Bool)

まずは一番簡単なリテラルです。
1 はどうあがいても int ですし、制約も特にありません。

$$
\Gamma \vdash n : int \ \mid_{\emptyset} \{ \}
$$

$$
\Gamma \vdash true : bool \ \mid_{\emptyset} \{ \}
$$

肩: int や bool
使用済み変数: なし ($\emptyset$)
制約: なし ($\{\}$)

変数 (CT-Var)

変数の場合、文脈 $\Gamma$ からその変数の型を探してきます。

$$
\frac{x:T \in \Gamma}{\Gamma \vdash x : T \mid_{\emptyset} \{ \}}
$$

もし文脈にその変数がなければ、宣言されていない変数を使おうとしたことになるのでエラーになります。

加算 (CT-Plus)

ここから推論っぽくなります。足し算 $e_1 + e_2$ です。

足し算ができるということは、以下が確定します。

左辺 $e_1$ の型 $T_1$ は int でなければならない
右辺 $e_2$ の型 $T_2$ は int でなければならない
全体の結果の型も int になる

これを数式にします。

$$
\frac{\Gamma \vdash e_1 : T_1 \mid_{X_1} C_1 \quad \Gamma \vdash e_2 : T_2 \mid_{X_2} C_2}{\Gamma \vdash e_1 + e_2 : int \mid_{X_1 \cup X_2} C_1 \cup C_2 \cup \{ T_1 = int, T_2 = int \}}
$$

再帰的に $e_1, e_2$ を解析して出てきた制約 $C_1, C_2$ に加えて、「$T_1 = int$ かつ $T_2 = int$」という新しい制約 を追加して返すのがポイントです。

if式 (CT-If)

Goのif式 if e_1 { e_2 } else { e_3 } です。
ここでも以下が確定します。

条件式 $e_1$ の型 $T_1$ は bool でなければならない
else 側の型 $T_3$ は、then 側の型 $T_2$ と同じでなければならない
全体の結果の型は $T_2$（あるいは $T_3$）になる

$$
\frac{\Gamma \vdash e_1 : T_1 \dots \quad \Gamma \vdash e_2 : T_2 \dots \quad \Gamma \vdash e_3 : T_3 \dots}{\Gamma \vdash if \ e_1 \ \{ e_2 \} \ else \ \{ e_3 \} : T_2 \mid_{\dots} C_{all} \cup \{T_1 = bool, T_2 = T_3\}}
$$

ここでの成果物は、「$T_1 = bool$」 と 「$T_2 = T_3$」 という制約です。

関数定義 (CT-Abs)

func(x) { return e } という式を考えます。
Goではできない型推論なのでここから拡張になります。

引数 x には型が書かれていません。
そこで、新しい型変数 $X$ を勝手に発行して割り当ててしまいます。
そして、「引数 x は型 $X$ だよ」という情報を文脈に追加して、関数の中身 $e$ を解析します。

$$
\frac{X \notin \mathcal{X} \quad \Gamma, x:X \vdash e : T_{body} \mid_{X} C}{\Gamma \vdash func(x) \ \{ return \ e \} : func(X) \ T_{body} \mid_{X \cup \{X\}} C}
$$

$X \notin \mathcal{X}$: まだ使われていない新しい型変数 $X$ を用意します
型: 結果の型は、引数が $X$ で戻り値が $T_{body}$ なので、$func(X) \ T_{body}$ になります

これで、「引数の型はわからんけど、一旦 $X$ ってことにして中身を見てみよう」という処理ができました。

関数呼び出し (CT-App)

最後は関数呼び出し $e_1(e_2)$ です。

関数部分 $e_1$ の型を $T_1$ とする
引数部分 $e_2$ の型を $T_2$ とする
戻り値の型もわからないので、新しい型変数 $X$ を用意する

このとき成り立たなければならない制約はこれです。
「$T_1$（関数の型）は、『引数が $T_2$ で戻り値が $X$ の関数』と等しくなければならない」

$$
\frac{\Gamma \vdash e_1 : T_1 \mid_{X_1} C_1 \quad \Gamma \vdash e_2 : T_2 \mid_{X_2} C_2}{\Gamma \vdash e_1(e_2) : X \mid_{X_1 \cup X_2 \cup \{X\}} C_1 \cup C_2 \cup \{ T_1 = func(T_2) \ X \}}
$$

これにより、「関数定義側で推論された型」と「呼び出し側で渡している引数の型」が一致するような方程式が作られました！

型を導く

ここまでプログラム全体を走査して大量の「制約」を集めました。
しかし、このままではまだ型推論は完了していません。

例えば、以下のような制約が集まったとします。

$X_1 = func(X_2) \ X_3$ （$X_1$ は何らかの関数である）
$X_1 = func(int) \ bool$ （$X_1$ は int を受け取って bool を返す関数である）

人間が見れば「あ、じゃあ $X_2$ は int で、$X_3$ は bool だな」と分かりますが、これをコンパイラが行う必要があります。
これを 単一化 と呼びます。

単一化のアルゴリズム

単一化とは、制約の集合 $C$ を上から順に処理していき、「型代入」 のリストを作成することです。
型代入とは、「型変数 $X$ を具体的な型 $T$ に置き換えろ」という命令（$[X \mapsto T]$）のことです。

具体的な手順は以下のようになります。制約集合 $C$ から等式 $S = T$ を1つ取り出して、その形によって処理を分岐します。

1. 両辺が同じ型の場合

$$
int = int, \quad X = X
$$

自明なので、何もしなくてOKです。その制約を捨てて次に行きます。
もし $int = bool$ のように矛盾していたら、その時点で型エラーです。

2. 片方が型変数の場合

$$
X = T
$$

これが一番重要です！
「正体不明だった $X$ は、実は $T$ だった」ということが判明しました。

解として記録: 答えリストに $[X \mapsto T]$ を追加します
全体を置換: 残っているすべての制約と、これまでに求めた解の中に $X$ があれば、それを $T$ に書き換えます

3. 両辺が関数型の場合

$$
func(S_1) \ S_2 = func(T_1) \ T_2
$$

関数同士が等しいということは、引数の型と戻り値の型がそれぞれ等しいということです。
制約を分解して、元の集合に戻します。

引数の制約: $S_1 = T_1$
戻り値の制約: $S_2 = T_2$

これを制約集合が空になるまで繰り返せば、すべての型変数が判明します。
最終的に残った代入リストを、最初に解析した項の型に適用すれば、型推論の完了です！！

まとめ

今回は、Goを題材に、制約に基づく型推論の仕組みを見てきました。
ぜひ型推論をマスターしコンパイラの気持ちになって人力型推論を行ってみてはいかがでしょうか！！

最後に

以上、6日目の記事でした。まだまだ12月は始まったばかりですね！
引き続き今後のカレンダーも宜しくお願いします。