型システムは何を保証してくれないのか
型を信じている。 信じているからこそ、型が何を保証しないのかを、ときどき確かめておきたくなる。
型は「形」を証明する
型システム が証明してくれるのは、値の形だ。
この関数は i32 を受け取り String を返す──そういう約束が、コンパイル時に破られないことを保証する。
これは強力だ。 形が合っていることの確認を、人間が毎回やらなくて済む。 nullを踏む、フィールド名を打ち間違える、そういう退屈なミスの大半が消える。
けれど「正しさ」は証明しない
問題は、形が合っていることと、意味が正しいことは別だという点だ。
fn add(a: i32, b: i32) -> i32 の中身が a - b でも、型は通る。
型は「i32 を二つ受けて i32 を返す」ことしか見ていない。
足し算が引き算にすり替わっていても、型システムにとっては正しい関数だ。
型は形を証明する。正しさは証明しない。この一線を曖昧にすると、型を過信して検証を省くようになる。
形の保証と意味の保証のあいだには、テストや証明という別の層が必要になる。
型が見ていない実行時の世界
さらに型が見ないものがある。 実行時のメモリの状態だ。
長時間動くプロセスで起きるメモリの 断片化 は、型の知るところではない。
確保と解放を繰り返すうちに使える隙間が虫食いになっていく現象を、Vec<u8> という型は何も語らない。
値の アラインメント が崩れて性能が落ちても、型は同じ型のままだ。
型はメモリの「形」の上澄みだけを見ていて、その下で起きる物理的な事情には触れない。
だから型を、過不足なく信じる
型を信じすぎると、検証を型に肩代わりさせようとして失敗する。 型を軽んじると、退屈なミスに時間を溶かす。
ちょうどいい距離は、「型は形を保証する道具であって、正しさと実行時の世界は別途見る」と割り切ることだと思う。 保証してくれない範囲を知っているほど、型を安心して使えるようになる。