5 分ではわからない HM 型推論 - 型システム祭りオンライン 2020 4/17

型システムについての議論は ML 言語系の表現と数学的な定式化の表現が基本的に必要になってきます。しかし、その見た目はものものしくてちょっと腰が引けてしまいます。そこで、ごく簡単に ML / HM 型システムについて概略的に入門してみようと思います。

Transcript

1. 5 分ではわからない HM 型推論 Biacco42
2. お話すること • 対象言語であることが多い ML の構文のごく簡単な説明 • 型システムに関する表現の ごく簡単な説明 • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
3. お話すること • 対象言語であることが多い ML の構文のごく簡単な説明 • 型システムに関する表現の ごく簡単な説明 • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
4. 5 分では説明しようがなかった なのでだいぶ天下りな説明をします
5. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？
6. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 全ては式でありある値に評価できる
7. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 変数宣言みたいなやつ
8. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ in の後ろで別名が使える
9. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 関数定義
10. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 引数
11. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 本体 (式) 引数をパラメタとして使える
12. 問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int
13. 問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int
14. 問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int `fun x -> x + 1` よりこの式全体の型は f: int -> int
15. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 問：この式の返す値の型は？
16. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool
17. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
18. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
19. ？？？？？？？
20. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現
21. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説)
22. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け
23. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け 型代入 (Substitution)
24. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け 型代入 (Substitution) これがしたい
25. 型変数と型スキームと型環境 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 型環境 Γ のもとで
26. 型変数と型スキームと型環境 型環境 Γ のもとで項 e が型変数 σ に型付けできる
27. 型変数と型スキームと型環境
28. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or
29. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or 型スキーム
30. 補：型スキーム α は全称量化された型変数 型スキームの引数のようなもの
31. 補：型スキーム σ は型スキームの実体 ex: α -> α
32. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or 型スキーム
33. 型変数と型スキームと型環境 Γ は空集合 or σ は τ (型変数・型コンストラクタ) or 型スキーム
34. 型変数と型スキームと型環境 Γ は空集合 or Γ に x: σ の型スキームを 加えたもの (再帰的定義) σ は τ (型変数・型コンストラクタ) or 型スキーム
35. 型変数と型スキームと型環境 項 e は型環境 Γ によって提供される ある型変数 x を型スキーム σ’ として与えた場合に 型 (スキーム) σ に評価できる
36. σ って具体的な型なの？
37. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の (free でない) 型変数を τ i に置き換える
38. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の (free でない) 型変数を τ i に置き換える 型環境に型代入 S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる
39. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の (free でない) 型変数を τ i に置き換える 型環境に型代入 S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる いい感じの型代入 S を見つけると具体的な型が定まる
40. 【再掲】問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int `fun x -> x + 1` よりこの式全体の型は f: int -> int
41. 【再掲】問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int `fun x -> x + 1` よりこの式全体の型は f: int -> int 型に関する連立方程式としてみれる = 型の仮定を置き換えていく = 連立方程式を解く型代入 S をさがす！
42. 型付けのアルゴリズム：項の定義 abstract class Term {} case class Var(x: String) extends Term {} case class Lam(x: String, e: Term) extends Term {} case class App(f: Term, e: Term) extends Term {} case class Let(x: String, e: Term, f: Term) extends Term {}
43. 型付けのアルゴリズム：項の定義 abstract class Term {} case class Var(x: String) extends Term {} 型変数 case class Lam(x: String, e: Term) extends Term {} case class App(f: Term, e: Term) extends Term {} case class Let(x: String, e: Term, f: Term) extends Term {}
44. 型付けのアルゴリズム：項の定義 abstract class Term {} case class Var(x: String) extends Term {} case class Lam(x: String, e: Term) extends Term {} ラムダ式 case class App(f: Term, e: Term) extends Term {} case class Let(x: String, e: Term, f: Term) extends Term {}
45. 型付けのアルゴリズム：項の定義 abstract class Term {} case class Var(x: String) extends Term {} case class Lam(x: String, e: Term) extends Term {} case class App(f: Term, e: Term) extends Term {} 関数適用 case class Let(x: String, e: Term, f: Term) extends Term {}
46. 型付けのアルゴリズム：項の定義 abstract class Term {} case class Var(x: String) extends Term {} case class Lam(x: String, e: Term) extends Term {} case class App(f: Term, e: Term) extends Term {} case class Let(x: String, e: Term, f: Term) extends Term {} let 式
47. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1)
48. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 式の AST を手繰る
49. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 再帰的な項の探索
50. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 単一化 再帰的な項の探索
51. 単一化？
52. 単一化：HM 型システムの中心 def unifier(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => s case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => unifier(u, t, s) } case (Arrow(t1, t2), Arrow(u1, u2)) => unifier(t1, u1, unifier(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (ts zip us).foldLeft(s)((s, tu) => unifier(tu._1, tu._2, s)) case _ => throw new TypeError 型代入 S の元で型変数 t と u が同じになるような より拡張した型代入 S’ を探す = 単一化
53. 単一化：HM 型システムの中心 def unifier(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => s case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => unifier(u, t, s) } case (Arrow(t1, t2), Arrow(u1, u2)) => unifier(t1, u1, unifier(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (ts zip us).foldLeft(s)((s, tu) => unifier(tu._1, tu._2, s)) case _ => throw new TypeError 同じ型変数ならなにもしない
54. 単一化：HM 型システムの中心 def unifier(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => s case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => unifier(u, t, s) } case (Arrow(t1, t2), Arrow(u1, u2)) => unifier(t1, u1, unifier(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (ts zip us).foldLeft(s)((s, tu) => unifier(tu._1, tu._2, s)) case _ => throw new TypeError 片方が型変数のときそれを相手の型での置き換えるように 型環境を拡張する
55. 単一化：HM 型システムの中心 def unifier(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => s case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => unifier(u, t, s) } case (Arrow(t1, t2), Arrow(u1, u2)) => unifier(t1, u1, unifier(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (ts zip us).foldLeft(s)((s, tu) => unifier(tu._1, tu._2, s)) case _ => throw new TypeError 関数適用ならそれぞれの引数と返り値が同じになるように 型代入を拡張する
56. 単一化：HM 型システムの中心 def unifier(t: Type, u: Type, s: Subst): Subst = (s(t), s(u)) match { case (Tyvar(a), Tyvar(b)) if (a == b) => s case (Tyvar(a), _) if !(tyvars(u) contains a) => s.extend(Tyvar(a), u) case (_, Tyvar(a)) => unifier(u, t, s) } case (Arrow(t1, t2), Arrow(u1, u2)) => unifier(t1, u1, unifier(t2, u2, s)) case (Tycon(k1, ts), Tycon(k2, us)) if (k1 == k2) => (ts zip us).foldLeft(s)((s, tu) => unifier(tu._1, tu._2, s)) case _ => throw new TypeError 型コンストラクタならそれぞれの要素の型が同一になるよう 型環境を拡張
57. 【再掲】型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 単一化 再帰的な項の探索
58. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 項を手繰りながら 連立方程式を立てつつ => 単一化で再帰的に解く
59. 【再掲】問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
60. let 多相 let id = fun x -> x in If id false then 1 else id 2 let 式においてのみ型変数の多相性を許す
61. let 多相 let id = fun x -> x in If id false then 1 else id 2 let 式においてのみ型変数の多相性を許す => 実はすでに登場している型スキーマの 　 全称量化された型変数がこれ
62. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) 型スキームのインスタンス化
63. 型スキームのインスタンス化 全称量化された型変数に具体的な型を適用する ∀α.α -> α　=>　'a -> 'a　　とか ∀α.α -> α　=>　int -> int
64. 型付けのアルゴリズム：S を探す def tp(env: Env, e: Term, t: Type, s: Subst): Subst = { e match { case Var(x) => // 型変数の場合 val u = lookup(env, x) unifier(u.newInstance, t, s) case Lam(x, e1) => // ラムダ式 val a, b = newTyvar() val s1 = unifier(t, Arrow(a, b), s) val env1 = {x, TypeScheme(List(), a)} :: env tp(env1, e1, b, s1) } case App(e1, e2) => // 関数適用 val a = newTyvar() val s1 = tp(env, e1, Arrow(a, t), s) tp(env, e2, a, s1) case Let(x, e1, e2) => // let 式 val a = newTyvar() val s1 = tp(env, e1, a, s) tp({x, gen(env, s1(a))} :: env, e2, t, s1) newInstance は全称量化された型変数を ある型変数に固定したコピーを作ってからから単一化する
65. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id instance #1` は bool -> bool `id instance #2` は int -> int twemoji by Twitter CC BY 4.0
66. Ref プログラミング言語の基礎概念 [五十嵐淳 サイエンス社 2011] Hindley–Milner type system - Wikipedia https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Substitution_in_typings 第 16 章 Hindley/Milner 型推論 - プログラミング言語 Scala 日本語情報サイト https://sites.google.com/site/scalajp/home/documentation/scala-by-example/chapter16 Hindley-Milner型推論アルゴリズムを Groovyで書いてみた http://uehaj.hatenablog.com/entry/2014/02/01/183039 人でもわかる型推論 https://qiita.com/uint256_t/items/7d8c8feeffc03b388825
67. end twemoji by Twitter CC BY 4.0
68. @Biacco42