Upgrade to Pro — share decks privately, control downloads, hide ads and more …

型システムを知りたい人のための型検査器作成入門

 型システムを知りたい人のための型検査器作成入門

Avatar for Yusuke Endoh

Yusuke Endoh

June 14, 2025
Tweet

More Decks by Yusuke Endoh

Other Decks in Technology

Transcript

  1. Yusuke Endoh (@mametter) • プログラミング言語 Ruby の開発者のひとり • STORES, Inc.

    でフルタイムでやっている • 主な貢献:キーワード引数を実装したとか • 最近は Ruby の型解析器 TypeProf の開発 • 趣味:変なプログラムを書くこと
  2. 変なプログラムの例:放射線耐性Quine • どの1文字を消しても元のプログラムを出力する eval=eval=eval='eval$s=%q(eval(%w(puts((%q(eval=ev al=eval=^Z^##^_/#{eval@eval@if@eval)+?@*10+%(.size >#{(s=%(eval$s=%q(#$s)#)).size-1}}}#LMNOPQRS_##thx .flagitious!## )+?@*12+%(TUVW XY/.i@rescue## /_3141592653

    589793+)+?@* 16+%(+271828 182845904; _987654321 0;;eval)+? @*18+%("x =((#{s.s um}-eval. _sum)%256 ).chr; ;eval)+?@ *12+%(.s can(//){ a=$`+x+$ ^_a.unpa ck (^ H*^)[0]. hex%999989==#{s.unpac k("H*")[0].hex%999989 }&&eval(a)}#"##"_eval @eval####@(C)@Copyrig ht@2014@Yusuke@Endoh@# ###)).tr("@_^",32.chr< <10<<39).sub(?Z,s));e xit#AB CDEFGHIJK)*%()))#'##' /#{eval eval if eval .size>692}}#LMNOPQRS ##thx.flagitious!## TUVWXY/.i rescue##/ 3141592653589793+ +271828182845904; 9876543210;;eval "x=((42737-eval. sum)%256).chr;;eval .scan(//){a=$`+x+$' a.unpack('H*')[0].hex%999989==68042&&eval(a)}#"##" eval eval#### (C) Copyright 2014 Yusuke Endoh ####
  3. 余談:放射線耐性 Quine チャレンジ • これまで放射線耐性 Quine を達成した言語 • 2014: Ruby

    (by me) • 2014: Perl (by @shinh) • 2024: JavaScript (by @Yuk3u) • いわゆる「型がない言語」ばかり • 型はないほうが創造性が高い(?) • 「型がある言語」でのチャレンジャー求む ※ 0 バイトで Quine と主張するのは除く
  4. Yusuke Endoh (@mametter) • 『型システム入門』翻訳者のひとり • Types and Programming Languages

    (TAPL) の日本語版 • Benjamin C. Pierce 著 • 住井英二郎 監訳 • 遠藤侑介、酒井政裕、今井敬吾、 黒木裕介、今井宜洋、才川隆文、 今井健男 訳
  5. 今日の話題:型検査器を自作してみよう • ゴール:型検査器のブートストラップ • 型システムの一面を理解する演習としてオススメ • なにより、楽しい! • 今日は TypeScript

    サブセットでの事例を紹介します • 型検査の対象も、型検査器の実装も TypeScript サブセット • どんな言語でも必要になる考え方だけ説明します
  6. 話の流れ 1. 最小の型検査器を作る • 真偽値型と数値型だけ 2. 型検査器がサポートする言語機能を順次増やしていく • 関数と変数、再帰関数 •

    再帰型 • その他もろもろ(TypeScript 特有の話が多いのでほぼ割愛) 3. 型検査器の実装に使っているすべての言語機能を サポートできたら完成
  7. 真偽値と数値 • 次をサポートする型検査器を作りたい • リテラル: true 、false 、1 、2 、100

    … • 足し算: 1 + 2 、(1 + 2) + (3 + 4) • 条件分岐: true ? 1 : 2 • 引き算や掛け算などはサポートしない • 足し算とやることは変わらない • 型検査器のブートストラップに不要だったので…… t ::= true | false | 0 | 1 | … | t + t | t ? t : t
  8. 今回の型検査器で検査すること 1. 真偽値を足し算していないこと • OK: 1 + 2 • NG:

    1 + true 、true + false 2. 条件演算子の条件式が真偽値であること • OK: true ? 1 : 2 • NG: 123 ? 1 : 2 3. 条件演算子の返す型が一致していること • OK: true ? 1 : 2 • NG: true ? 1 : true
  9. AST の例 • 足し算 • 条件演算子 (1 + 2) +

    3 プログラム add num 1 num 2 num 3 add left right right left 抽象構文木(AST) { tag: "add", left: { tag: "add", left: { tag: "num", n: 1 }, right: { tag: "num", n: 2 } }, right: { tag: "num", n: 3 } } 実際のデータ構造 = = { tag: "if", cond: { tag: "true" }, thn: { tag: "true" }, els: { tag: "false " } } true true if cond thn false els true ? true : false = =
  10. パーサ(構文解析器) • プログラム文字列を AST に変換する機能 • 今回は tiny-ts-parser という npm

    パッケージを使う import { parseArith } from "npm:tiny-ts-parser"; parseArith("1 + 2") //=> { // tag: "add", // left: { tag: "number", n: 1 }, // right: { tag: "number", n: 2 } // }
  11. 型検査器の実装で使う型の定義 • ASTを表す型 • 「型」を表す型 • 真偽値の型は "Boolean" という文字列で表現する •

    数値の型は "Number" という文字列で表現する type Term = | { tag:"true" } | { tag:"false" } | { tag:"number"; n:number } | { tag:"if"; cond:Term; thn:Term; els:Term } | { tag:"add"; left:Term; right:Term }; type Type = "Boolean" | "Number";
  12. 型検査器の本体、typecheck 関数 • AST を受け取り、そのASTが返す型の値を返す • つまり "Boolean" または "Number"

    を返す • 型エラーを見つけたときは例外を投げる export function typecheck(t: Term): Type { … }
  13. typecheck 関数の動作例 • 「true」の AST を受け取ったら "Boolean" を返す • 「1

    + 2」の AST を受け取ったら "Number" を返す • 型エラーを見つけたら例外を投げる typecheck(parseArith("1 + true")) //=> Error: number expected typecheck({ tag: "true" }) //=> "Boolean" typecheck(parseArith("1 + 2")) //=> "Number" typecheck(parseArith("true")) //=> "Boolean"
  14. typecheckの実装:大枠 • 構文の種類ごとに処理する export function typecheck(t: Term): Type { switch

    (t.tag) { case "true": { … } case "false": { … } case "number": { … } case "add": { … } case "if": { … } } }
  15. typecheckの実装:リテラルの実装 • リテラルは、対応する型を返すだけ export function typecheck(t: Term): Type { switch

    (t.tag) { case "true": return "Boolean"; case "false": return "Boolean"; case "number": return "Number"; case "add": { … } case "if": { … } } } あとはこの2つ
  16. 両方とも "Number" なら OK typecheck( ) typecheckの実装:add の実装 • left

    と right に再帰的に typecheck を適用し、 number 型になることを確認する(ちがったら例外) add left right L R typecheck( ) //=> "Number" L typecheck( ) //=> "Number" R
  17. typecheckの実装:add の実装 • コードで書くと case "add": { // t.leftにtypecheckを適用し、number型じゃなかったら例外 const

    leftTy = typecheck(t.left); if (leftTy !== "Number") throw "number expected"; // rightも同様 const rightTy = typecheck(t.right); if (rightTy !== "Number") throw "number expected"; return "Number"; // OKならnumber型を返す }
  18. typecheckの実装:if の実装 • cond が boolean 型になること、thn と els が同じ型に

    なることを確認する(ちがったら例外) typecheck( ) typecheck( ) //=> "Boolean" C C T E if cond thn els typecheck( ) //=> ? E typecheck( ) //=> ? T "Boolean" なら OK 同じなら OK
  19. typecheckの実装:if の実装 • コードで書くと case "if": { // t.condにtypecheckを適用し、boolean型じゃなかったら例外 const

    condTy = typecheck(t.cond); if (condTy !== "Boolean") throw "boolean expected"; // t.thnとt.elsのtypecheck結果がちがったら例外 const thnTy = typecheck(t.thn); const elsTy = typecheck(t.els); if (thnTy !== elsTy) throw "then and else have different types"; return thnTy; // OKならt.thnのtypecheck結果を返す }
  20. 型検査器の完成! • ほんの 30 行ほどで 型検査器が書けた type Type = "Boolean"

    | "Number"; type Term = | { tag: "true" } | { tag: "false" } | { tag: "if"; cond: Term; thn: Term; els: Term } | { tag: "number"; n: number } | { tag: "add"; left: Term; right: Term }; export function typecheck(t: Term): Type { switch (t.tag) { case "true": return "Boolean"; case "false": return "Boolean"; case "number": return "Number"; case "if": { const condTy = typecheck(t.cond); if (condTy !== "Boolean") throw "boolean expected"; const thnTy = typecheck(t.thn); const elsTy = typecheck(t.els); if (thnTy !== elsTy) throw "then and else have different types"; return thnTy; } case "add": { const leftTy = typecheck(t.left); if (leftTy !== "Number") throw "number expected"; const rightTy = typecheck(t.right); if (rightTy !== "Number") throw "number expected"; return "Number"; } } }
  21. 型検査器の動作確認 console.log(typecheck(parseArith("(1 + 2) + 3"))); //=> "Number" console.log(typecheck(parseArith("true ?

    true : false"))); //=> "Boolean" typecheck(parseArith("true ? 1 : false")); //=> error: then and else have different types
  22. 関数と変数 • 型検査器に次のサポートを追加したい • 変数参照: x 、y 、z … •

    無名関数: (x: number) => x • 関数呼び出し: f(42) 、f(true) • 変数参照の AST はそのまま • 例:x の AST { tag: "var", name: "x" } ※ついでに const 宣言と複文も入れるけど、簡単なので説明は省略
  23. 関数の AST の例 • 無名関数 • 関数呼び出し (x: number) =>

    x { tag: "func", params: [ { name: "x", type: { tag: "Number" } } ], body: { tag: "var", name: "x" } } x: number var x func params body = = foo(42) var foo num 42 call func args { tag: "call", func: { tag: "var", name: "foo" }, args: [{ tag: "number", n: 42 }] } = =
  24. 型検査器で使う型の定義:ASTの型 type Term = … // これまでと同じ | { tag:

    "var"; name: string } | { tag: "func"; params: Param[]; body: Term } | { tag: "call"; func: Term; args: Term[] }; type Param = { name: string; type: Type };
  25. 型検査器で使う型の定義:「型」の型 • 関数型の導入により、型も構造を持つようになる type Type = | { tag: "Boolean"

    } | { tag: "Number" } | { tag: "Func"; params: Param[]; retType: Type }; type Param = { name: string; type: Type }; 関数型にあわせて { tag: … } でくるんだ
  26. 関数型の構造例 () => number なし Func params retType Number {

    tag: "Func", params: [], retType: { tag: "Number" } } = = (x: boolean) => number { tag: "Func", params: [ { name: "x", type: { tag: "Boolean" } } ], retType: { tag: "Number" } } = = x: Boolean Number Func params retType
  27. typecheckの実装:大枠 export function typecheck(t: Term): Type { switch (t.tag) {

    case "true": { … } case "false": { … } case "number": { … } case "if": { … } case "add": { … } case "var": { … } case "func": { … } case "call": { … } } } すでに作ったのと ほぼ同じ いまから書く
  28. typecheckの実装:変数参照の実装 • 変数の型は文脈によって変わる • の中の x なら number 型 •

    の中の x なら boolean 型 • 型検査器でも「文脈」を扱う必要がある (x: number) => x (x: boolean) => x case "var": { … } (いまのままでは) 書けない!
  29. typecheckの実装:無名関数の実装 • 引数の変数を型環境に追加したうえで、 関数の中身を再帰的にtypecheckする • の例 typecheck( ,{…}) x: number

    func params body B typecheck( ,{…, x: }) B Number (x: number) => ... 1. 型環境をコピーしつつ 2. x: number を追加 3. 拡張した型環境で関数の中身をtypecheckする
  30. typecheckの実装:無名関数の実装 case "func": { // 型環境をコピーして追加する let newTyEnv = tyEnv;

    for (const param of t.params) { newTyEnv = { ...newTyEnv, [param.name]: param.type }; } // 関数の中身を再帰的に typecheck する const retType = typecheck(t.body, newTyEnv); // 関数型を返す return { tag: "Func", params: t.params, retType }; }
  31. typecheckの実装:関数呼び出しの実装 • 呼び出す対象が関数型であることを確認する • 引数の数や型が一致することを確認する • 例: typecheck( ) typecheck(

    ) //=> F foo(…) call func args F A x: ? ? Func params retType typecheck( ) //=> A ? 実引数の数と型、 仮引数の数と型、 が一致してたら OK 関数型なら OK
  32. typecheckの実装:関数呼び出しの実装 case "call": { const funcTy = typecheck(t.func, tyEnv); if

    (funcTy.tag !== "Func") throw "function type expected"; if (funcTy.params.length !== t.args.length) throw "wrong number of arguments"; for (let i = 0; i < t.args.length; i++) { const argTy = typecheck(t.args[i], tyEnv); if (!typeEq(argTy, funcTy.params[i].type)) throw "parameter type mismatch"; } return funcTy.retType; }
  33. 関数と変数の対応完了 • 100 行くらいで関数や変数をサポートできた • ついでに const 宣言と複文も console.log(typecheck(parseBasic("() =>

    1"))); //=> { tag: "Func", params: [], body: { tag: "Number" } } console.log(typecheck(parseBasic("( (x: number) => x )(42)"))); //=> { tag: "Number" } console.log(typecheck(parseBasic("( (x: number) => x )(true)"))); //=> parameter type mismatch
  34. 余談:TypeScript の再帰関数の宣言 • 実行すると、実行時エラー! const f = (): number =>

    g(); f(); //=> Cannot access 'g' before initialization const g = (): number => f();
  35. 余談:TypeScriptはなぜ型安全ではない? • 解決できないか? • たとえば再帰関数定義の間で 書ける式を制限すれば 解決できそう(多分) • だが、既存 JavaScript

    コードの TypeScript 移植が面倒になる • コールバックの多い JavaScript ではこういう相互再帰は結構ある • TypeScript は型安全性よりも移植の簡単さを優先した? • JavaScript には未定義動作がないので、悪くない妥協 const f = (): number => g(); f(); const g = (): number => f(); これは禁止
  36. ダイジェスト:function 文の AST の例 function foo(x: number): number { return

    x; } foo(42); { tag: "recFunc", funcName: "foo", params: [{ name:"n", type: { tag:"Number" } }], retType: { tag: "Number" }, body: { tag: "var", name: "n" }, rest: { tag: "call", func: { tag: "var", name: "foo" }, args: [{ tag: "number", n: 42 }], }, } = = x: number var x recFunc foo params body var foo num 42 call func args rest
  37. ダイジェスト:typecheckのfunction文の実装 • 引数の変数に加え、関数自身を型環境に追加する • 関数の中身 の文脈では、変数 x と foo 自身が参照できる

    • function 文の後の式 の文脈では、変数 foo が参照できる typecheck( ,{…}) typecheck( ,{…, x: , foo: }) B number number => number x: number recFunc foo params body rest B R typecheck( ,{…, foo: }) R number => number B R
  38. 再帰型の表現 • 普通の関数型 • 再帰型 type T = () =>

    number; なし Func params retType Number { tag: "Func", params: [], retType: { tag: "Number" } } = = なし Func params retType なし Func params retType なし Func params retType Func params retType =? type T = () => T; = 循環するデータは 扱いにくい
  39. 再帰型の表現 • 普通の関数型 • 再帰型 type T = () =>

    number; なし Func params retType Number { tag: "Func", params: [], retType: { tag: "Number" } } = = type T = () => T; Rec type なし Func params retType Var = = { tag: "Rec", type: { tag: "Func", params: [], retType: { tag: "TypeVar" }, }, } 循環の起点 循環する位置
  40. 再帰型の展開 • Rec を消して、Var の部分に全体を埋め込む Rec type なし Func params

    retType Var Rec なし Func params retType Rec type なし Func params retType Var 展開
  41. 型の等価性判定 typeEq: 再帰型の対応 // 再帰型だったら展開する関数 function simplifyType(ty: Type): Type {

    // 実装略 } // 型の等価性判定 function typeEq(ty1: Type, ty2: Type): boolean { // どちらかが再帰型なら、展開してから比較する if (ty1.tag === "Rec") return typeEq(simplifyType(ty1), ty2); if (ty2.tag === "Rec") return typeEq(ty1, simplifyType(ty2)); // どちらも再帰型でないなら再帰的に比較する、実装略 } これだと停止しない!
  42. 型の等価性判定 typeEq: 再帰型の対応 // 再帰型だったら展開する関数 function simplifyType(ty: Type): Type {

    // 実装略 } // 型の等価性判定 function typeEq(ty1: Type, ty2: Type, seen: [Type, Type][]): boolean { // [ty1, ty2] が seen に含まれていたら、等しいとする if (seen.some(...)) return true; // どちらかが再帰型なら、展開してから比較する if (ty1.tag === "Rec") return typeEq(simplifyType(ty1), ty2, [...seen, [ty1, ty2]]); if (ty2.tag === "Rec") return typeEq(ty1, simplifyType(ty2), [...seen, [ty1, ty2]]); // どちらも再帰型でないなら再帰的に比較する、実装略 } まったく同じ比較を 繰り返しそうになったら 止める
  43. 再帰型の対応完了! • 再帰型は typeEq 関数の変更だけで対応できる • typecheck 関数への変更は(ほとんど)不要(!) • こんなコードの型検査ができる

    • 型検査器のブートストラップに必須の道具は揃った! type Hungry = (x: number) => Hungry; (f: Hungry) => f(0)(1)(2)(3)(4)(5);
  44. 細かい機能をどんどん実装する • 型検査器の実装で使ってる言語機能を全部サポートする • このあたりは言語ごとに様々だと思うのでばっさり省略 • むずかしい言語機能を避けて型検査器を書くのも良し • 言語機能の選び方(サブセット言語の設計力)が問われる const

    文 複文 let 文 変数代入 文字列リテラル 比較演算 for文 配列型とその演算 Record型とその演算 オブジェクト型とその演算 バリアント型(タグ付きunion型)とその演算 undefined型(最小限の部分型付け)
  45. さらなる発展の方向性 • 言語機能と型の機能をリッチにしていく • 部分型付け • ジェネリクス • 型推論 •

    相互再帰関数のサポート • パーサも自作して純粋なブートストラップを目指す
  46. 今日の内容が簡単すぎた人は • Ruby の型システムの開発にご協力ください! • Steep, Sorbet: 伝統的な型システム+漸進的型付けベース • TypeProf:

    データフローの差分解析ベース • TypeProf は関数呼び出しから型推論する! • 関数呼び出し があったら • 関数定義 の x が Integer だと推論する • whole program analysis だけど差分解析により意外とスケール • 興味あったら是非遊んでみて foo(42) def foo(x)