型推論について
暇をみつけては python の型推論をやっている (やろうとしている)。でも、いまだに本当にこれが「原理的に可能」なのかどうか疑問だ…。
http://www.unixuser.org/~euske/offline/memo/cur/cur.html#180812
「原理的に可能」とかについて．
まず「原理的に可能」の意味を考える必要がある．「可能」ってなに?なにができたら「可能」なの?
型推論とかのプログラム解析の技術を評価する場合，二つの性質が重要になる．「健全性」と「完全性」．「型推論が健全性を持っている」というのは，「型が推論できたら，そのプログラムは正しい」ということ*1．「型推論が完全性を持っている」というのは，「正しいプログラムは必ず型が推論できる」ということ．MLなんかの型推論は，完全かつ健全である．非常に良くできた型推論アルゴリズムと言える．ただし，型推論アルゴリズムというのは，型システムに基づいて考えるべきものなので，型システムがクソだった場合はいくら完全かつ健全な型推論アルゴリズムだったとしても使いものになるかはわからない．一般的に，完全性と健全性を考えると，完全性は保つのが困難で健全性は保つのが比較的容易である．
実は，この二つの性質も，それだけではあんまり意味はない．良く見ると，「どういう入力に対してもfalseを返す型推論アルゴリズム」は健全であるし，「どういう入力に対してもtrueを返す型推論アルゴリズム」は完全になる．どういう型システムに対して型推論アルゴリズムが定義されているのか，というのが非常に重要になる．
あと完全性と健全性を両立できない場合は，健全性だけでも成り立たせるのが常套手段．「たまにfalse positiveが出るけどtrueって返ってきたらOK」なシステムと，「たまにfalse negativeが出るので，trueって返ってきても大丈夫かよくわからない」システムだと，当然前者の方が使い勝手が良い．
そういうわけで，型推論の話に戻ろう．
まず，完全な型推論アルゴリズムというのは，Pythonのような動的な(evalのある)言語においては，そもそも不可能である．だってevalあるんだもん．「ここでユーザー入力をevalするけど，絶対ここでintが入力されるもんね．絶対だもんね．命かけていいもんね」とか言って型推論しても，実際のユーザーが文字列を入力したら，そこで型推論の完全性は破れる．完全性は諦めよう．
次に健全性の問題になる．一番簡単かつ確実なのは，さっき言ったように「どんなプログラムを入力してもfalseを返す」ことだけど，まあ常識的に言えばこういうのは無意味だ．
そもそも，型推論というのは，何ができたら「OK」なのか，を考えなくてはいけない．これがMLやCなら，話は簡単で，「プログラムが未定義の状態にならない」ことが保証できれば，それで良い．MLの型推論というのは，そういう発想の基で実装されている．未定義の状態というのは，例えば「関数を呼びだしてみたら，実はintだった」とか，そういう状態．わけわかんない．多分，Bus errorとか言って落ちる．MLは安全な言語なので，こういう状態にならないことが，型システムによって保証されている．つまり「let f = 1 in f x」とかいうプログラムは，型推論の時点で拒否される．Pythonだと，そういうことにはならない．「そんなメソッド無いもんね」とか「メソッドの引数が違うからどうしたいいかわかんない」といった状態になっても，例外が上がって来る．「例外が上がる」という挙動が定義されているんだから，それは未定義の状態ではない．そもそも例外っていうのはプログラム中で扱われる値なんだから，その値を処理できる時点で，Cとかの「未定義」とは全然違う．
そういうわけで，なにができたらOKなのかを，まず決める必要がある．私は，「Rubyにおいて未定義メソッドの呼び出しを検出できる」というのを目標にした．この目標は，「型システム」という形で，形式的に表現する．そのうえで，型推論アルゴリズムを定義して，それが私が定義した型システムについて健全である，と言う．
なにが言いたいのかよくわからなくなって来たので，おわりにします．わかりにくいと思う．つまり，「原理的に可能」って言っても，「それだけでは意味を成さない」ということかも．でも意味を成さなければいけないもんでもないと思うけど．
ちなみに私に言わせれば，「型推論」でやろうとするのは「原理的に不可能」である．「原理的に不可能」でも，「実用上十分」なものはできる可能性はある．「フロー解析」でやるのは「原理的に可能」と言って良いんじゃないかと思う．ただし下で説明するように，計算量などの問題があるので「実用的」なものができるかはわからない．
*1:「正しい」の意味がまた問題になるんだけど，それは後で
