5 分ではわからない HM 型推論 - わいわいswiftc 2020 4/20

1. 5 分ではわからない HM 型推論 in わいわいswiftcオンライン Biacco42
2. 4/17 に行われた 型システム祭りオンライン での LT 発表の拡大版になります。 https://opt.connpass.com/event/169724/
3. プログラミング言語の基礎概念 [五十嵐淳 サイエンス社 2011] だいたいこれの 8 章 〜 10 章 https://amzn.to/2XOsC4N
4. お話すること • 型システムの具体的実装例であ ることが多い ML の構文の ごく簡単な説明 • 型システムに関する表現の ごく簡単な説明 • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
5. お話すること • 型システムの具体的実装例であ ることが多い ML の構文の ごく簡単な説明 • 型システムに関する表現の ごく簡単な説明 • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
6. 5 分では説明しようがなかった なのでだいぶ天下り・省略した説明をして ML や型システムに関する文章が 雰囲気で読めるところを目指す
7. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？
8. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ ML 風の式 全ては式でありある値に評価できる
9. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 変数宣言みたいなやつ
10. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ in の後ろで別名が使える
11. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 関数定義
12. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 引数
13. 問題：自動で型をつけたい let f = fun x -> x + 1 in f 問：この式の返す値の型は？ 本体 (式) 引数をパラメタとして使える
14. 問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int
15. 問題：自動で型をつけたい let f = fun x -> x + 1 in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int
16. 問題：自動で型をつけたい 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
17. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 問：この式の返す値の型は？
18. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool
19. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
20. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system
21. ？？？？？？？
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) の表現 型変数 (型推論中の仮説)
24. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け
25. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け 型代入 (Substitution)
26. 型推論の定式化 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 項 (Exp) の表現 型変数 (型推論中の仮説) 型環境と型付け 型代入 (Substitution) これがしたい
27. 型変数と型スキームと型環境 https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system 型環境 Γ のもとで
28. 型変数と型スキームと型環境 型環境 Γ のもとで項 e が型変数 σ に型付けできる
29. 型変数と型スキームと型環境
30. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or
31. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or 型スキーム
32. 補：型スキーム α は全称量化された型変数 型スキームの引数のようなもの
33. 補：型スキーム σ は型スキームの実体 ex: α -> α つまりはだいたい λ 抽象と同じ
34. 型変数と型スキームと型環境 σ は τ (型変数・型コンストラクタ) or 型スキーム
35. 型変数と型スキームと型環境 Γ は空集合 or σ は τ (型変数・型コンストラクタ) or 型スキーム
36. 型変数と型スキームと型環境 Γ は空集合 or Γ に x: σ の型スキームを 加えたもの (再帰的定義) σ は τ (型変数・型コンストラクタ) or 型スキーム
37. 型変数と型スキームと型環境 項 e は型環境 Γ によって提供されるある型変数 x を 型スキーム σ’ として与えた場合に 型 (スキーム) σ に評価できる
38. σ って具体的な型なの？
39. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の 型変数を τ i に置き換える
40. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の 型変数を τ i に置き換える 型環境に型代入 S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる
41. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の 型変数を τ i に置き換える 型環境に型代入 S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる いい感じの型代入 S を見つけると具体的な型が定まる
42. 【再掲】問題：自動で型をつけたい 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
43. 【再掲】問題：自動で型をつけたい 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 をさがす！
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 {}
47. 型付けのアルゴリズム：項の定義 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 {}
48. 型付けのアルゴリズム：項の定義 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 式
49. 型付けのアルゴリズム：項の定義 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 式 ex: λx. cons x nil = Lam("x", App(App(Var("cons"), Var("x")), Var("nil")))
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. 型付けのアルゴリズム：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 を手繰る
52. 型付けのアルゴリズム：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) 再帰的な項の探索
53. 型付けのアルゴリズム：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) 連立方程式 e1: a -> t の導入
54. 型付けのアルゴリズム：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) 単一化 再帰的な項の探索
55. 単一化？
56. 型付けのアルゴリズム：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) 単一化 = 連立方程式の両辺が等しくなる解を探す
57. 単一化：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’ を探す = 単一化
58. 単一化：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 同じ型変数ならなにもしない
59. 単一化：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 片方が型変数のときそれを相手の型での置き換えるように 型環境を拡張する
60. 単一化：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 関数適用ならそれぞれの引数と返り値が同じになるように 型代入を拡張する
61. 単一化：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 型コンストラクタならそれぞれの要素の型が同一になるよう 型環境を拡張
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. 型付けのアルゴリズム：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) 項を手繰りながら 連立方程式を立てつつ => 単一化で再帰的に解く
64. 【再掲】問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
65. let 多相 let id = fun x -> x in If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す
66. let 多相 let id = fun x -> x in If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す => 実はすでに登場している型スキーマの 　 全称量化された型変数がこれ
67. let 多相 let id = fun x -> x in If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す => 実はすでに登場している型スキーマの 　 全称量化された型変数がこれ 'a -> 'a　==>　∀α.α -> α
68. 型スキームのインスタンス化 全称量化された型変数に具体的な型を適用すること ∀α.α -> α　=>　'a -> 'a　　とか ∀α.α -> α　=>　int -> int
69. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α -> τ} のとき SΓ は？ 　　∀α.α -> 'b　=>　∀τ.τ -> 'b　？
70. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α -> τ} のとき SΓ は？ 　　∀α.α -> 'b　=>　∀τ.τ -> 'b　？
71. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α -> τ} のとき SΓ は？ S{α -> τ} ∀α.α -> 'b => S{'a -> τ} ∀'a.'a -> 'b => S{'a -> τ} 'a -> 'b => τ -> 'b 置き換える型変数の名前を変更しても意味は変わらない => α変換
72. 型付けのアルゴリズム：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) 型スキームのインスタンス化
73. 型付けのアルゴリズム：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 は全称量化された型変数を ある型変数に固定したコピーを作ってからから単一化する
74. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id instance #1` は 'a -> 'a `id instance #2` は 'b -> 'b twemoji by Twitter CC BY 4.0
75. 問題：自動で型をつけたい (2) let id = fun x -> x in If id false then 1 else id 2 `id instance #1` は 'a -> 'a => bool -> bool `id instance #2` は 'b -> 'b => int -> int twemoji by Twitter CC BY 4.0
76. 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
77. end twemoji by Twitter CC BY 4.0
78. @Biacco42