型安全性入門

型安全性入門 2017.4.6 LT Thursday

自己紹介 ● ● 名前：阿部晃典（あべあきのり） 2016 年新卒入社 ○ ○ ● 広告配信の設定自動化（ Scala） DSP の CTR 予測（C++） 興味のある分野 ○ ○ 機械学習 プログラミング言語理論（型理論、メタプログラミング）

LT のきっかけ ● 最近、「型安全」って単語をよく聞きます ○ ● それ、ほんとに型安全なの？ ○ ○ ● Scala のライブラリとか type safe の謳い文句が多い 安全って何？ ちゃんと証明したの？自明なの？ 今日は静的型安全性の話をします ○ ○ ○ 「型安全性」をざっくり理解してもらうことが目的 静的型付き言語を前提に話します 厳密な話はしないので、興味のある人は後で聞いて下さい

お品書き 今日話すこと ● ● ● ● 型安全性とは何か 型安全性で保証されるもの 健全性と完全性 テストとの違い 話さないこと ● ● 厳密な型安全性の定義と証明 高度な型システム

型安全性とは？

型安全とは、どういうこと？ (Milner 1978) Well-typed programs can’t go wrong. 型付けできるプログラム 間違った状態に陥らない = 型検査を通過したプログラム = ある種のバグが存在しない

型安全性 「型検査（コンパイル）を通過したなら、 ある種のバグが存在しない」 という性質 ● コンパイル時に「ある種のバグが存在しない」ことを数学的に証明 ○ ● ● 型安全性を持つように、型システム・型検査器を設計・証明してある 検査済みのバグは実行時には絶対に起こらない プログラムの信頼性を数学的に保証

強い型付け、弱い型付け ● 強い型付け：型安全性が型検査で保証される ○ ○ ○ ● e.g., Java, Scala, OCaml, Haskell, etc. 「強い」とは「安全性の保証がある」ということ 型システムが高度であるかどうかとは別の話 弱い型付け：型安全性が保証されない ○ ○ e.g., C, C++ , etc. 型検査に通過しても、特に何も保証しない

ある種のバグって何？

安全性（バグの定義）は言語による ● だいたい言語 (Java, Scala, Go, OCaml, Haskell, etc.) ○ ● より高度な言語や型システム (ATS, Coq, etc.) ○ ○ ○ ○ ● メモリ安全とか null 安全が多い（と思う） 配列の境界検査 Termination check（反復・再帰が常に停止することを検査） Dead-lock freedom（絶対にデッドロックしないことを検査） など ライブラリが +α の安全性を提供することも ○ ○ ○ DB クエリ言語の実行時型エラーを防ぐ (Slick, Rogue) 行列演算のサイズ検査 など

型検査の恩恵が薄いことも ● ● Java はメモリのアクセス違反は起こさない でも、コンパイル時には検出せず、実行時に例外を投げる List x = null x.add(42) // NullPointerException ● Java は「実行時に補足されたエラーだから OK」というスタンス（たぶん） ○ ● C, C++ だと（言語レベルで補足されない）セグメンテーション違反を起こす いわゆる null 安全な言語は、この手のエラーを型検査で検出

要するに ● ● 言語・ライブラリで安全性（検査できるバグの種類）が違う どんな安全性を保証してくれるのか把握しておくことが大事

健全性と完全性

健全性と完全性 型安全性 (type safety), 健全性 (soundness) ● ● 「型が付くならば、ある種のバグは絶対にない」（偽陰性の排除） 「型エラーならば、バグがあるかもしれない」（偽陽性の許容） ○ ○ バグがないのに、間違って型エラー出しちゃうかも バグがあるのに型検査を通過させるリスクが大きい 完全性 (completeness) ● ● 「型エラーがあれば、バグが絶対にある」（偽陽性の排除） 健全かつ完全な型検査は難しい ○ チューリング完全な言語では決定不能問題

テストとは何が違うの？

テストと型検査 テスト ● ● ● 有限個の入力（テストケース）でプログラムが仕様を満たすか実行して確認 （あるテストケースで）バグが存在することを保証 検査対象のバグの種類を増やすことは比較的簡単 型検査 ● ● ● 任意の入力について、プログラムが仕様を満たか実行せずに確認 （ある種の）バグが存在しないことを証明 検査対象のバグの種類を増やすのは難しい

テストと型検査どっちがいいの？ 私見ですが、 ● ● それぞれの特徴を踏まえて、どっちもやるのが現実的に良い 可能なところは型検査、難しいところはテストが一番楽 ○ 型検査で「可能なところ」を見極めるには、「型安全性」を知る必要がある 型検査の範囲を増やすには？ ● ● 型レベルトリック（GADT、幽霊型などで頑張る） 依存型のある言語を使う（Coq、ATS など）

まとめ

まとめ ● 型安全性：型検査で特定のバグが存在しないことを保証する性質 ○ ○ ● 強い型検査とテストは特徴が違う ○ ● 言語・ライブラリで安全性（検査できるバグの種類）が違う どんな安全性を保証してくれるのか把握しておくことが大事 組み合わせるといい感じ 上手に使って、バグを殺しましょう！