幽霊型の紹介（サイバーエージェントA.J.A.社内勉強会 2016.6.23）

A.J.A.社内勉強会 6/23 幽 霊 型 の 紹 介

自己紹介 ● ● ● 名前：阿部晃典 言語：OCaml, Perl, JavaScript, C/C++, Go, Java, PHP, LaTeX, Octave, etc. 専門：プログラミング言語理論 ○ ○ ● 大学〜大学院１年くらいまで、幽霊型を使った線形代数ライブラリを作成 ■ Sized Linear Algebra Package (SLAP): http://akabe.github.io/slap/ C++ テンプレート（メタプログラミング）を出力するコンパイラを書いた ■ EvilML (a compiler from ML to C++ template): http://akabe.github.io/evilml/ 趣味：機械学習

• http://akabe.github.io/slap/
• http://akabe.github.io/evilml/

幽霊型 (phantom type) とは... ● プログラムのバグをコンパイル時に発見する手法 ○ ○ ○ ● テスト工数削減 プログラムの信頼性向上 使ってて楽しい プログラムに型が付く ⇒ ある種のバグは存在しないことを証明 ○ 「ある種のバグ」の範囲は幽霊型トリックによって色々 ■ 例１：行列演算の次元の整合性の検査 [Eaton ‘06, Abe & Sumii ‘15] ■ 例２：配列アクセスの境界検査 [Kiselyov & Shan ‘07] ■ 例３：型安全な DSL (Domain Specific Language) ● C 関数のバインディング in Standard ML [Blume ‘01] ● JavaScript のバインディング in OCaml, Haskell (js_of_ocaml, ghcjs) ● Rogue (MongoDB in Scala)

簡 単 な 例

例：多重エンコードの検出 val x = "Hello, World!” val y = encode(x) // これは OK val z = encode(y) // これは型エラーにしたい ● ● enc 関数の仕様 ○ 入力：普通の（エンコードされていない）文字列 ○ 出力：エンコード済みの文字列 enc 関数の型 ○ 引数型：Str[Normal] (= String) ○ 戻り値型：Str[Encoded] (= String) ポイント① プログラムの 詳細な仕様を型で表現

素朴な実装 class Str [T] (val str: String) // T は幽霊型変数：内部では使われない型変数 trait Normal // 幽霊型（値を持たない型） trait Encoded // これも幽霊型 ポイント② 幽霊型変数に 仕様を表す型を入れる def encode(x: Str[Normal]) = new Str[Encoded](...) // encode: (x: Str[Normal]): Str[Encoded] val x = Str[Normal](“Hello, World”) val y = encode(x) // これは OK (y: Str[Encoded]) val z = encode(y) // 型エラー

素朴な実装の問題点 class Str [T] (val str: String) trait Normal trait Encoded エンコード済みの文字列 なのに Str[Normal] の def encode(x: Str[Normal]) = new Str[Encoded](...) 型付いている val val val val x y z w = = = = Str[Normal](“Hello, World”) encode(x) // y: Str[Encoded] Str[Normal](y.str) // z: Str[Normal] encode(z) // 二重エンコードできてしまう！

コンストラクタの隠蔽 ポイント③ コンストラクタと フィールドを隠蔽する object SafeStr { class Str [T] private[SafeStr] (private[SafeStr] val str: String) trait Normal trait Encoded def create(x: String) = new Str[Normal](x) def encode(x: Str[Normal]) = new Str[Encoded](...) } val val val val x y z w = = = = create(“Hello, World”) encode(x) // y: Str[Encoded] Str[Normal](y.str) // Error! encode(y) // type mismatch

ポイントのおさらい ポイント③ コンストラクタと フィールドを隠蔽する object SafeStr { class Str [T] private[SafeStr] ポイント② (private[SafeStr] val str: String) 幽霊型変数に trait Normal 仕様を表す型を入れる trait Encoded def create(x: String) = new Str[Normal](x) def encode(x: Str[Normal]) = new Str[Encoded](...) // encode (x: Str[Normal]): Str[Encoded] } ポイント① プログラムの 詳細な仕様を型で表現

も う 少 し 高 度 な 例

型レベル自然数 (Peano 形式) class Nat[N] (val n: Int) // Nat[N]=Int trait Z // zero trait S[N] // successor (n+1) val zero = new Nat[Z](0) // zero: Nat[N] def succ[N](n: Nat[N]) = new Nat[S[N]](n.n+1) // succ: (n: Nat[N]): Nat[S[N]] def pred[N](n: Nat[S[N]]) = new Nat[N](n.n-1) // pred: (n: Nat[S[N]]): Nat[N] val x = zero // x: Nat[Z] val y = succ(x) // y: Nat[S[Z]] val z = succ(y) // z: Nat[S[S[Z]]]

型レベル自然数による安全性 class Nat[N] (val n: Int) // Nat[N]=Int trait Z // zero trait S[N] // successor (n+1) val zero = new Nat[Z](0) // zero: Nat[N] def succ[N](n: Nat[N]) = new Nat[S[N]](n.n+1) // succ: (n: Nat[N]): Nat[S[N]] def pred[N](n: Nat[S[N]]) = new Nat[N](n.n-1) // pred: (n: Nat[S[N]]): Nat[N] val x = pred(succ(zero)) // x: Nat[Z] val y = pred(zero) // 型エラー（非負数であることを保証） zero == succ(zero) // 型エラー（値の等しさの保証）

型レベル自然数の用例：型安全 head, tail, zip class SList[N, E] (val list: List[E]) // SList[N,E]=List[E] trait Z // zero trait S[N] // successor (n+1) def empty[E]: SList[Z, E] = ... def cons[N, E] (a:E, x: SList[N, E]): SList[S[N], E] = ... def head[N, E] (x: SList[S[N], E]): E = ... def tail[N, E] (x: SList[S[N], E]): SList[N, E] = ... val x = cons(“baz”, empty[String]) // x: SList[S[Z], String] val y = tail(x) // y: SList[Z, String] val z = tail(y) // 型エラー（空リストは tail, head 不可）

型レベル自然数の用例：型安全 head, tail, zip class SList[N, E] (val list: List[E]) // SList[N,E]=List[E] trait Z // zero trait S[N] // successor (n+1) def empty[E]: SList[Z, E] = ... def cons[N, E] (a:E, x: SList[N, E]): SList[S[N], E] = ... def zip[N,E] (x: SList[N,E], y: SList[N,E]): SList[N,E] = val x = cons(“baz”, empty[String]) // x: SList[S[Z],String] val y = zip(x, x) // y: SList[S[Z], (String, String)] val z = zip(x, empty[String]) // 型エラー（長さの等しさを保証）

まとめ ● プログラムのバグをコンパイル時に発見する手法 ○ ○ ○ ● ポイント１：プログラムの詳細な仕様を型で表現 ポイント２：幽霊型変数に仕様を表す型を入れる ポイント３：コンストラクタを隠蔽して、幽霊型変数に入る型を制限 プログラムに型が付く ⇒ ある種のバグは存在しないことを証明 ○ 「ある種のバグ」の範囲は幽霊型トリックによって色々 ■ SafeStr の例：多重エンコード ■ ■ ■ ■ SafeList の例：空リストへの head, tail、異なる長さのリストの zip (http://bit. ly/ScalaSafeList) 例１：行列演算の次元の整合性の検査 [Eaton ‘06, Abe & Sumii ‘15] 例２：配列アクセスの境界検査 [Kiselyov & Shan ‘07] 例３：型安全な DSL (Domain Specific Language) [Blume’01, etc.]

• http://bit.ly/ScalaSafeList