自己紹介情報科学の研究をしています専門はプログラミング言語とか型理論とか研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらいの著者です

Size: px

Start display at page:

Download "自己紹介情報科学の研究をしています専門はプログラミング言語とか型理論とか研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらいの著者です"

えのいくのや
5 years ago
Views:

1 ML 平成廿一年東都大駱駝会京都大学五十嵐淳

2 自己紹介情報科学の研究をしています専門はプログラミング言語とか型理論とか研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらいの著者です

3 いきなり鶴亀算 OCaml プログラマとラクダが合わせて 7 匹いる足の数が合わせて 20 本である時 OCaml プログラマとラクダはそれぞれ何匹いるか小学生の解法全員ラクダだとすると足の数は 4 x 7 = 28 本実際には 20 本あるから 8 本分ラクダが多いラクダ一匹を OCaml プログラマに置き換えると足は 2 本減るから 4 人置き換えれば丁度よい OCaml プログラマ 4 匹ラクダ 3 匹

4 いきなり鶴亀算 OCaml プログラマとラクダが合わせて 7 匹いる足の数が合わせて 20 本である時 OCaml プログラマとラクダはそれぞれ何匹いるか中学生の解法 OCaml プログラマの数を x ラクダの数を y とすると x + y = 7 2x + 4y = 20 これを解いて x = 4, y = 3

5 中学生の解法のエラいところ未知数の導入未知数を使った式で状況をとにかく表現簡単に解ける問題 ( 連立一次方程式 ) に帰着

6 今日のおはなし ML 型推論の仕組み長所短所を知る MLの型検査と型推論 ML 型推論の仕組み多相型などにはほとんど踏みこみません ML 型推論礼賛 ML 型推論に毒づく解毒剤まとめ

7 ML の型検査型推論

8 ML の型検査プログラムのつじつまが合っているかの検査 if の条件部には真偽値がくるか関数の引数は適当かプログラム実行前に行われる ( 静的検査 ) 型検査を通過データの種類にまつわるエラーが実行時に発生しないことが保証される 0 での除算などのエラーはその限りではない型安全性

9 型プログラム ( 断片 ) の分類のためのラベル int 型実行結果が整数である ( あろう ) ような式 bool 型実行結果が真偽値であるような式 int bool 型実行結果が整数を引数として真偽値を返すような関数値であるような式分類にあてはまる式がつじつまの合った式 1+1 は int 型の式 fun x x > 3 は int bool 型の式 if 3 then 4 else 5 は型が与えられない式

10 型付け規則何がつじつまの合った式なのかを型を使って規定整数定数式には int 型を与える式 e1 と e2 ともに int 型が与えられるなら式 e1+e2 には int 型を与える式 e1 と e2 にそれぞれ S T 型 S 型が与えられるなら適用式 e1 e2 には T 型を与える x は S 型であるという仮定の下で式 e に T 型が与えられるなら fun x e には S T 型を与える

11 型推論変数に対する型宣言のないプログラムからを知る変数の型プログラムの型 fun x x > 1 の型は? x は int 型で全体は int bool 型です!

12 ML 型推論の仕組み Hindley の写真 Milner の写真 J. Roger Hindley (b. 1938) Robin Milner (b. 1934) Luís Damas (b. 19??) John Alan Robinson (b. 1930)

13 問題設定の確認入力 : 式 ( とこれまでに定義された関数などの型 ) 出力 : 各変数の型と式の型またはエラー

14 基本的なアイデア : 中学生の鶴亀算わからないことは変数で表す型変数 (α, β,...) の導入状況をとにかく式で表す状況 : 部分式の型同士の関係型付け規則の役割各部分式の型の間に成立すべき関係の規定具体的な問題全てに共通する背景知識簡単な問題に帰着 ML の場合 : 一階の単一化 (unification) 問題

15 例題 (1): fun f f(3) + 2 f の型は α, 各部分式 3, f(3), 2, f(3)+2, fun f f(3)+2 の型を β1,...,β5 とおく型付け規則から方程式を立てる整数定数式の型付け規則 β1 = int 関数呼び出し式の型付け規則 α = β1 β2 整数定数式の型付け規則 β3 = int 足し算式の型付け規則 β2 = int, β3 = int, β4 = int funの型付け規則 β5 = α β4 解く! α = int int, β1 =... = β4 = int β5 = (int int) int

