Closed8

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

riddle_tecriddle_tec

昨日
https://zenn.dev/gin_nazo/scraps/97459ba625f082


https://blog.framinal.life/entry/2025/04/14/154104

100日チャレンジに感化されたので、アレンジして自分でもやってみます。

やりたいこと

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

できたもの

https://github.com/lirlia/100day_challenge_backend/tree/main/day43_type_inference_go

riddle_tecriddle_tec

目的

  • Hindley-Milner型システムに基づいたシンプルな型推論エンジンをGo言語で実装する。
  • 型推論のプロセス(型変数の導入、制約収集、単一化)を理解する。
  • 実装した型推論エンジンをGoのhtml/templateで生成されたWeb UI経由で操作し、動作を確認できるようにする。

対象言語 (MiniLang)

(前回の提案と同じ仕様です)

  1. データ型: int, bool
  2. リテラル: 整数, 真偽値 (true, false)
  3. 変数: 英字で始まり、英数字とアンダースコアが続く識別子
  4. 演算:
    • 算術演算: +, -, *, / (int -> int -> int)
    • 比較演算: >, <, == (int -> int -> bool)
    • 論理演算: &&, || (bool -> bool -> bool)
    • 括弧 () をサポート
  5. :
    • リテラル, 変数参照, 演算式
    • let <variable> = <expr1> in <expr2>
    • if <cond_expr> then <then_expr> else <else_expr>
    • 関数定義 (ラムダ式): fn <param> => <body_expr>
    • 関数適用: <func_expr> (<arg_expr>) (カリー化対応)
  6. コメント: # から行末まで

型推論アルゴリズム

(前回の提案と同じ仕様です)

  • Hindley-Milner (Algorithm W) に基づく。
  • 主要な概念: 型変数, 型コンストラクタ, 型スキーム, 型環境, 制約収集, 単一化。

実装コンポーネント (すべてGo言語)

  1. AST (Abstract Syntax Tree):
    • MiniLangのコード構造を表現するGoの構造体 (ast/ast.go)。
  2. パーサー (Parser):
    • MiniLangのコード文字列をASTに変換 (parser/parser.go)。
    • 外部ライブラリ github.com/alecthomas/participle/v2 を使用。
  3. 型表現 (Type Representation):
    • MiniLangの型を表現するGoの構造体/インターフェース (types/types.go)。
  4. 単一化器 (Unificator):
    • 2つの型を受け取り、単一化可能であれば型代入を返すロジック (unification/unification.go)。
  5. 型推論器 (Inferencer):
    • ASTと型環境を受け取り、式の型を推論するメインロジック (inference/inference.go)。
  6. HTTPハンドラとUI:
    • main.go: HTTPサーバーを起動。
      • ルート (/) : html/template を用いてUI (コード入力フォーム、結果表示) を提供。
      • /infer (POST): フォームからMiniLangコードを受け取り、型推論を実行。結果を同じテンプレートに渡して再描画。
    • templates/index.html: UIのHTMLテンプレート。
    • static/style.css (任意): ミニマリズムに基づいた基本的なスタイリング。

デザイン

  • UI: Go html/template とシンプルなCSS (またはインラインスタイル)
  • デザイントレンド: ミニマリズム。機能的でクリーンなインターフェース。

