Amosapientiam

https://yuchiki.github.io/

F*(F Star)の複雑な型システムの何が嬉しいのか?

マイクロソフトが開発中のF* という依存型プログラミング言語を少し触ってみました。 この言語には強力で複雑な型システムが組み込まれています。 現状、依存型言語は世間にはあまり広まっていませんので

  • F*とは?
  • 複雑な型ってなんだろう?
  • 複雑な型システムを組み込んで何が嬉しいんだろう?
  • 何が嬉しくないんだろう?

と疑問をお持ちになる方も多いだろうと思います。 この記事ではF*で使われている複雑な型の一部と、複雑な型を持つことの利点・欠点の一部を述べ、それを簡単なコード例を通じて体感してみます。

疑問に対する答え

F*とは?

マイクロソフトと Inria が開発中のプログラミング言語です。 依存型や monadic effect などが組み込まれており、複雑な仕様が型で表現できます。構文は OCaml や F#などのML系関数型言語に似ています。 詳しくは下記のリンクたちを参照。

F*の複雑な型システムって?

上の説明から、 F*の型システムには依存型と effectが組み込まれていることがわかります。

依存型

型の中に値が現れる型です。

依存型 - Wikipedia

例えば、 「整数型で100より大きい値」の型や「文字列で、長さが10より小さい値」の型などです。

effect

F* では、関数の型の中には

  • 純粋で必ず停止する関数である
  • 停止するとは限らない
  • 副作用があるかもしれない
  • ...

などの情報が埋め込まれています。これらを表現する仕組みがeffectと呼ばれています。

型が複雑であることの利点

型は仕様でもあること、型検査は仕様検証でもあることは以前の記事で書きました。 この観点から、複雑で表現力の高い型を持つことには以下の利点があると言えます。

  • 型によって複雑な仕様が表現でき、実装が複雑な仕様を満たすことを型検査によって保証できる。

型が複雑であることの欠点

型が複雑になるにつれ、コンパイラが自力で型検査ををするのは難しくなります。コンパイラの助けになるように人間が自力で型付けのヒントを書かなければならない場面も増えます。極端な場合は複雑な証明をひたすら書くハメになります。 *1

F*コードの例

以上で挙げた特徴がどういうものなのか、具体的にシンプルな関数を例にとって確認してみます。

今回の関数

以下の関数を例にとります。

// 仕様:関数gcdは2つの正整数を受け取り、その(最大)公約数を返す
let rec gcd a b =
    match compare_int a b with
    | Gt -> gcd (a - b) b
    | Lt -> gcd b a
    | Eq -> a

この関数は少なくともコンパイルが通ります。

"match with" は場合分けの構文です。a と b の2つの引数を受け取り、a と b を大小比較し、

  • a の方が大きかった場合(greater than)は gcd (a-b) b を返り値とし、
  • a の方が小さかった場合(less than)は gcd b a を返り値とし、
  • a と b が等しい場合(equal)は a を返します。

確認したい性質・仕様

私は関数gcdを「正整数 2 つの最大公約数を返す関数」のつもりで書いたのですが、本当に正しく書けているでしょうか?それをコンパイラ(の中の型検査器)に保証してもらうためには、gcd に「正整数を2つ受け取り、その最大公約数を返す関数」の型が付くことを確認してもらえばよいです。

この記事では簡単のため、もう少し弱い仕様である「関数 gcd は正整数を2つ受け取り、その公約数を返す」ことの確認を最終目標とし、そのために gcd に「正整数を2つ受け取り、その公約数を返す関数」の型を付けるところまでを目指します。

いきなり複雑な型を読み解くのは難しいので、最初は弱い簡単な型を付けて、徐々に強くしていく方針で説明します。

返り値が整数であることを保証する型

少なくとも gcd には 整数を2つ受け取って整数を返す関数であってほしいです。 これを表す型は F*ではint -> int -> ML intです。

"ML"というのはこの関数が純粋で total だとは限らないという断り書きです。 返り値の型の前に ML と書くことで、「この関数は参照透過でないかもしれないし、クラッシュするかもしれないし、ひょっとしたら停止しないかもしれないが、停止した時には必ず int 型の値を返す」という意味の型になります。 よくあるプログラミング言語の関数の型の意味と同じです。

gcdが int ->int -> ML intの型を持つかどうかF*コンパイラにチェックしてもらいます。

val gcd : int -> int -> ML int
let rec gcd a b =
    match compare_int a b with
    | Gt -> gcd (a-b) b
    | Lt -> gcd b a
    | Eq -> a

上のコードは無事型検査が通ります。 gcdの実装が「整数を2つ受け取って(停止すれば)整数を返す関数」であることは保証されました。

停止性・参照透過性などまで保証する型

"ML"の代わりに"Tot"と書く場合、F*では「関数は副作用を持たず、必ず停止し、int 型の値を返す関数」の型になります。 gcd には必ず停止して答えを返す関数であってほしいので、型シグネチャの部分を以下のように書き換えます。

val gcd : int -> int -> Tot int

この例では残念ながら型検査を通りません。 よくよく考えると、例えばgcd -1 0などは停止せずに無限ループし続けるので当然です。 そもそもそんな入力は受け付けたくないので、関数の定義域を絞ります。