16 例題 (2): fun f f(3) + f f の型は α, 各部分式 3, f(3), f(3)+f, fun f f(3)+f の型を β1,...,β4 とおく型付け規則から方程式を立てる整数定数式の型付け規則 β1 = int 関数呼び出し式の型付け規則 α = β1 β2 整数定数式の型付け規則 α = int 足し算式の型付け規則 β2 = int, α = int, β3 = int funの型付け規則 β4 = α β3 解く! 解けない!

17 鶴亀算でいうと Ocaml プログラマとラクダが合わせて 7 匹いる足の数が合計で 20 本であったレントゲン写真を撮ってみると胃が 14 個見える Ocaml プログラマとラクダはそれぞれ何匹いるかちなみにラクダには胃が 3 つある ( 生物学的には 4 つでひとつは退化しているらしい ) OCaml プログラマの数を x ラクダの数を y とすると x + y = 7 2x + 4y = 20 x + 3y = 14 この方程式には解がない

18 例題 (2): fun f f(3) + f... 整数定数式の型付け規則 β1 = int 関数呼び出し式の型付け規則 α = β1 β2 整数定数式の型付け規則 α = int 足し算式の型付け規則 β2 = int, α = int, β3 = int funの型付け規則 β4 = α β3 解く! 解けない! ってよく見たら f を関数として使ったり整数として使ったりしてるじゃん型検査を通してはいけないプログラム

19 例題 (3): fun f f(3) f の型は α, 各部分式 3, f(3), fun f f(3) の型を β1,...,β3 とおく型付け規則から方程式を立てる整数定数式の型付け規則 β1 = int 関数呼び出し式の型付け規則 α = β1 β2 funの型付け規則 β3 = α β2 解く! 別解が無数にある! 解 1: α = int int, β3=(int int) int 解 2: α = int string, β3=(int string) string 解 3: α = int int list, β3=(int int list) int list...

20 ふたたび鶴亀算でいうと Ocaml プログラマとラクダが合わせて 7 匹いる目の数は合計で 14 個であった OCaml プログラマとラクダはそれぞれ何匹いるか OCaml プログラマの数を x ラクダの数を y とすると x + y = 7 2x + 2y = 14 これを解いて x = 7 y ( 解のパラメータ表示 ) この関係を満たす自然数 x, y ならなんでもよい

21 例題 (3): fun f f(3)... 整数定数式の型付け規則 β1 = int 関数呼び出し式の型付け規則 α = β1 β2 funの型付け規則 β3 = α β2 解く! fun 式の型 β3 = (int β2) β2 上の式を満たす β3 β2 ならなんでもよい多相性!

22 方程式の一般形と解法型に関する等式の集合等式の例 : β int = (bool * α) δ 両辺 : int, bool などの基本型と型変数をや * で繋いでいった型一般的には一階 (first-order) の単一化問題と呼ばれる ( 解ける場合には ) 解が必ず求まる方法 ( 詳細は省略 ) がある![Robinson65] しかも最も一般的な解が求まる! 全ての解のパラメータ表示

23 ここまでのまとめ ML の型推論は単一化問題に帰着できる式が型付けできるかどうか = 式から導かれる単一化問題の解の有無解が複数ある場合 : 多相的なプログラム

24 ML 型推論礼賛

25 プログラムにいちいち型書かなくてもよくてしかも安全なんてちょー便利じゃんだよね

26 ML 型推論の性質型推論の完全性 ( 主要型の推論 ) うまく変数の型を与えれば型検査に通るようなプログラムは必ず型推論に成功する型宣言はいつでも省略可最も一般的な型 ( 主要型 ) を推論型推論の健全性型推論に成功したプログラムは必ず型エラーなく実行できる

27 主要型式に与えうる型のバリエーション全てを網羅するような ( 多相 ) 型 fun x (x, x) に与えうる型 int int*int string string*string int list int list * int list 主要型は : α α * α 主要型の推論は単一化を解くアルゴリズムの性質の系

28 ML 型推論に毒づくここにはイギリスのロックバンド Black Sabbath のアルバム Heaven and Hell のジャケットがあると思ってください

29 つーか ML ってプログラム見ても型書いてなくて何すんだかわかんねーんだけどだよねここにはイギリスのロックバンド Black Sabbath のアルバム Heaven and Hell のジャケットがあると思ってください

