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

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

Biacco42
April 20, 2020

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

Biacco42

April 20, 2020
Tweet

More Decks by Biacco42

Other Decks in Programming

Transcript

  1. お話すること • 型システムの具体的実装例であ ることが多い ML の構文の ごく簡単な説明 • 型システムに関する表現の ごく簡単な説明

    • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
  2. お話すること • 型システムの具体的実装例であ ることが多い ML の構文の ごく簡単な説明 • 型システムに関する表現の ごく簡単な説明

    • HM 型推論のざっくりした アルゴリズム • let 多相の実現法の概念 • ML の導出・推論規則 • 定理と証明 • 具体的な実装 しないこと
  3. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は?
  4. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? ML 風の式 全ては式でありある値に評価できる
  5. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? 変数宣言みたいなやつ
  6. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? in の後ろで別名が使える
  7. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? 関数定義
  8. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? 引数
  9. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f 問:この式の返す値の型は? 本体 (式) 引数をパラメタとして使える
  10. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f `+` は int -> int -> int => x: int
  11. 問題:自動で型をつけたい let f = fun x -> x + 1

    in f `+` は int -> int -> int => x: int `x + 1` より fun x -> x + 1: int -> int
  12. 問題:自動で型をつけたい 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
  13. 問題:自動で型をつけたい (2) let id = fun x -> x in

    If id false then 1 else id 2 問:この式の返す値の型は?
  14. 問題:自動で型をつけたい (2) let id = fun x -> x in

    If id false then 1 else id 2 `id` は bool -> bool
  15. 問題:自動で型をつけたい (2) let id = fun x -> x in

    If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
  16. 型変数と型スキームと型環境 Γ は空集合 or Γ に x: σ の型スキームを 加えたもの

    (再帰的定義) σ は τ (型変数・型コンストラクタ) or 型スキーム
  17. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の 型変数を τ i に置き換える 型環境に型代入

    S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる
  18. 型代入 (Substitution) 型代入 S は型環境や型スキーム中の 型変数を τ i に置き換える 型環境に型代入

    S を適用した型環境では 項 e が型代入 S を適用した型 (スキーム) Sσ に型付けできる いい感じの型代入 S を見つけると具体的な型が定まる
  19. 【再掲】問題:自動で型をつけたい 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
  20. 【再掲】問題:自動で型をつけたい 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 をさがす!
  21. 型付けのアルゴリズム:項の定義 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 {}
  22. 型付けのアルゴリズム:項の定義 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 {}
  23. 型付けのアルゴリズム:項の定義 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 {}
  24. 型付けのアルゴリズム:項の定義 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 {}
  25. 型付けのアルゴリズム:項の定義 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 式
  26. 型付けのアルゴリズム:項の定義 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")))
  27. 型付けのアルゴリズム: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)
  28. 型付けのアルゴリズム: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 を手繰る
  29. 型付けのアルゴリズム: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) 再帰的な項の探索
  30. 型付けのアルゴリズム: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 の導入
  31. 型付けのアルゴリズム: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) 単一化 再帰的な項の探索
  32. 型付けのアルゴリズム: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) 単一化 = 連立方程式の両辺が等しくなる解を探す
  33. 単一化: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’ を探す = 単一化
  34. 単一化: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 同じ型変数ならなにもしない
  35. 単一化: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 片方が型変数のときそれを相手の型での置き換えるように 型環境を拡張する
  36. 単一化: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 関数適用ならそれぞれの引数と返り値が同じになるように 型代入を拡張する
  37. 単一化: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 型コンストラクタならそれぞれの要素の型が同一になるよう 型環境を拡張
  38. 【再掲】型付けのアルゴリズム: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) 単一化 再帰的な項の探索
  39. 型付けのアルゴリズム: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) 項を手繰りながら 連立方程式を立てつつ => 単一化で再帰的に解く
  40. 【再掲】問題:自動で型をつけたい (2) let id = fun x -> x in

    If id false then 1 else id 2 `id` は bool -> bool `id` は bool -> bool
  41. let 多相 let id = fun x -> x in

    If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す
  42. let 多相 let id = fun x -> x in

    If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す => 実はすでに登場している型スキーマの   全称量化された型変数がこれ
  43. let 多相 let id = fun x -> x in

    If id false then 1 else id 2 let 式においてのみ型変数の多相性の伝搬を許す => 実はすでに登場している型スキーマの   全称量化された型変数がこれ 'a -> 'a ==> ∀α.α -> α
  44. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α

    -> τ} のとき SΓ は?   ∀α.α -> 'b => ∀τ.τ -> 'b ?
  45. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α

    -> τ} のとき SΓ は?   ∀α.α -> 'b => ∀τ.τ -> 'b ?
  46. 型スキームのインスタンス化 (2) Γ が ∀α.α -> 'b のもとで S {α

    -> τ} のとき SΓ は? S{α -> τ} ∀α.α -> 'b => S{'a -> τ} ∀'a.'a -> 'b => S{'a -> τ} 'a -> 'b => τ -> 'b 置き換える型変数の名前を変更しても意味は変わらない => α変換
  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) newInstance は全称量化された型変数を ある型変数に固定したコピーを作ってからから単一化する
  49. 問題:自動で型をつけたい (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
  50. 問題:自動で型をつけたい (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
  51. 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