型の目を、すりぬけるもの
残しておいた宿題
ここまでの6つのレッスンで、型の目はずっと頼もしい味方でした。実行する前に、すべての道を読んで、種類のつじつまが合わないまちがいを残らず捕まえてくれました。
では、これは捕まえられるでしょうか。
1 / 0レッスン3で「1 / 0 は素通りする」と予告だけして、通り過ぎたのを覚えていますか。今日はその宿題を回収する日——型の目の限界を、正直に見にいくレッスンです。
すりぬけ その1——0で割る
まず、実験です。型検査と実行、両方の返事を見くらべてください。
型のまちがいは、見つかりませんでした。
0では割れませんでした。
型の目は「型のまちがいは、見つかりませんでした。」と通しました。なのに実行は「0では割れませんでした。」と転びます。実行前の検査が見逃したまちがいを、実行が捕まえた——レッスン1と、立場が逆です。
なぜ通したのか。型の表を引くと、/ が受け取るのは「数 と 数」——1 は数、0 も数で、つじつまは完璧だからです。0は型ではなく、値なのです。
思い出してください。型の読みは「封を切らずに仕分ける」読み方でした。封を切らないからこそすべての道を読めるのですが、封を切らないからこそ、中身の値——その数がたまたま0かどうか——は見えません。
⟡ よりみち：0を、数の国から追い出せないか
「0だけ別の型にすれば捕まえられるのでは」——よい着眼です。実際、「0でない数」のような細かい型を持つ言語は研究されていて、一部は実用にもなっています。ただし型を細かくするほど、つじつまの確認は難しくなり、書く人の手間も増えます。どこまで型に語らせるかは、言語設計の現在進行形の問いです。
すりぬけ その2——止まらないくりかえし
次の実験です。コース2で作ったwhileに、ご登場願います。
型のまちがいは、見つかりませんでした。
i数プログラムがいつまでも とまりませんでした。くりかえしの「終わる条件」は、いつか本当に成り立ちますか？
型の目を、たどってみます。i は数、i > 0 は「数 と 数」をくらべるので真偽、whileの条件としてつじつまが合い、i + 1 も数。どこにも、ほころびがありません。
なのに実行すると「プログラムがいつまでも とまりませんでした。」——燃料切れです。i は増える一方で、i > 0 が false になる日は来ません。
これは型の目の手抜きでしょうか。ちがいます——「このプログラムは止まるか」を実行せずに必ず言い当てることは、どんな検査にも原理的にできないと証明されているのです。停止性問題と呼ばれる、計算そのものの限界です（コース5で、証明まで詳しく歩きます）。
レッスン1で「実行前の検査には、登れない崖と、登れる丘がある」と言いました。型の目が止まらないループを通すのは、丘の上にとどまっている証拠——崖に手を出さないからこそ、型検査は必ず終わり、必ず答えを返せるのです。
すりぬけ その3——意図のまちがい
最後の実験が、いちばんたちが悪いものです。a と b の平均を出すつもりで、(a + b) / 2 と書くべきところを——かっこを忘れて a + b / 2 と書いてしまったとします。
型のまちがいは、見つかりませんでした。
a数b数正しい版の答えは 15。では最後の行を a + b / 2 に変えてみてください。わり算が先にまとまるので b / 2 が 10、それに a を足して——答えは 20 になります。
注目してほしいのは、型の目がどちらも通すことです。どちらも数と数の合法な計算で、種類のつじつまに、けちのつけようがありません。しかも今度は実行さえ転ばず、まちがった答えが静かに出てきます。
前のレッスンで「型は意味までは語らない」と言いました。その延長線の、いちばん遠い地点がここです。「平均を出したい」という意図は、プログラムのどの行にも書かれていない——書かれていないものは、どんな検査にも読めません。
3つのすりぬけの、正体
並べてみると、すりぬけたものの正体が見えてきます。
| すりぬけ | 型の目に見えなかったもの |
|---|---|
1 / 0 | 値——その数が、たまたま0かどうか |
| 止まらないwhile | 時間——実行が、いつか終わるかどうか |
| かっこ忘れの平均 | 意図——何を計算したかったのか |
型の目が見ているのは、種類のつじつま、それだけです。レッスン1の言い方に戻るなら——実行は一本の道しか歩けないかわりに、道の上の石ころにちゃんとつまずいてくれます。型の目はすべての道を見わたせるかわりに、道の上の石ころまでは見ていないのです。
それでも、型を使う理由
ここまで読んで、「型、思ったより頼りない」と感じたかもしれません。でも見方を変えてください——種類のまちがいというまちがいの一種類が、丸ごと消えるのです。
「数に真偽を足す」たぐいのまちがいは、どの道に隠れていようと、実行前に全部捕まる。書く人は、その種類の心配をしなくてよくなる。まちがいの種類がひとつ消えるだけで、残りの心配——値と、時間と、意図——に集中できます。
では残りは誰が見るのか。テストです——実行する検査であるテストは、実際の値でプログラムを走らせるので、0除算にもまちがった平均にもつまずけます。テストと型は競争相手ではなく、分業なのです。
ただし、ここでも正直でいましょう。二枚重ねても、すりぬけるまちがいはあります——完璧な検査は存在しません。だからこそ「どのざるが何をこせるか」を知っていることが、書く人の腕になるのです。
✎ 演習：すりぬけるか、捕まるか
次の3つを、実行する前に予言してください——型の目は通すでしょうか。通すなら、実行で何が起きるでしょうか。予言してから、上の実験室で確かめます。
10 / (5 - 5)- 3から1ずつ減らして止めるつもりで、
-を+と書いてしまった：i = 3のあとwhile i > 0 { i = i + 1 } 1 + (2 == 2)
ヒント1（考え方）
それぞれのまちがいが「種類」「値」「時間」「意図」のどれに属するかを考えてください。型の目が捕まえられるのは、ひとつだけです。
こたえ
1は通します。5 - 5 は型の表では立派な「数」で、その値が0になることは見えません。実行すると「0では割れませんでした。」と転びます。
2も通します。型のつじつまは全部合っていて、実行すると燃料切れです。元をたどれば - と + の書きまちがい——意図のまちがいが時間のまちがいを生んだ例で、すりぬけは重なって起こることもあります。
3は捕まえます。真偽に数を足す——これは種類のつじつまの問題なので、型の目のど真ん中の守備範囲です。
このレッスンで分かったこと
- 型の目が見ているのは種類のつじつまだけ。値（0かどうか）・時間（止まるかどうか）・意図（何を計算したかったか）は見えない
- 止まらないループを通すのは手抜きではない——「止まるか」の判定は原理的に不可能（停止性問題。コース5で証明まで歩く）
- 意図のまちがいは、エラーにすらならずに、まちがった答えを静かに返す
- それでも型を使うのは、まちがいの一種類が丸ごと消えるから
- テストと型は、網の目のちがう二枚のざる——競争相手ではなく分業。ただし二枚重ねても、完璧にはならない