静的解析の限界、現実世界との境界

私が最初に静的解析の限界を感じたのは多分依存型で遊んでいたとき

依存型の力はすごくて、まぁそれもそのはず命題論理から述語論理に進んで元への言及ができるので見かけ上表現力はとんでもなく上がるわけです。例えば「ある方程式を満たす解のみを受け取って何かする」みたいな関数が型として表現できるようになる。

一見すると最強に見えるんだけどこれは実質定理証明をすることなので、制限の強い型をつければつけるほど実装で苦しむ羽目になるということを割とすぐ痛感することになった。

例えば head : Vect (Suc n) a -> a で長さ1以上のvectorの先頭を安全に取り出す関数を表現できる。 これはコンストラクタを見るだけなので実装も簡単ですね。 それでは今度は quick_sort : (xs: Vect n a) -> \exists (ys: Vect n a). Increasing ys /\ Isomorphic xs ys (読み方としては、長さnのvectorを受け取って、「長さnのvectorであって、昇順に並んでおり、適当に順番を入れ替えるとxsに一致するもの」を返す関数と読みます)とかどうかというとまぁこれを見てすぐ実装が思いつく人はいないでしょう。

やってみると分かるがこれに実装を与えるためには相当な定理証明力を要求される。もはや関数型プログラミングですらない、単なる定理証明である。

とか言う話は↓にもよくまとまっているのでよければ読んで

• 問題を解決するつもりでキッチリ型を付けた先にある高い壁 - ぼくのぬまち 出張版

• 実世界を扱う依存型プログラミングのたぶん基本～外界から安全な世界までの道 - ぼくのぬまち 出張版

上の記事にも書いてあるんだけど、実は依存型のつらみはこれだけではない(そして今回の記事はむしろこっちの話を書きたい)

例えば先程のquick_sort関数をめでたく実装できたとしよう、すると我々はwell-sortednessが証明されたquick_sortを手にしたことになる。素晴らしい！ではこのquick_sortを使ってみよう！

普通のアプリケーションであればquick_sortにはリストを食わせた後そのまま普通に使ってデータとしては捨てられてしまうかもしれない。quick_sortから返却されたリストが 昇順に並んでいる ことが保証されていなければならないアルゴリズムを書く人がどれだけいるのだろうか？ もちろんソートされていなければ後々まずいことになるということは往々にしてあるが、それが至るところに出現するということはあまりなさそうだ。数百行のプログラム中で1-2ヶ所、たかがその程度だろう。 quick_sortを実装するために支払ったコストは本当にここの嬉しさを上回るのだろうか？

あるいは、もっとひどければ全く利用されないこともある。ソートされたデータを一度DBやファイルに書き出してしまえば、型の保証はなくなってしまう。ファイルに書き込まれる前にソートされたことが型で保証されていたデータは、ファイルから読み出したときにはすでにその保証を失っている。

実際にはシステムレベルでの保証というのがある。ファイルに読み書きされると当然型による保証は失われてしまうが、「そのファイルがこのプログラム以外で読み書きされないことを仮定してよいのなら」ソートされたデータを書き込んだファイルは再び読み込むとソートされているとしてよいはずである。 というわけでプログラムの型レベルでは保証できなくとも、 システム全体がまともに動いているなら ちゃんと制約を満たしてくれているはず、というのがある。

システムレベルでの「保証」とは人間の頭の中にしかなく、通常いくつかの仮定が必要であるので型システムではうまく取り扱うことができず、例えば unsafeCoerce : a -> b のような関数の出番ということになる。

めちゃくちゃ話が変わってTypeScriptの話をする(実はそんなに話は変わらない)。

先に引用をしましょうね

• 漸進的型付けの未来を考える - yu-i9.tmp

• 漸進的型付け言語の時代に必要なもの - mizchi's blog

JS(型なし言語)界隈では漸進的型付けが流行っており、雑に言うとanyを許しつつできるところはできるだけ型つけたい〜みたいなやつ。Pythonのtype hintとかもこの部類。

上にも書いてあるんだけどこの手の仕組みはだいたい「使いたいフレームワークに型ついてないんだけど」が大きな問題として立ちはだかる。

使いたいフレームワークに型がついてないと何が問題かと言うと、APIをコールして戻ってきた値がだいたいanyなので「これ型つける意味ある？？？(ない)」って気持ちになる。

現実世界(js)に言って戻ってきたものはすべてdirtyである、慈悲はないという点では上の依存型の話と共通している。

やはりここではanyからのキャストが欲しくなる。どうしてもというときは仕方ない。

そろそろ大体流れが見えてきたと思うけど、RustでもFFIをしようとすると同じ問題が発生する。

具体的には、FFIでCの関数を呼ぶときに参照を渡してしまうとライフタイムが破壊される。こっち側のシステムではライフタイムパラメータとして &'a A みたいなのが推論されていたとしても、FFIでそれを渡して戻ってきた参照にもはや保証などない。

これもライフタイムパラメーターに対してキャストするしかない。 やるならstd::mem::transmuteかな。

[追記] transmuteしなくても unsafe { &*raw_ptr } でできるよって教えてもらった(https://twitter.com/qnighy/status/1017051171477786626) [/追記]

上のような問題はだいたい似たような話で、 現実世界は型が弱すぎる というのが悪い。 それは人間が欲を書いて型システムなどというものを傲慢にも発明しそれを勝手に使っているのでしょうがないのだけど、とにかく型が強い世界から弱い世界に行くときには静的解析で得られた保証の多くを捨てていかねばならない。

保証を捨てるのは自己責任で構わないが、弱い世界から強い世界に戻るためには入国審査として再びその保証が必要になるので、ここでunsafeなキャストを無理やり行うことになる。

しかしそれは決して悪いことではなくて、そもそもこういう静的解析のある言語も、標準ライブラリや言語のセマンティクスとして内部的にはおよそこういうunsafeキャストでしか説明できないことがたくさんあって、しかしそれらが正しいことはメタ的に(今考えている言語の静的解析よりももう一段上の段階で)開発者たちが頑張って保証してくれていることなので我々は安心して静的解析を用いることができるわけである。

現実世界つらいねで終わってしまうと意味がないと言うか、いやいやそうは言ってもこっちはソフトウェア書いてんだぞという話なので現実的な落とし所が必要になるよねって思う。

上にも少し書いていたが現実的な落とし所としては「システムによる保証」ということになる。

(当たり前だが設計にこのことをしっかり盛り込んだ上で)設計レベルで「このシステムでは次のようなことが保証されている」「この保証を破る操作は一切許されない」というラインを最初に決めてしまおう。 そのライン上では上のような問題が発生したときは神に祈る気持ちで(実際はちゃんと前提を満たしてるかを実行時にassertionかけたりしよう)unsafe castを行おう。

別に難しい話ではなくて「getは冪等」とかそのレベルでいいのである。しかしこのレベルでさえもそれを保証するためには時々unsafeの力が必要になる。そのときには次のようなことに気を配ろう。

• unsafeはユーザー側に露出させないこと

• unsafeは事前に決めた制約を守るときに限って利用すること

• unsafeは弱い世界から強い世界に戻ってくるときに限って利用すること

この3つのこと正しく守っていて、システムが正しく設計されていれば、それはもはやunsafe castではなくsafeな保証の付与という操作である。