Welcome to the "Parametricity" 🏙️ − Generic だけど Specific な世界 −

このスライドは、2026/07/12「関数型まつり 2026」で発表したものです。

cf. https://fortee.jp/2026fp-matsuri/proposal/310a9a71-f65b-4ad1-a6d6-81878923cfb3

Transcript

1. Welcome to the "Parametricity" 🏙️ − Generic だけど Specific な世界 − #関数型まつり 2026 — @Guvalif (TAKASE Kazuyuki)
2. 自己紹介 - 高瀬 和之 (TAKASE Kazuyuki) 𝕏：@Guvalif 余談) ScalaMatsuri 2020 ぶりの登壇です 💪 Profile { works = [ "IoT エンジニア", "フロントエンド・エンジニア", "開発人事", "TechPM (← 現職)", "エンジニア育成 (← 複業)" ], memo = "関数型 XXX を名乗りがち 😗" }
3. 関数型プログラミングに対する私の立ち位置 🧑‍🏫 良い設計を発見する ための、ベース知識として用いる 安全な開発を実現する ための、勘所として用いる これらは決してプログラミング言語に依存すること無く、 普遍的に応用可能 だと考える
4. アイスブレイク："Parametricity"，知ってる？
5. アイスブレイク："Parametricity"，知ってる？ 初めて聞く 👂
6. アイスブレイク："Parametricity"，知ってる？ 初めて聞く 👂 聞いたことはあるが、中身は知らない 🤔
7. アイスブレイク："Parametricity"，知ってる？ 初めて聞く 👂 聞いたことはあるが、中身は知らない 🤔 理論的背景も含めて知っている ✌️
8. アイスブレイク："Parametricity"，知ってる？ 初めて聞く 👂 聞いたことはあるが、中身は知らない 🤔 理論的背景も含めて知っている ✌️ 住んでいる 🏙️
9. アイスブレイク："Parametricity"，知ってる？ 初めて聞く 👂 聞いたことはあるが、中身は知らない 🤔 理論的背景も含めて知っている ✌️ 住んでいる 🏙️
10. I. (パラメトリック) 多相型
11. 多相型のモチベーション (1) 配列に対する head 関数を考える もし 多相型が無い 場合、次のようなことが起こる： const headN: (_: number[]) => number | undefined = (xs) => xs.at(0); const headS: (_: string[]) => string | undefined = (xs) => xs.at(0); const headB: (_: boolean[]) => boolean | undefined = (xs) => xs.at(0); // 以下、同一な実装であっても各型ごとに区別しなければならない 😇
12. 多相型のモチベーション (2) 多相型がある 場合、次のように記述できる： const head: <T>(_: T[]) => T | undefined = (xs) => xs.at(0); head([ 1, 2, 3 ]); // 1 head([ 'a', 'b', 'c' ]); // 'a' head([ true, false, true ]); // true head([]); // undefined // 任意の型 `T` に対して、(型安全性を保って) 同一な実装を用いることができる 🙆‍♂️
13. 本当に？ 🤔 ある型 T ごとに分岐を許すと、変な実装も許されそう しかし直感的には、そのような実装はできないようにしたい 多相型で型付けされた実装 に対して、 暗黙のうちに ある型 T に依存しない ことを考えていそう → 多相型で型付けすることで、実装が限定される ことを導きたい
14. II. 数学的なモデル化
15. 前提 本資料では、以下の前提のもと数学的なモデルを考えていく： (素朴な) 型 を 集合 とみなす 純粋な関数のみを考慮する 不動点演算子 (いわゆる Y or Z コンビネータ) は考慮しない type F<X, Y> = (_: (_: X) => Y) => (_: X) => Y; type G<X, Y> = (_: G<X, Y> ) => (_: X) => Y; const Z = <X, Y>(f: F<X, Y>) => ( (g: G<X, Y>) => f((x) => g(g)(x)) ) ( (g: G<X, Y>) => f((x) => g(g)(x)) );
16. 導入：多相型の表現 多相型で型付けされた値は (チルダ) で区別する。このとき： 1. 通常の TypeScript における型表現 ∗ ~ ​ ​ ​ ​ h ~ h ~ ​ h ~ A : : : ⟨T⟩(_ : T[]) ⇒ T ∣ undefined ⟨T⟩. T[] ⇒ T ∣ undefined ⟨A/T⟩. A[] ⇒ A ∣ undefined (1) (2) (3)
17. 導入：多相型の表現 多相型で型付けされた値は (チルダ) で区別する。このとき： 1. 通常の TypeScript における型表現 2. 引数を省力した型表現 (本資料では一貫してこの型表現を採用) ∗ ~ ​ ​ ​ ​ h ~ h ~ ​ h ~ A : : : ⟨T⟩(_ : T[]) ⇒ T ∣ undefined ⟨T⟩. T[] ⇒ T ∣ undefined ⟨A/T⟩. A[] ⇒ A ∣ undefined (1) (2) (3)
18. 導入：多相型の表現 多相型で型付けされた値は (チルダ) で区別する。このとき： 2. 引数を省力した型表現 (本資料では一貫してこの型表現を採用) 3. ある型 A による具体化 ∗ ~ ​ ​ ​ ​ h ~ h ~ ​ h ~ A : : : ⟨T⟩(_ : T[]) ⇒ T ∣ undefined ⟨T⟩. T[] ⇒ T ∣ undefined ⟨A/T⟩. A[] ⇒ A ∣ undefined (1) (2) (3) ※ ※ 厳密には、具体化した時点で型パラメータ <T> は消去されます ( <A/T> は視覚的区別 )
19. 検討：多相型を 集合 でモデル化する？ 🤔 型を集合とみなすことは素朴だが、(e.g. boolean = ) ある型 T ごとに分岐する実装 を排除しきれない！ {true, false}
20. 検討：多相型を 集合 でモデル化する？ 🤔 型を集合とみなすことは素朴だが、(e.g. boolean = ) ある型 T ごとに分岐する実装 を排除しきれない！ e.g. を考える： 型パラメータ が取れること を、 宇宙 に属する 任意の集合 に対する操作 として解釈する 関数の型 を、配置集合 として解釈する ここで、ある型 による具体化 は、恒等関数以外も含みうる {true, false} ⟨T⟩. T ⇒ T ⟨T⟩ U T T ⇒ T TT A AA
21. 方針：多相型を 関係 でモデル化し、制約を強める そもそも "関係" とは？ デカルト積 の部分集合 のこと ソフトウェア・エンジニア的には、 2 Tuple の集まりのこと A × B
22. 方針：多相型を 関係 でモデル化し、制約を強める そもそも "関係" とは？ デカルト積 の部分集合 のこと ソフトウェア・エンジニア的には、 2 Tuple の集まりのこと 本資料では、関係を考えるとき で囲って表す は、 の部分集合であることを表す A × B [[ X ]] : (A, B) ​ R [[ ]] (A, B) ​ R A × B
23. III. さまざまな関係
24. 空関係 の部分集合として、空集合 を取ることができる これも として、関係に持ち上げて捉えて良い A × B ∅ [[ ∅ ]] [[ ∅ ]] : (A, B) ​ R
25. 恒等関係 型を関係に持ち上げる際の、自明な例のひとつ： [[ I ​ ]] : T (T, T) ​ = R {(t, t) ∣ t ∈ T} ≅ T
26. 恒等関係 型を関係に持ち上げる際の、自明な例のひとつ： e.g. の持ち上げ： [[ I ​ ]] : T (T, T) ​ = R {(t, t) ∣ t ∈ T} ≅ T boolean ​ ​ ​ [[ I ​ ]] boolean = = = ≅ {(t, t) ∣ t ∈ boolean} {(t, t) ∣ t ∈ {true, false}} {(true, true), (false, false)} boolean
27. 恒等関係 型を関係に持ち上げる際の、自明な例のひとつ： e.g. の持ち上げ： [[ I ​ ]] : T (T, T) ​ = R {(t, t) ∣ t ∈ T} ≅ T boolean ​ ​ ​ [[ I ​ ]] boolean = = = ≅ {(t, t) ∣ t ∈ boolean} {(t, t) ∣ t ∈ {true, false}} {(true, true), (false, false)} boolean
28. 恒等関係 型を関係に持ち上げる際の、自明な例のひとつ： e.g. の持ち上げ： [[ I ​ ]] : T (T, T) ​ = R {(t, t) ∣ t ∈ T} ≅ T boolean ​ ​ ​ [[ I ​ ]] boolean = = = ≅ {(t, t) ∣ t ∈ boolean} {(t, t) ∣ t ∈ {true, false}} {(true, true), (false, false)} boolean
29. 恒等関係 型を関係に持ち上げる際の、自明な例のひとつ： e.g. の持ち上げ： [[ I ​ ]] : T (T, T) ​ = R {(t, t) ∣ t ∈ T} ≅ T boolean ​ ​ ​ [[ I ​ ]] boolean = = = ≅ {(t, t) ∣ t ∈ boolean} {(t, t) ∣ t ∈ {true, false}} {(true, true), (false, false)} boolean
30. 関係としての関数 関数 は、関係 に持ち上げることができる： f : X ⇒ Y [[ f ]] [[ f ]] : (X, Y) ​ = R {(x, ​ ) ∣ ∈Y ​ f(x) x ∈ X}
31. 関係としての関数 関数 は、関係 に持ち上げることができる： e.g. not 関数 の持ち上げ： f : X ⇒ Y [[ f ]] [[ f ]] : (X, Y) ​ = R {(x, ​ ) ∣ ∈Y ​ f(x) x ∈ X} ¬ : boolean ⇒ boolean ​ ​ ​ [[ ¬ ]] = = = {(x, ¬(x)) ∣ x ∈ boolean} {(x, ¬(x)) ∣ x ∈ {true, false}} {(true, false), (false, true)}
32. 関係としての関数 関数 は、関係 に持ち上げることができる： e.g. not 関数 の持ち上げ： f : X ⇒ Y [[ f ]] [[ f ]] : (X, Y) ​ = R {(x, ​ ) ∣ ∈Y ​ f(x) x ∈ X} ¬ : boolean ⇒ boolean ​ ​ ​ [[ ¬ ]] = = = {(x, ¬(x)) ∣ x ∈ boolean} {(x, ¬(x)) ∣ x ∈ {true, false}} {(true, false), (false, true)}
33. 関係としての関数 関数 は、関係 に持ち上げることができる： e.g. not 関数 の持ち上げ： f : X ⇒ Y [[ f ]] [[ f ]] : (X, Y) ​ = R {(x, ​ ) ∣ ∈Y ​ f(x) x ∈ X} ¬ : boolean ⇒ boolean ​ ​ ​ [[ ¬ ]] = = = {(x, ¬(x)) ∣ x ∈ boolean} {(x, ¬(x)) ∣ x ∈ {true, false}} {(true, false), (false, true)}
34. メモ 📝：関係の表現力 関数 の関係への持ち上げ は、 1 つの入力に対して 1 つの出力を持つ表現 に限定される 一方、 関係 は の任意の部分集合なので、 1 つの入力に対して複数の出力を持つ表現 も許容できる f : X ⇒ Y [[ f ]] X × Y
35. メモ 📝：関係の表現力 関数 の関係への持ち上げ は、 1 つの入力に対して 1 つの出力を持つ表現 に限定される 一方、 関係 は の任意の部分集合なので、 1 つの入力に対して複数の出力を持つ表現 も許容できる e.g. 平方根の関係 について： f : X ⇒ Y [[ f ]] X × Y [[ S ]] = {(x, y) ∣ x = y } 2 (4, 2) ∈ [[ S ]] ∧ (4, −2) ∈ [[ S ]]
36. 関数関係 (1) 2 つの関係 と を用いて、 2 Tuple の各要素が関数 となるような関係を定義できる： [[ X ]] : (X, X ) ​ ′ R [[ Y ]] : (Y, Y ) ​ ′ R [[ X ]] ​ R [[ Y ]] : (X ⇒ Y, X ⇒ Y ) ​ ′ ′ R (f, f ) ​ ​ ​ ​ { ′ for all (x, x ) ′ (f(x), f (x )) ′ ′ ∈ ∈ [[ X ]], [[ Y ]] }
37. 関数関係 (2) 具体例として、 を考えてみる： 【 関数関係が満たすべき条件 】 [[ I ​ ]] ​ boolean R [[ I ​ ]] 0∣1 ​ ​ ​ ​ for all ( ​ ) x=x′ ※ x, x′ ( ​ ) f(x)=f (x ) ′ ′ ※ ​ f(x), f (x ) ′ ′ ∈ ∈ [[ I ​ ]], boolean [[ I ​ ]] 0∣1 ※ 恒等関係に含まれる 2 Tuple は、常に第 1 要素と第 2 要素が等しいため
38. 関数関係 (2) 具体例として、 を考えてみる： 【 関数関係が満たすべき条件 】 → 関数の外延性から、 を満たす 2 Tuple のみ考えれば良い [[ I ​ ]] ​ boolean R [[ I ​ ]] 0∣1 ​ ​ ​ ​ for all ( ​ ) x=x′ ※ x, x′ ( ​ ) f(x)=f (x ) ′ ′ ※ ​ f(x), f (x ) ′ ′ ∈ ∈ [[ I ​ ]], boolean [[ I ​ ]] 0∣1 f = f′ ※ 恒等関係に含まれる 2 Tuple は、常に第 1 要素と第 2 要素が等しいため
39. 関数関係 (3) その上で、 関数の型 の値 をすべて列挙する： boolean ⇒ 0∣1 const c0: (_: boolean) => 0|1 = (_) => 0; const c1: (_: boolean) => 0|1 = (_) => 1; const n: (_: boolean) => 0|1 = (x) => Number(x) as 0|1; const u: (_: boolean) => 0|1 = (x) => Number(!x) as 0|1;
40. 関数関係 (4) 最後に を満たす 2 Tuple を列挙すると、以下となる： f = f′ [[ I ​ ]] ​ boolean R [[ I ​ ]] = 0∣1 {(c ​ , c ​ ), (c ​ , c ​ ), (n, n), (u, u)} 0 0 1 1
41. 全称関係 (1) を、関係 を表現のどこかに持つ関係とする その上で、関係 について 全称量化 することを考える： F([[ X ]]) [[ X ]] [[ X ]] ⟨[[ X ]]⟩. F([[ X ]]) = ( ​ , ​ ) ​ ​ ​ ​ { f ~ f ~′ for all [[ X ]] ( ​ ​ , ​ ​ ) f ~ X f ~′ X′ : ∈ (X, X ) ​ , ′ R F([[ X ]]) }
42. 全称関係 (1) を、関係 を表現のどこかに持つ関係とする その上で、関係 について 全称量化 することを考える： ここで、 は で添字づけられた集まり， は で添字づけられた集まりを意味し、 と を型で考えると、 多相型で型付けされた値 とみなせる F([[ X ]]) [[ X ]] [[ X ]] ⟨[[ X ]]⟩. F([[ X ]]) = ( ​ , ​ ) ​ ​ ​ ​ { f ~ f ~′ for all [[ X ]] ( ​ ​ , ​ ​ ) f ~ X f ~′ X′ : ∈ (X, X ) ​ , ′ R F([[ X ]]) } ​ f ~ X ​ f ~′ X′ X X′
43. 全称関係 (2) 具体例として、 を考えてみる： 【 全称関係が満たすべき条件 】 ⟨[[ X ]]⟩. [[ X ]] ​ ​ ​ ​ for all [[ X ]] ( ​ ​ , ​ ​ ) f ~ X f ~′ X′ : ∈ (X, X ) ​ , ′ R [[ X ]]
44. 全称関係 (2) 具体例として、 を考えてみる： 【 全称関係が満たすべき条件 】 ここで、どのような と に対しても、 空関係 を考慮する必要がある → 述語を満たせない 😇 ⟨[[ X ]]⟩. [[ X ]] ​ ​ ​ ​ for all [[ X ]] ( ​ ​ , ​ ​ ) f ~ X f ~′ X′ : ∈ (X, X ) ​ , ′ R [[ X ]] X X′ [[ ∅ ]] : (X, X ) ​ ′ R
45. 全称関係 (2) 具体例として、 を考えてみる： 【 全称関係が満たすべき条件 】 ここで、どのような と に対しても、 空関係 を考慮する必要がある → 述語を満たせない 😇 → を満たすことは、とても大変 😵‍💫 ⟨[[ X ]]⟩. [[ X ]] ​ ​ ​ ​ for all [[ X ]] ( ​ ​ , ​ ​ ) f ~ X f ~′ X′ : ∈ (X, X ) ​ , ′ R [[ X ]] X X′ [[ ∅ ]] : (X, X ) ​ ′ R for all [[ ∗ ]]
46. ここまでのまとめ 以下それぞれを定義し、簡単に性質を確かめた： 空関係 恒等関係 関係としての関数 関数関係 全称関係 (本資料では取り扱わないが) 参考文献では 直積関係 や リスト関係 なども記載されているので、興味があれば参照まで 📝 [[ ∅ ]] [[ I ​ ]] T [[ f ]] [[ X ]] ​ R [[ Y ]] ⟨[[ X ]]⟩. F([[ X ]])
47. ※ まだ、実装が限定される性質は示していない 🤔
48. IV. "Parametricity" の主張
49. Parametricity 多相型を持つ型システムを考える ある値 の型 から、帰納的に導出できる 関係 は、 を満たす 【 簡単な具体例 】 に関して、 が成り立つ ※ t T [[ T ]] (t, t) ∈ [[ T ]] ​ : t ​ true ​ T ​ boolean (true, true) ∈ [[ I ​ ]] boolean ※ 参考文献における記述は "閉じた項" ですが、型環境を適切に考慮すれば解消可能です
50. 実際に試してみる (1) (の型) から、 という関係を 帰納的に導出した上で、満たすべき条件を考える： 【 関係が満たすべき条件 】 ​ : f ~ ⟨T⟩. T ⇒ T ⟨[[ T ]]⟩. [[ T ]] ​ R [[ T ]] ​ ​ ​ ​ for all for all [[ T ]] (t, t ) ′ ( ​ ​ (t), ​ ​ (t )) f ~ T f ~ T′ ′ : ∈ ∈ (T, T ) ​ , ′ R [[ T ]], [[ T ]]
51. 実際に試してみる (1) (の型) から、 という関係を 帰納的に導出した上で、満たすべき条件を考える： 【 関係が満たすべき条件 】 ​ : f ~ ⟨T⟩. T ⇒ T ⟨[[ T ]]⟩. [[ T ]] ​ R [[ T ]] ​ ​ ​ ​ for all for all [[ T ]] (t, t ) ′ ( ​ ​ (t), ​ ​ (t )) f ~ T f ~ T′ ′ : ∈ ∈ (T, T ) ​ , ′ R [[ T ]], [[ T ]]
52. 実際に試してみる (1) (の型) から、 という関係を 帰納的に導出した上で、満たすべき条件を考える： 【 関係が満たすべき条件 】 ​ : f ~ ⟨T⟩. T ⇒ T ⟨[[ T ]]⟩. [[ T ]] ​ R [[ T ]] ​ ​ ​ ​ for all for all [[ T ]] (t, t ) ′ ( ​ ​ (t), ​ ​ (t )) f ~ T f ~ T′ ′ : ∈ ∈ (T, T ) ​ , ′ R [[ T ]], [[ T ]]
53. 実際に試してみる (2) の部分集合として、関数の持ち上げ を 任意にとってみる： (T, T ) ​ ′ R [[ g : T ⇒ T ]] ′ ​ ​ ​ ​ for all for all [[ g ]] (t, t ) ′ ( ​ ​ (t), ​ ​ (t )) f ~ T f ~ T′ ′ : ∈ ∈ (T, T ) ​ , ′ R [[ g ]], [[ g ]]
54. 実際に試してみる (3) 関数の持ち上げ は、 を満たす 2 Tuple のみ持つので： [[ g ]] (∗, g(∗)) ​ ​ ​ ​ for all for all [[ g ]] (t, ​ ) g(t) ​ t′ ( ​ ​ (t), ​ ) f ~ T g( ​ ​ (t)) f ~ T ​ ​ ​ (t ) f ~ T′ ′ : ∈ ∈ (T, T ) ​ , ′ R [[ g ]], [[ g ]]
55. 実際に試してみる (4) ここまでの状況を整理すると： ​ ​ ​ t′ ​ ​ (t ) f ~ T′ ′ = = g(t) g( ​ ​ (t)) f ~ T
56. 実際に試してみる (4) ここまでの状況を整理すると： 代入して整理すると、以下の等式が得られる： ​ ​ ​ t′ ​ ​ (t ) f ~ T′ ′ = = g(t) g( ​ ​ (t)) f ~ T ​ ​ (g(t)) = f ~ T′ g( ​ ​ (t)) f ~ T
57. 実際に試してみる (4) ここまでの状況を整理すると： 代入して整理すると、以下の等式が得られる： → この等式によって、 の実装が限定される！ ​ ​ ​ t′ ​ ​ (t ) f ~ T′ ′ = = g(t) g( ​ ​ (t)) f ~ T ​ ​ (g(t)) = f ~ T′ g( ​ ​ (t)) f ~ T ​ f ~
58. Fin. 🥳
59. α. 自然性条件
60. 関数関係，ふたたび (1) 2 つの関係 と を用いて、 2 Tuple の各要素が関数となるような関係を定義できる： [[ X ]] : (X, X ) ​ ′ R [[ Y ]] : (Y, Y ) ​ ′ R [[ X ]] ​ R [[ Y ]] : (X ⇒ Y, X ⇒ Y ) ​ ′ ′ R (f, f ) ​ ​ ​ ​ { ′ for all (x, x ) ′ (f(x), f (x )) ′ ′ ∈ ∈ [[ X ]], [[ Y ]] }
61. 関数関係，ふたたび (2) 2 つの関係 と を取り巻く状況： [[ X ]] : (X, X ) ​ ′ R [[ Y ]] : (Y, Y ) ​ ′ R
62. 関数関係，ふたたび (3) から関数の持ち上げ を、 から関数の持ち上げ を選ぶ： (X, X ) ​ ′ R [[ g ]] (Y, Y ) ​ ′ R [[ h ]]
63. 関数関係，ふたたび (3) から関数の持ち上げ を、 から関数の持ち上げ を選ぶ： → ＼完全に可換図式／ (X, X ) ​ ′ R [[ g ]] (Y, Y ) ​ ′ R [[ h ]]
64. 全称関係で "対象" を任意に動かす 可換図式が任意に成立することを表し、 特に の場合は 自然変換 といえる ​ = f ~ ​ f ~′
65. まとめ 関数関係 により、 可換図式 が得られる 全称関係 により、 自然変換 が得られる これより、 多相関数は自然変換 であることもわかる 【 参考文献 】 『Theorems for free !』by Philip Wadler 『型システム入門 - プログラミング言語と型の理論 -』by オーム社