val gcd : a:int{ a > 0 } -> b:int{ b > 0 } -> Tot int

a:int{ a > 0 } は 「int 型のうち、 0 より大きい値」の型です。 この種の型は型の中に値の情報が現れており、値に依存しているので、依存型と呼ばれます。

今度は型の意味するところは正しいはず...なのですが、これでも型検査を通りません! 値域を正整数に限ればたしかに停止するのですが、残念ながら型検査器はその証明を思いつけていないのです。

そこで、人間がヒントを与える必要があります。

停止性の証明のためには

  • 再帰的な呼び出しごとに真に減少するが
  • 無限減少列はない

    ような値があることを型検査器に教えてあげればよいです。

例えば a+b とかはどうでしょう?再帰の度に小さくなっていそうだし、2 より大きいことは確定しているし、良さそうです。 このヒントを付けた型シグネチャが以下になります。

val gcd : a:int{a > 0} -> b:int{b > 0} -> Tot int (decreases %[a+b])

これでもまだ型検査が通りません。型検査器は

  • 関数中の Lt -> gcd b a の辺りで証明が回らないよ!?

などと、どこで検査に失敗したか教えてくれます。たしかに、 gcd a b の中で gcd b a が呼ばれているので、 このケースでは a+b が減っていません。そこで、 「a+b が変わらないときは b の値が減ってるはずだから、(a+b, b)のペアで考えてみて!」と教えることにします。

val gcd : a:int{a > 0} -> b:int{b > 0} -> Tot int (decreases %[a+b; b])

今度は無事に型がつきました。 これでこの関数が確実に停止することが保証されました。

実は x:int{x > 0} という型には pos という別名が定義されています。よって、以下のように書くことも出来ます。

val gcd : a:pos -> b:pos -> Tot int (decreases %[a+b; b])

公約数を返す関数の型

さて、「2つの正整数を受け取ってその公約数を返す」関数の型を定義するために、 まず、 c が a と b の公約数かどうか判定する関数を定義します。

val is_common_factor : pos -> pos -> pos -> bool
let is_common_factor a b c = (a % c = 0) && (b % c = 0)

この関数を使って、欲しい仕様に対応する型シグネチャは以下のように書けます。

val gcd : a:pos -> b:pos -> Tot (c:pos{is_common_factor a b c})
              (decreases %[a+b; b])

なのですが、やっぱり型検査器は証明を見つけられません。 今度は

  • Gt -> gcd (a - b) b のケースで、 gcd (a - b) b が本当に a と b の公約数になってるかどうかわからないよ!

とのことです。

今後ちょいちょい出てくるので、説明の簡単化のために gcd (a - b) b の値を g と名づけます。 帰納法の仮定より g は a - b と b を割り切ることは即座にわかります。ですので、型検査器が苦労しているのはg が a を割り切るかどうかの確認ではないかと予測します。

ここで、「c が a と b の公約数だったら、 c は a+b を割り切る」という補題を仮定します。

val division_distributivity : a:pos -> b:pos -> c:pos{is_common_factor a b c}
        -> Lemma ((a + b) % c = 0)
let division_distributivity a b c = Math.Lemmas.modulo_distributivity a b c
// modulo_distributivity a b c = Lemma ((a + b) % c = (a + (b % c)) % c))

この補題より、 「g が (a-b) と b の公約数だったら、 g は a を割り切る」が言えるので、 必要な場所でコンパイラに教えてあげます。

val gcd : a:pos -> b:pos -> Tot (c:pos{is_common_factor a b c}) (decreases %[a+b; b])
let rec gcd a b =
    match compare_int a b with
    | Gt ->
        let g = gcd (a-b) b in
        division_distributivity (a-b) b g;
        g
    | Lt -> gcd b a
    | Eq -> a

これをコンパイルすると無事に型がつきました。gcd が公約数を返すことが証明されました。

エイリアス

type common_factor (a:pos) (b:pos) = c:pos{is_common_factor a b c}

なる型の別名(型エイリアス)を定義すれば、上の型を

val gcd : a:pos -> b:pos -> Tot (common_factor a b)

くらいにすっきりさせることができます。意味がわかりやすくなりました。

完成したプログラムはこちらです。

あとがき

なんとなく複雑な型を持つ言語の雰囲気が伝わったら幸いです。 ちなみに今日は新暦七夕です。織姫星と彦星にちなんでF starの記事を書きました。

余談

ここのところ型や形式手法についての話題が世間を賑わしていますね!

gfn 氏が静的型付きの組版用言語とその処理系の SATySFiを発表したり github.com

soutaro 氏が Ruby を型検査するシステムSteepを構築したり soutaro.hatenablog.com

バーチャル定理証明士が定理証明動画シリーズを開始したり www.youtube.com

みょん氏が型の強さについての紹介記事を書いてくれたり myuon.github.io

毎日興味深い話題がありドキドキがとまりません。

*1:この場合でもコンパイラはヒントを鵜呑みにせず、そのヒントが正しいかどうかを検査してくれるので正しさは保証されます。