作業手順案

  1. プロジェクトの仕様決定 (現在実施中)

    • ディレクトリレイアウトと作成するファイル一覧 (下記参照)
    • 各ファイルは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
    
  2. プロジェクト初期化

    • 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 に作業工程を追記・更新。
  3. 基本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.StripPrefixhttp.FileServer)。
    • テスト: サーバーを起動し、ブラウザで / にアクセスしてフォームが表示されることを確認。フォーム送信後、入力値と空の結果が表示されることを確認。
  4. AST定義 (ast/ast.go)

    • MiniLangの各構文要素 (リテラル、変数、二項演算、Let束縛、If式、ラムダ、関数適用) に対応するGoの構造体を定義。
    • 各構造体は participle のタグ (@, @@ など) を利用してパースルールを指定。
    • テスト (ast/ast_test.go): AST構造体が意図通り定義されているか、基本的な構造体生成のテスト (直接インスタンス化してフィールド確認など、パーサーがまだないので限定的)。
  5. パーサー実装 (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)
      • 構文エラーケース
  6. 型表現定義 (types/types.go)

    • Type インターフェースを定義 (例: String() string メソッドを持つ)。
    • 具象型: TInt, TBool
    • 型変数: TVar (一意なIDまたは名前を持つ)。新しい型変数を生成するヘルパー関数も用意。
    • 関数型: TFunc (引数の型 ArgType Type, 戻り値の型 ReturnType Type を持つ)。
    • 型スキーム: TScheme (束縛された型変数リスト QuantifiedVars []*TVar, 型 Type を持つ)。
    • テスト (types/types_test.go): 各型表現の文字列表現 (String()) や、型変数の生成ロジックなどをテスト。
  7. 単一化アルゴリズム実装 (unification/unification.go)

    • 型代入を表すマップ Substitution map[*TVar]Type を定義。
    • Unify(t1 Type, t2 Type) (Substitution, error) 関数を実装。
      • 基本的な単一化ルール (IntとInt、BoolとBoolは成功、IntとBoolは失敗など)。
      • 型変数 α と型 τ の単一化: ατ に含まれていなければ (occurs check)、{α := τ} を返す。
      • 関数型 T1 -> T2T3 -> T4 の単一化: T1T3T2T4を再帰的に単一化し、結果を合成。
    • 型代入を型に適用するヘルパー関数 Apply(sub Substitution, t Type) Type および型環境に適用する ApplyEnv(sub Substitution, env TypeEnvironment) TypeEnvironment を実装。
    • テスト (unification/unification_test.go):
      • TInt vs TInt (成功)
      • TInt vs TBool (失敗)
      • TVar("a") vs TInt (成功、{a := TInt})
      • TVar("a") vs TVar("b") (成功、{a := TVar("b")} or {b := TVar("a")})
      • TVar("a") vs TFunc(TVar("a"), TInt) (失敗、occurs check)
      • TFunc(TInt, TVar("a")) vs TFunc(TVar("b"), TBool) (成功、{b := TInt, a := TBool})
  8. 型推論アルゴリズム実装 (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
        1. e1 の型 t1 を推論。
        2. 現在の環境の型変数を一般化 (generalize) して x の型スキーム s1 を作成。
        3. xs1 を束縛した新しい環境で e2 の型 t2 を推論。
      • If式: 条件部の型が TBool であることを確認。then節とelse節の型を推論し、それらが単一化可能であることを確認。その型を返す。
      • ラムダ: fn x => body
        1. x のために新しい型変数 α を導入。
        2. x: α を環境に追加して body の型 τ_body を推論。
        3. 結果の型は α -> τ_body
      • 関数適用: f(arg)
        1. f の型 τ_farg の型 τ_arg を推論。
        2. 新しい型変数 β を導入。
        3. τ_fτ_arg -> β を単一化。
        4. 結果の型は β (単一化後の代入を適用したもの)。
    • テスト (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)
  9. API連携とUI表示 (main.go, templates/index.html)

    • /infer ハンドラ: フォームから受け取ったコード文字列をパーサーでASTに変換。
    • 初期型環境を作成 (空または組み込み関数があればそれらを含む)。
    • 型推論器を呼び出し、ASTのルートノードの型を推論。
    • 結果 (推論された型またはエラーメッセージ) を index.html テンプレートに渡して再レンダリング。
    • エラーハンドリングを丁寧に行い、ユーザーに分かりやすいメッセージを表示。
  10. デバッグと総合テスト

    • ブラウザから様々なMiniLangコードを入力し、型推論が期待通りに動作することを確認。
    • 型エラーが正しく報告されることを確認。
    • エッジケースや複雑な式での動作を確認。
  11. ドキュメント作成

    • README.md: アプリケーションの概要、MiniLangの文法、ビルド・実行方法、実装のポイントなどを記載。
    • PROGRESS.md: 完了したタスクにチェック。
    • .cursor/rules/knowledge.mdc: 新しいアプリの情報を追記。

これで進めて問題なければ、最初のステップであるプロジェクト初期化から開始します。
いかがでしょうか?

riddle_tecriddle_tec

型推論の仕組み、特に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 ...... の部分では、xint 型だと分かっています。
    • 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 を同じにするには、型変数 'xint に、型変数 'ybool にすればよい」といった代入 (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の木構造を再帰的に下から上へと辿りながら、各部分式の型を決定し、同時に必要な型変数の代入を蓄積していきます。

  1. 式の種類に応じて適切な推論規則を適用。
  2. 必要に応じて新しい型変数を導入。
  3. 型同士を比較し、一致させる必要がある場合は単一化を実行。
    • 単一化は、型変数に対する代入の集合を生成します。例えば、「型変数 αint である」「型変数 βγ -> bool である」など。
    • この代入は、以降の推論で他の型変数にも影響を与えます。
  4. let 式では、定義された変数の型を一般化して型スキームを作り、型環境に追加。
  5. 最終的に、式全体の型と、それを導くために必要だった全ての代入が得られます。

ポイント:

  • 最も汎用的な型: Hindley-Milnerは、可能な限り最も一般的(多相的)な型を推論しようとします。
  • 副作用なし: 基本的に純粋関数型言語を対象としています。
  • 決定性: 同じ式に対しては常に同じ主型 (principal type) を推論します。

この説明で、ASTから型が推論されるまでの大まかな流れや、型変数、型環境、単一化といった重要な概念の役割が少しでも明確になれば幸いです。非常に洗練されたアルゴリズムですが、核となるアイデアはこれらの組み合わせです。

riddle_tecriddle_tec

かしこまりました!もっと身近な例えを使って、型推論の雰囲気を掴んでみましょう。

AST(式の構造図)まではOKとのことなので、そこからスタートします。

料理に例えてみましょう!

  • あなた(型推論器): 天才シェフです。レシピ(AST)を見れば、完成する料理(式の型)が分かります。
  • 食材(値や部分式): 10(整数)、true(真偽値)、x(変数という名前の箱)、fn a => a + 1(「何かを受け取って1を足す」という調理法)など。
  • 料理の種類(型): 「甘いもの」「しょっぱいもの」「飲み物」「前菜」など。ここでは「整数」「真偽値」「整数→整数な関数」などです。
  • 謎の食材(型変数): 箱に入っていて中身がまだ分からない食材 'a'b。シェフは「これはたぶん果物 'a だな」と仮のラベルを貼ります。

シェフ(あなた)の仕事:

  1. レシピ(AST)をじっくり見る:
    レシピの各工程(式の各部分)で、どんな種類の料理(型)ができあがるかを見極めます。

  2. 「食材リスト」(型環境)を管理する:

    • x という名前の箱には『整数』が入っている」
    • id という調理法は『どんな食材 'a を入れても、そのまま 'a が出てくる魔法の鍋』だ」
      という情報をメモしておきます。
  3. 調理工程(式の評価)で「型」を合わせていく(単一化):

    • 例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

      1. let myFunc = fn item => item + 1 の部分:
        • シェフは fn item => item + 1 という調理法を見ます。
        • item は謎の食材 'b だな」と仮ラベルを貼ります。
        • item + 1 は… + 1 するから item は『整数』じゃないとダメだ!謎食材 'b の正体は『整数』だった!」(単一化で 'b = int
        • 「ということは、この調理法は『整数』を受け取って『整数』を返すものだな (int -> int)」
        • シェフは食材リストに「myFunc は『整数→整数な調理法』」と書き込みます。
        • 重要: このとき、myFunc は「特定のレシピだけでなく、一般的に使える『整数を1増やす機械』」として登録されます(一般化)。
      2. in myFunc true の部分:
        • シェフは食材リストから「myFunc は『整数→整数な調理法』」という情報を取り出します。
        • true を見ます。「これは『真偽値』だな」。
        • 「おっと! myFunc は『整数』を期待しているのに、『真偽値』が来たぞ!これは調理できない!」とエラーを出します。(単一化失敗)

ポイント:

  • 型変数は「とりあえずの仮置き」: 後で他の情報から具体的な型が決まったり、他の型変数と同じものであることが判明したりします。
  • 単一化は「パズル合わせ」: 「この型とこの型は同じはずだ」という制約から、型変数に入るべき型をパチパチとはめていきます。
  • letは賢い: let で定義されたものは、可能な限り汎用的に(多相的に)扱えるように「型スキーム」という形で登録されます。これにより、同じ関数を異なる型で安全に再利用できます (例: let id = fn x => x in id 1; id true)。

この料理の例えで、ASTの先で型推論器が何をしているかのイメージが少しでも具体的になっていれば嬉しいです!
「矛盾がないように、各部分の『料理の種類(型)』を賢く決定していく」のが型推論の仕事です。

riddle_tecriddle_tec

はい、day43_type_inference_go/inference/inference.goInfer 関数(内部的には 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{}} という代入が含まれていれば、condTypetypes.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{}} のような代入になります。
      • もし condTypetypes.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 節の推論で得られた代入 sThensCurrent に合成します。
		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 節の推論で得られた代入 sElsesCurrent に合成します。
		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 節の型は同じでなければなりません。
    • ここで、(代入適用済みの) thenTypeelseType を単一化します。
    • これにより、もし両者が型変数を含んでいれば、それらが同じ型になるような追加の代入 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 式の型推論処理の各行の解説です。
やっていることは、

  1. 条件式の型を推論し、それが bool 型であることを確認(単一化)。
  2. then 節の型を推論。
  3. else 節の型を推論。
  4. then 節の型と else 節の型が同じであることを確認(単一化)。
  5. その結果の型を if 式全体の型とする。
    各ステップで得られた型制約(代入)は、後続の推論に影響を与えるために、sCurrent という変数に逐次合成されていきます。
このスクラップは2ヶ月前にクローズされました