30 つーか ML ってプログラム見ても型書いてなくて何すんだかわかんねーんだけどだよねトップレベルの関数くらいは型が宣言されていた方が親切かもしれません ( 特に一週間後のあなたに ) ここにはイギリスのロックバンド Black Sabbath のアルバム Heaven and Hell のジャケットがあると思ってください

31 つーか ML ってさあエラーメッセージが腐ってない? こないだもさぁここにはイギリスのロックバンド Black Sabbath のアルバム Heaven and Hell のジャケットがあると思ってください

32 let f x ls = (List.fold_left x (+) ls, x + 1);; Characters xx-yy:... x + 1);; ^ This expression has type (int -> int -> int) -> 'a -> int -> int -> int but is here used with type int ここの巨大な型はいったい!? (20 分後デバグを終えて ) 間違えてんのここじゃねーし!( 怒 )

33 解毒剤

34 親切なエラーメッセージを出す研究方程式を解く順序を工夫するエラーは ( 型 ) 変数消去ができなくなった時に発生する型推論がいかに失敗したかをうまく説明適当な経験則でエラー箇所を推測 (& 修正の提案 ) 経験則の例 : 場合分けの各枝で型が合わない場合は多数決で (!) どの枝が悪いか決めるエラーに関連するプログラムを抽出して見せる ( プログラムスライシング )

35 方程式を解く順序を工夫する fold_left : (α β α) α β list α x : α1, (+) : int int int fold_left x (+) ls, x + 1 fold_left x fold_left x (+) x +... α1 = α β α α = int int int α1 = int α を消去 α1 を消去即エラー α1 = (int int int) β (int int int) α1 = int

36 万能な順序付けは難しい多くの ML 処理系では式の位置で解く順番が決まる例えばペアの要素順を変えるだけでぐっとわかりやすくなる let f x ls = (x + 1, List.fold_left x (+) ls);; Characters xx-yy:... List.fold_left x (+) ls);; ^ This expression has type int but is here used with type 'a -> 'b -> 'a 本当はいつでも正しいあたりから解き始めたい

37 難しいというか根本的な解決は無理な話では? 問題設定のどこ ( 個体数足の数胃の数 ) が間違っていたのか答える方法がないのと同じ? Ocaml プログラマとラクダが合わせて 7 匹いる足の数が合計で 20 本であったレントゲン写真を撮ってみると胃が 14 個見える Ocaml プログラマとラクダはそれぞれ何匹いるか結局大体うまくいく経験則に頼るしかない

38 まとめ方程式はエラい ML 型推論もかなりエラい実行時の安全性保証主要な型の推論何が間違いなのかを知るのは難しい経験則に基いた対策はいろいろ考えられている実用上充分な決定版はまだないラクダの胃の数は 3 つ第三第四の胃がくっついている

39 おまけ : 型推論実装演習のはなし学生に ML 型推論を OCaml で実装させてます対象 : 学部 3 回生 (Scheme の経験はあり ) 期間 : 週 6 コマの演習 x 6 週間のうち最後の 2 週間多相性はオプション正しく実装するのは難しいです方程式の構成と単一化の解消を交互にやるのがミスりやすい結果 : はじくべきプログラムをはじけない対策 : テスト用の正例反例両方を提供

40 学生の実装の傑作 No.1 # let s x y z = x z (y z);; (* 正しい結果 *) val s : ('a 'b 'c) ('a 'b) 'a 'c = <fun> (* 学生 X の提出したプログラムの出力 *) val s : 'a 'b 'c 'd = <fun> Obj.magic か!?

構造化プログラミングとデータ抽象

構造化プログラミングとデータ抽象計算の理論後半第 3 回 λ 計算と型システム本日の内容 λ 計算の表現力 ( 前回の復習 ) データの表現不動点演算子と再帰 λ 計算の重要な性質チャーチロッサー性簡約戦略型付き λ 計算ブール値組ブール値と組の表現 true, false を受け取り対応する要素を返す関数として表現 T = λt.λf.t F = λt.λf.f if e 1 then e 2 else

自己紹介 情報科学の研究をしています 専門はプログラミング言語とか型理論とか 研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらい の著者です

自己紹介情報科学の研究をしています専門はプログラミング言語とか型理論とか研究のひとつは Java の改良ですが Java でプログラムは書きません ( けません ) ML 歴 16 年 OCaml 歴は 11 年くらいの著者です