100日チャレンジ day43 (型推論エンジン)

昨日
100日チャレンジに感化されたので、アレンジして自分でもやってみます。
やりたいこと
- 世の中のさまざまなドメインの簡易実装をつくり、バックエンドの実装に慣れる(dbスキーマ設計や、関数の分割、使いやすいインターフェイスの切り方に慣れる
- 設計力(これはシステムのオーバービューを先に自分で作ってaiに依頼できるようにする
- 生成aiをつかったバイブコーティングになれる
- 実際にやったことはzennのスクラップにまとめ、成果はzennのブログにまとめる(アプリ自体の公開は必須ではないかコードはgithubにおく)
できたもの

型推論 をやる

目的
- Hindley-Milner型システムに基づいたシンプルな型推論エンジンをGo言語で実装する。
- 型推論のプロセス(型変数の導入、制約収集、単一化)を理解する。
- 実装した型推論エンジンをGoの
html/template
で生成されたWeb UI経由で操作し、動作を確認できるようにする。
対象言語 (MiniLang)
(前回の提案と同じ仕様です)
-
データ型:
int
,bool
-
リテラル: 整数, 真偽値 (
true
,false
) - 変数: 英字で始まり、英数字とアンダースコアが続く識別子
-
演算:
- 算術演算:
+
,-
,*
,/
(int -> int -> int
) - 比較演算:
>
,<
,==
(int -> int -> bool
) - 論理演算:
&&
,||
(bool -> bool -> bool
) - 括弧
()
をサポート
- 算術演算:
-
式:
- リテラル, 変数参照, 演算式
let <variable> = <expr1> in <expr2>
if <cond_expr> then <then_expr> else <else_expr>
- 関数定義 (ラムダ式):
fn <param> => <body_expr>
- 関数適用:
<func_expr> (<arg_expr>)
(カリー化対応)
-
コメント:
#
から行末まで
型推論アルゴリズム
(前回の提案と同じ仕様です)
- Hindley-Milner (Algorithm W) に基づく。
- 主要な概念: 型変数, 型コンストラクタ, 型スキーム, 型環境, 制約収集, 単一化。
実装コンポーネント (すべてGo言語)
-
AST (Abstract Syntax Tree):
- MiniLangのコード構造を表現するGoの構造体 (
ast/ast.go
)。
- MiniLangのコード構造を表現するGoの構造体 (
-
パーサー (Parser):
- MiniLangのコード文字列をASTに変換 (
parser/parser.go
)。 - 外部ライブラリ
github.com/alecthomas/participle/v2
を使用。
- MiniLangのコード文字列をASTに変換 (
-
型表現 (Type Representation):
- MiniLangの型を表現するGoの構造体/インターフェース (
types/types.go
)。
- MiniLangの型を表現するGoの構造体/インターフェース (
-
単一化器 (Unificator):
- 2つの型を受け取り、単一化可能であれば型代入を返すロジック (
unification/unification.go
)。
- 2つの型を受け取り、単一化可能であれば型代入を返すロジック (
-
型推論器 (Inferencer):
- ASTと型環境を受け取り、式の型を推論するメインロジック (
inference/inference.go
)。
- ASTと型環境を受け取り、式の型を推論するメインロジック (
-
HTTPハンドラとUI:
-
main.go
: HTTPサーバーを起動。- ルート (
/
) :html/template
を用いてUI (コード入力フォーム、結果表示) を提供。 -
/infer
(POST): フォームからMiniLangコードを受け取り、型推論を実行。結果を同じテンプレートに渡して再描画。
- ルート (
-
templates/index.html
: UIのHTMLテンプレート。 -
static/style.css
(任意): ミニマリズムに基づいた基本的なスタイリング。
-
デザイン
- UI: Go
html/template
とシンプルなCSS (またはインラインスタイル) - デザイントレンド: ミニマリズム。機能的でクリーンなインターフェース。
作業手順案
-
プロジェクトの仕様決定 (現在実施中)
- ディレクトリレイアウトと作成するファイル一覧 (下記参照)
- 各ファイルは300行以内を目標
- 各ステップごとにテスト (Goのユニットテスト) を作成し実施
- テスト通過後はステップ名を含むコミット
ディレクトリレイアウト案:
day[DAY_NUMBER]_type_inference_go/ ├── go.mod ├── go.sum ├── main.go # HTTPサーバー、ルーティング ├── ast/ │ └── ast.go # ASTノード定義 │ └── ast_test.go ├── parser/ │ └── parser.go # パーサー実装 │ └── parser_test.go ├── types/ │ └── types.go # 型表現定義 │ └── types_test.go ├── unification/ │ └── unification.go # 単一化アルゴリズム │ └── unification_test.go ├── inference/ │ └── inference.go # 型推論アルゴリズム │ └── inference_test.go ├── templates/ │ └── index.html # UIテンプレート ├── static/ # CSSなど静的ファイル (任意) │ └── style.css ├── README.md └── PROGRESS.md
-
プロジェクト初期化
-
template
ディレクトリの内容をday[DAY_NUMBER]_type_inference_go
にコピー。 -
cd day[DAY_NUMBER]_type_inference_go
で移動。 -
package.json
を削除 (今回はNode.jsプロジェクトではないため)。 -
go mod init github.com/lirlia/100day_challenge_backend/day[DAY_NUMBER]_type_inference_go
を実行。 -
go get github.com/alecthomas/participle/v2
を実行。 - 上記のディレクトリ構造を作成。
-
README.md
に今回のアプリ設計概要を記載。 -
PROGRESS.md
に作業工程を追記・更新。
-
-
基本HTTPサーバーとUIテンプレート設定
-
main.go
: ルート (/
) でtemplates/index.html
をレンダリングするハンドラと、/infer
(POST) でリクエストボディからコードを受け取り、結果をindex.html
に渡して再レンダリングするハンドラを実装。 -
templates/index.html
: コード入力用<textarea name="code">
、送信ボタン、結果表示エリア ({{ .Result }}
) を持つHTMLを作成。前回入力したコードも表示されるように (<textarea name="code">{{ .Code }}</textarea>
)。 - (任意)
static/style.css
: 基本的なスタイルを追加。main.go
で/static/
パスへのリクエストを処理できるようにする (http.StripPrefix
とhttp.FileServer
)。 - テスト: サーバーを起動し、ブラウザで
/
にアクセスしてフォームが表示されることを確認。フォーム送信後、入力値と空の結果が表示されることを確認。
-
-
AST定義 (
ast/ast.go
)- MiniLangの各構文要素 (リテラル、変数、二項演算、Let束縛、If式、ラムダ、関数適用) に対応するGoの構造体を定義。
- 各構造体は
participle
のタグ (@
,@@
など) を利用してパースルールを指定。 - テスト (
ast/ast_test.go
): AST構造体が意図通り定義されているか、基本的な構造体生成のテスト (直接インスタンス化してフィールド確認など、パーサーがまだないので限定的)。
-
パーサー実装 (
parser/parser.go
)-
participle.New[MiniLangRootNode]
を使用してパーサーを構築。MiniLangRootNode
はMiniLangプログラム全体のルートとなるASTノード。 - 入力文字列を受け取り、ASTを返す
Parse(code string) (*ast.MiniLangRootNode, error)
関数を実装。 - テスト (
parser/parser_test.go
):- 簡単なリテラル (
123
,true
) - 変数 (
x
) - 算術演算 (
1 + 2 * 3
,(1 + 2) * 3
) -
let
束縛 (let x = 10 in x + 5
) -
if
式 (if x > 0 then 1 else -1
) - 関数定義 (
fn x => x + 1
) - 関数適用 (
myFunc(10)
,(fn x => x)(10)
) - コメントが含まれるコード (
let x = 1 # comment \n in x
) - 構文エラーケース
- 簡単なリテラル (
-
-
型表現定義 (
types/types.go
)-
Type
インターフェースを定義 (例:String() string
メソッドを持つ)。 - 具象型:
TInt
,TBool
。 - 型変数:
TVar
(一意なIDまたは名前を持つ)。新しい型変数を生成するヘルパー関数も用意。 - 関数型:
TFunc
(引数の型ArgType Type
, 戻り値の型ReturnType Type
を持つ)。 - 型スキーム:
TScheme
(束縛された型変数リストQuantifiedVars []*TVar
, 型Type
を持つ)。 - テスト (
types/types_test.go
): 各型表現の文字列表現 (String()
) や、型変数の生成ロジックなどをテスト。
-
-
単一化アルゴリズム実装 (
unification/unification.go
)- 型代入を表すマップ
Substitution map[*TVar]Type
を定義。 -
Unify(t1 Type, t2 Type) (Substitution, error)
関数を実装。- 基本的な単一化ルール (IntとInt、BoolとBoolは成功、IntとBoolは失敗など)。
- 型変数
α
と型τ
の単一化:α
がτ
に含まれていなければ (occurs check)、{α := τ}
を返す。 - 関数型
T1 -> T2
とT3 -> T4
の単一化:T1
とT3
、T2
とT4
を再帰的に単一化し、結果を合成。
- 型代入を型に適用するヘルパー関数
Apply(sub Substitution, t Type) Type
および型環境に適用するApplyEnv(sub Substitution, env TypeEnvironment) TypeEnvironment
を実装。 - テスト (
unification/unification_test.go
):-
TInt
vsTInt
(成功) -
TInt
vsTBool
(失敗) -
TVar("a")
vsTInt
(成功、{a := TInt}
) -
TVar("a")
vsTVar("b")
(成功、{a := TVar("b")}
or{b := TVar("a")}
) -
TVar("a")
vsTFunc(TVar("a"), TInt)
(失敗、occurs check) -
TFunc(TInt, TVar("a"))
vsTFunc(TVar("b"), TBool)
(成功、{b := TInt, a := TBool}
)
-
- 型代入を表すマップ
-
型推論アルゴリズム実装 (
inference/inference.go
)- 型環境
TypeEnvironment map[string]TypeScheme
を定義 (変数名から型スキームへのマップ)。 -
Infer(env TypeEnvironment, expr ast.Expression) (Type, Substitution, error)
関数 (または類似のシグネチャでASTノードごとに処理するヘルパー関数群) を実装。-
リテラル:
TInt
,TBool
を返す。 - 変数: 環境から型スキembraを取得。多相的な場合は型変数を具体化 (instantiate)。
- 二項演算: オペランドの型を推論し、演算子の期待する型と単一化。結果の型を返す。
-
Let束縛:
let x = e1 in e2
-
e1
の型t1
を推論。 - 現在の環境の型変数を一般化 (generalize) して
x
の型スキームs1
を作成。 -
x
にs1
を束縛した新しい環境でe2
の型t2
を推論。
-
-
If式: 条件部の型が
TBool
であることを確認。then節とelse節の型を推論し、それらが単一化可能であることを確認。その型を返す。 -
ラムダ:
fn x => body
-
x
のために新しい型変数α
を導入。 -
x: α
を環境に追加してbody
の型τ_body
を推論。 - 結果の型は
α -> τ_body
。
-
-
関数適用:
f(arg)
-
f
の型τ_f
とarg
の型τ_arg
を推論。 - 新しい型変数
β
を導入。 -
τ_f
とτ_arg -> β
を単一化。 - 結果の型は
β
(単一化後の代入を適用したもの)。
-
-
リテラル:
- テスト (
inference/inference_test.go
):-
10
->int
-
true
->bool
-
let id = fn x => x in id(10)
->int
-
let id = fn x => x in id(true)
->bool
-
(fn x => x + 1)(5)
->int
-
let const = fn x => fn y => x in const(1)(true)
->int
- 型エラーケース:
1 + true
,(fn x => x + 1)(true)
-
- 型環境
-
API連携とUI表示 (
main.go
,templates/index.html
)-
/infer
ハンドラ: フォームから受け取ったコード文字列をパーサーでASTに変換。 - 初期型環境を作成 (空または組み込み関数があればそれらを含む)。
- 型推論器を呼び出し、ASTのルートノードの型を推論。
- 結果 (推論された型またはエラーメッセージ) を
index.html
テンプレートに渡して再レンダリング。 - エラーハンドリングを丁寧に行い、ユーザーに分かりやすいメッセージを表示。
-
-
デバッグと総合テスト
- ブラウザから様々なMiniLangコードを入力し、型推論が期待通りに動作することを確認。
- 型エラーが正しく報告されることを確認。
- エッジケースや複雑な式での動作を確認。
-
ドキュメント作成
-
README.md
: アプリケーションの概要、MiniLangの文法、ビルド・実行方法、実装のポイントなどを記載。 -
PROGRESS.md
: 完了したタスクにチェック。 -
.cursor/rules/knowledge.mdc
: 新しいアプリの情報を追記。
-
これで進めて問題なければ、最初のステップであるプロジェクト初期化から開始します。
いかがでしょうか?

型推論の仕組み、特にASTから先の部分ですね。Hindley-Milner (アルゴリズムW) の主要なアイデアを簡単に説明します。
AST (抽象構文木) は、コードの構造を木で表現したものでしたね。型推論は、この木の各ノード(式や値など)に対して、「このノードはどんな型を持つべきか?」を解決していくプロセスです。
1. 型と型変数
-
具体的な型:
int
(整数),bool
(真偽値) など、決まった型。 -
型変数: まだ具体的な型が分からない場合に使う「仮の型」です。よく
'a
,'b
,α
,β
などと書かれます。例えば、「関数f
の引数x
の型はまだ分からないから、とりあえず'a
としておこう」という感じです。 -
関数型:
型1 -> 型2
という形で、「型1 を引数に取り、型2 を返す関数」を表します。例えば、int -> bool
は整数を受け取って真偽値を返す関数です。型変数も使えるので、'a -> 'b
は「何か('a
)を受け取って何か('b
)を返す関数」となります。
2. 型環境 (Type Environment)
- 変数名とその型(または型スキーム)を対応付ける辞書のようなものです。
- 例:
env = { "x": int, "id": forall 'a. 'a -> 'a }
-
let x = 10 in ...
の...
の部分では、x
はint
型だと分かっています。 -
id
は「どんな型'a
に対しても、'a
型の値を受け取って'a
型の値を返す関数」(いわゆる恒等関数)です。このような「どんな型でもOK」という性質を 多相性 (Polymorphism) といい、forall 'a.
(任意の型'a
について) という記号で表現されることがあります。これを型スキームと呼びます。
- 例:
3. 推論規則と単一化 (Unification)
ASTの各ノードの種類に応じて、型を推論するためのルール(推論規則)があります。
-
リテラル:
-
123
ならint
型。 -
true
ならbool
型。
-
-
変数:
- 型環境から変数の型を探します。もし型スキーム (
forall 'a. ...
) であれば、型スキーム内の型変数 ('a
) を新しい未使用の型変数(例:'t1
)に置き換えて(これをインスタンス化といいます)、具体的な型として使います。
- 型環境から変数の型を探します。もし型スキーム (
-
関数定義 (
fn x => expr
):- 引数
x
の型を新しい型変数'a
と仮定します。 - 型環境に
x: 'a
を追加して、本体expr
の型を推論します。もしexpr
の型が'b
と推論されたら、この関数全体の型は'a -> 'b
となります。
- 引数
-
関数適用 (
f arg
):- まず関数
f
の型を推論します。これが't_fun -> 't_ret
(何かを受け取って何かを返す関数型) であると期待されます。 - 次に引数
arg
の型't_arg
を推論します。 - ここで重要なのが 単一化 (Unification) です。関数の引数型
't_fun
と実際に渡された引数の型't_arg
は一致するはずです。単一化は、これら2つの型(型変数を含むかもしれない)が等しくなるように、型変数に具体的な型を割り当てるプロセスです。「't_fun
と't_arg
を同じにするには、型変数'x
はint
に、型変数'y
はbool
にすればよい」といった代入 (Substitution) を見つけ出します。 - 単一化が成功すれば、関数適用の結果の型は
't_ret
(適切に代入が適用されたもの) になります。失敗すれば型エラーです (例:int -> ...
な関数にbool
を渡そうとした)。
- まず関数
-
if cond then expr1 else expr2
:- 条件
cond
の型はbool
でなければなりません (単一化)。 -
expr1
の型 ('t1
) とexpr2
の型 ('t2
) は同じでなければなりません ('t1
と't2
を単一化)。 -
if
式全体の型は、その単一化された型't1
(または't2
) になります。
- 条件
-
let x = expr1 in expr2
:- まず
expr1
の型't1
を(現在の型環境で)推論します。 - 次に、この
't1
に含まれる型変数のうち、現在の型環境に束縛されていない自由な型変数を特定し、それらをforall
で束縛して型スキームを作ります(これを一般化といいます)。例えば't1
が'a -> 'a
で、'a
が現在の環境のどこにも出てこなければ、型スキームforall 'a. 'a -> 'a
を作ります。 - 新しい型環境として、元の環境に
x
とその型スキームを追加します。 - この新しい環境で
expr2
の型を推論し、それがlet
式全体の型となります。
- まず
4. アルゴリズム W の流れ (大まかに)
アルゴリズムWは、これらの推論規則と単一化を使い、ASTの木構造を再帰的に下から上へと辿りながら、各部分式の型を決定し、同時に必要な型変数の代入を蓄積していきます。
- 式の種類に応じて適切な推論規則を適用。
- 必要に応じて新しい型変数を導入。
- 型同士を比較し、一致させる必要がある場合は単一化を実行。
- 単一化は、型変数に対する代入の集合を生成します。例えば、「型変数
α
はint
である」「型変数β
はγ -> bool
である」など。 - この代入は、以降の推論で他の型変数にも影響を与えます。
- 単一化は、型変数に対する代入の集合を生成します。例えば、「型変数
-
let
式では、定義された変数の型を一般化して型スキームを作り、型環境に追加。 - 最終的に、式全体の型と、それを導くために必要だった全ての代入が得られます。
ポイント:
- 最も汎用的な型: Hindley-Milnerは、可能な限り最も一般的(多相的)な型を推論しようとします。
- 副作用なし: 基本的に純粋関数型言語を対象としています。
- 決定性: 同じ式に対しては常に同じ主型 (principal type) を推論します。
この説明で、ASTから型が推論されるまでの大まかな流れや、型変数、型環境、単一化といった重要な概念の役割が少しでも明確になれば幸いです。非常に洗練されたアルゴリズムですが、核となるアイデアはこれらの組み合わせです。

かしこまりました!もっと身近な例えを使って、型推論の雰囲気を掴んでみましょう。
AST(式の構造図)まではOKとのことなので、そこからスタートします。
料理に例えてみましょう!
- あなた(型推論器): 天才シェフです。レシピ(AST)を見れば、完成する料理(式の型)が分かります。
-
食材(値や部分式):
10
(整数)、true
(真偽値)、x
(変数という名前の箱)、fn a => a + 1
(「何かを受け取って1を足す」という調理法)など。 - 料理の種類(型): 「甘いもの」「しょっぱいもの」「飲み物」「前菜」など。ここでは「整数」「真偽値」「整数→整数な関数」などです。
-
謎の食材(型変数): 箱に入っていて中身がまだ分からない食材
'a
、'b
。シェフは「これはたぶん果物'a
だな」と仮のラベルを貼ります。
シェフ(あなた)の仕事:
-
レシピ(AST)をじっくり見る:
レシピの各工程(式の各部分)で、どんな種類の料理(型)ができあがるかを見極めます。 -
「食材リスト」(型環境)を管理する:
- 「
x
という名前の箱には『整数』が入っている」 - 「
id
という調理法は『どんな食材'a
を入れても、そのまま'a
が出てくる魔法の鍋』だ」
という情報をメモしておきます。
- 「
-
調理工程(式の評価)で「型」を合わせていく(単一化):
-
例1:
1 + 2
- シェフは「1は『整数』、2も『整数』だな」と見ます。
- 「『整数』と『整数』を
+
で混ぜるなら、出来上がるのも『整数』だ!」と判断します。
-
例2:
id 5
(id はfn x => x
とする)- まず
id
という調理法を見ます。食材リストには「id
は『どんな食材'a
を入れても、そのまま'a
が出てくる魔法の鍋』」とあります。 - 次に
5
を見ます。「これは『整数』だな」。 - ここで「魔法の鍋」のルール発動!
- 鍋(
id
)は「食材'a
を期待している」。 - 実際に来たのは「『整数』の
5
」。 - シェフは「なるほど!じゃあ、このレシピで使っている謎の食材
'a
の正体は『整数』だったんだ!」とひらめきます。(これが単一化。'a = int
という代入が見つかる) - 鍋から出てくるのも
'a
(つまり『整数』)なので、id 5
の結果は『整数』だと分かります。
- 鍋(
- まず
-
例3:
if flag then 10 else 20
-
flag
を見ます。シェフは「これは『真偽値』(本当か嘘か)じゃないとダメだぞ」と考えます。もしflag
が『整数』だったら「条件は『真偽値』じゃないと!」とエラーを出します。(単一化) -
10
は『整数』。20
も『整数』。 - 「『真偽値』の条件で、『整数』か『整数』を選ぶなら、最終的な料理も『整数』だ」
-
-
例4:
let myFunc = fn item => item + 1 in myFunc true
-
let myFunc = fn item => item + 1
の部分:- シェフは
fn item => item + 1
という調理法を見ます。 - 「
item
は謎の食材'b
だな」と仮ラベルを貼ります。 - 「
item + 1
は…+ 1
するからitem
は『整数』じゃないとダメだ!謎食材'b
の正体は『整数』だった!」(単一化で'b = int
) - 「ということは、この調理法は『整数』を受け取って『整数』を返すものだな (
int -> int
)」 - シェフは食材リストに「
myFunc
は『整数→整数な調理法』」と書き込みます。 -
重要: このとき、
myFunc
は「特定のレシピだけでなく、一般的に使える『整数を1増やす機械』」として登録されます(一般化)。
- シェフは
-
in myFunc true
の部分:- シェフは食材リストから「
myFunc
は『整数→整数な調理法』」という情報を取り出します。 -
true
を見ます。「これは『真偽値』だな」。 - 「おっと!
myFunc
は『整数』を期待しているのに、『真偽値』が来たぞ!これは調理できない!」とエラーを出します。(単一化失敗)
- シェフは食材リストから「
-
-
ポイント:
- 型変数は「とりあえずの仮置き」: 後で他の情報から具体的な型が決まったり、他の型変数と同じものであることが判明したりします。
- 単一化は「パズル合わせ」: 「この型とこの型は同じはずだ」という制約から、型変数に入るべき型をパチパチとはめていきます。
-
letは賢い:
let
で定義されたものは、可能な限り汎用的に(多相的に)扱えるように「型スキーム」という形で登録されます。これにより、同じ関数を異なる型で安全に再利用できます (例:let id = fn x => x in id 1; id true
)。
この料理の例えで、ASTの先で型推論器が何をしているかのイメージが少しでも具体的になっていれば嬉しいです!
「矛盾がないように、各部分の『料理の種類(型)』を賢く決定していく」のが型推論の仕事です。

はい、day43_type_inference_go/inference/inference.go
の Infer
関数(内部的には inferExpr
ヘルパー関数)の case *ast.If:
部分の処理ですね。1行ずつ解説します。
if cond then expr1 else expr2
という形の式を扱います。
case *ast.If:
// CondExpr: Term, ThenExpr: Term, ElseExpr: Term
-
case *ast.If:
:expr
が*ast.If
型(if
式のASTノード)である場合の処理ブロックを開始します。 - コメント
// CondExpr: Term, ThenExpr: Term, ElseExpr: Term
は、ast.If
構造体のフィールドCondExpr
,ThenExpr
,ElseExpr
がそれぞれast.Term
型であることを示しています(ASTの定義に基づきます)。
condType, sCond, err := inferExpr(env, e.CondExpr, sub)
-
inferExpr(env, e.CondExpr, sub)
:-
if
式の条件部分e.CondExpr
の型を推論するために、inferExpr
を再帰的に呼び出します。 -
env
: 現在の型環境(変数の型情報など)。 -
e.CondExpr
:if
式の条件式部分のASTノード。 -
sub
: これまでの型推論で蓄積されてきた代入(型変数に具体的な型を割り当てる情報)。
-
-
condType
: 条件式の推論された型が格納されます。 -
sCond
: 条件式の型推論によって新たに得られた(または更新された)代入が格納されます。 -
err
: 型推論中にエラーが発生した場合、その情報が格納されます。
if err != nil {
return nil, sCond, fmt.Errorf("type inference failed for if condition: %w", err)
}
-
if err != nil
: 条件式の型推論でエラーが発生した場合の処理です。 -
return nil, sCond, fmt.Errorf(...)
:-
nil
: 型の推論に失敗したためnil
を返します。 -
sCond
: エラーが発生した時点での代入を返します(エラーが代入の途中で発生した場合でも、それまでの情報は保持)。 -
fmt.Errorf(...)
: エラーメッセージを作成して返します。%w
はGo 1.13から導入されたエラーラッピングの書式指定子で、元のエラーerr
をラップします。
-
sCurrent := sCond
-
sCurrent := sCond
: 条件式の推論から得られた代入sCond
を、このif
式全体の型推論で使う現在の代入sCurrent
として初期化します。
condType = unification.Apply(sCurrent, condType)
-
unification.Apply(sCurrent, condType)
:-
condType
(条件式の推論された型)に対して、現在の代入sCurrent
を適用します。 - これにより、
condType
内の型変数が、sCurrent
によって具体的な型に置き換えられます。例えば、condType
が型変数'a
で、sCurrent
に{'a': types.TBool{}}
という代入が含まれていれば、condType
はtypes.TBool{}
になります。
-
sUnifyCond, errUnifyCond := unification.Unify(condType, types.TBool{})
-
unification.Unify(condType, types.TBool{})
:-
if
文の条件式は必ずbool
型でなければなりません。 - ここで、実際に推論され代入も適用済みの
condType
と、期待される型types.TBool{}
(ブール型)を単一化 (Unify) します。 - 単一化は、この2つの型が等しくなるように、新たな代入(
sUnifyCond
)を見つけようとします。- もし
condType
が既にtypes.TBool{}
なら、sUnifyCond
は空の代入になります。 - もし
condType
が型変数'a
で、types.TBool{}
と単一化可能なら、sUnifyCond
は{'a': types.TBool{}}
のような代入になります。 - もし
condType
がtypes.TInt{}
のようにtypes.TBool{}
と明らかに異なる型で単一化不可能な場合、errUnifyCond
にエラーが入ります。
- もし
-
-
sUnifyCond
: 単一化によって得られた追加の代入。 -
errUnifyCond
: 単一化に失敗した場合のエラー。
if errUnifyCond != nil {
return nil, sCurrent, fmt.Errorf("if condition must be boolean, got %s: %w", condType, errUnifyCond)
}
-
if errUnifyCond != nil
: 条件式の型とbool
型の単一化に失敗した場合(つまり、条件式がbool
型またはbool
型になれる型変数でない場合)の処理です。 -
return nil, sCurrent, fmt.Errorf(...)
: 型エラーとして処理を終了します。エラーメッセージには、期待される型 (boolean
) と実際の型 (condType.String()
) が含まれます。
sCurrent = sCurrent.Compose(sUnifyCond)
-
sCurrent.Compose(sUnifyCond)
:- これまでの代入
sCurrent
に、条件式の型とbool
型を単一化して得られた新しい代入sUnifyCond
を合成(Compose)します。 - Compose は、2つの代入を組み合わせて1つの新しい代入を作ります。例えば
s1 = {'a': 'b'}
とs2 = {'b': int}
があれば、s1.Compose(s2)
は{'a': int, 'b': int}
のような結果になります(正確な動作はCompose
の実装によります)。 - これにより、
sCurrent
は条件式がbool
型であるという制約を満たすために必要な全ての代入を含む最新の状態になります。
- これまでの代入
envForBranches := env.Apply(sCurrent)
-
env.Apply(sCurrent)
:-
then
節とelse
節の型を推論する前に、現在の型環境env
に対して、最新の代入sCurrent
を適用します。 - これにより、環境内の型スキームに含まれる型変数なども、条件式の推論と単一化で得られた情報で更新されます。
- この更新された環境
envForBranches
を使って、then
節とelse
節の推論を行います。
-
thenType, sThen, errThen := inferExpr(envForBranches, e.ThenExpr, sCurrent)
-
inferExpr(envForBranches, e.ThenExpr, sCurrent)
:then
節 (e.ThenExpr
) の型を推論します。-
envForBranches
: 条件部の推論結果を反映した型環境。 -
sCurrent
: 条件部の推論と単一化の結果を含む、ここまでの累積代入。
-
-
thenType
,sThen
,errThen
: それぞれthen
節の型、それによる追加代入、エラー。
if errThen != nil {
return nil, sThen, fmt.Errorf("type inference failed for then branch: %w", errThen)
}
-
then
節の型推論でエラーがあれば処理を終了します。
sCurrent = sCurrent.Compose(sThen)
-
then
節の推論で得られた代入sThen
をsCurrent
に合成します。
thenType = unification.Apply(sCurrent, thenType)
-
then
節の型thenType
に、最新の代入sCurrent
(ここにはsThen
も含まれる)を適用して、型変数を解決します。
elseType, sElse, errElse := inferExpr(env.Apply(sCurrent), e.ElseExpr, sCurrent)
-
inferExpr(env.Apply(sCurrent), e.ElseExpr, sCurrent)
:else
節 (e.ElseExpr
) の型を推論します。-
env.Apply(sCurrent)
: 型環境には、then
節の推論結果も反映された最新の代入sCurrent
を適用します。 -
sCurrent
:then
節の推論結果も含む累積代入。
-
-
elseType
,sElse
,errElse
: それぞれelse
節の型、それによる追加代入、エラー。
if errElse != nil {
return nil, sElse, fmt.Errorf("type inference failed for else branch: %w", errElse)
}
-
else
節の型推論でエラーがあれば処理を終了します。
sCurrent = sCurrent.Compose(sElse)
-
else
節の推論で得られた代入sElse
をsCurrent
に合成します。
elseType = unification.Apply(sCurrent, elseType)
-
else
節の型elseType
に、最新の代入sCurrent
(ここにはsElse
も含まれる)を適用して、型変数を解決します。
// Unify then and else branches
sUnifyBranches, errUnifyBranches := unification.Unify(thenType, elseType)
-
unification.Unify(thenType, elseType)
:-
if
式では、then
節の型とelse
節の型は同じでなければなりません。 - ここで、(代入適用済みの)
thenType
とelseType
を単一化します。 - これにより、もし両者が型変数を含んでいれば、それらが同じ型になるような追加の代入
sUnifyBranches
が見つかるか、型が不一致ならエラーerrUnifyBranches
が発生します。
-
if errUnifyBranches != nil {
return nil, sCurrent, fmt.Errorf("type mismatch between then (%s) and else (%s) branches: %w", thenType, elseType, errUnifyBranches)
}
-
then
節とelse
節の型の単一化に失敗した場合の処理です。 - エラーメッセージには、それぞれの節の型が表示されます。
sCurrent = sCurrent.Compose(sUnifyBranches)
-
then/else
の単一化で得られた代入sUnifyBranches
を、全体の代入sCurrent
に合成します。
return unification.Apply(sCurrent, thenType), sCurrent, nil // Result type is the unified type of branches
-
unification.Apply(sCurrent, thenType)
:-
if
式全体の型を返します。これは、then
節とelse
節が単一化された後の型です (elseType
を使っても同じ結果になるはずです)。最新の代入sCurrent
を適用して、残っている型変数をできるだけ解決します。
-
-
sCurrent
: このif
式全体の推論を通して蓄積・合成された最終的な代入。 -
nil
: エラーなし。
以上が、if
式の型推論処理の各行の解説です。
やっていることは、
- 条件式の型を推論し、それが
bool
型であることを確認(単一化)。 -
then
節の型を推論。 -
else
節の型を推論。 -
then
節の型とelse
節の型が同じであることを確認(単一化)。 - その結果の型を
if
式全体の型とする。
各ステップで得られた型制約(代入)は、後続の推論に影響を与えるために、sCurrent
という変数に逐次合成されていきます。