Chapter 08

2.2 型は合成可能性が主題

さのたけと
さのたけと
2021.05.04に更新

圏論は射の合成が主題である.しかしどんな二つの射も合成可能とは限らない.射(矢印)の終点にある対象は,次の射の始点でなければならない.プログラミングでは,一つの関数の戻り値を次の関数に渡す.このとき,次の関数が前の関数の戻り値を適切に受け取ることができなかったら,プログラムは正しく動作しない.合成がうまく行くためには,終点と始点で型が適合していないといけない.言語の型システムが強ければ強いほど,この適合はうまく表現され,機械的に検証しやすくなる.

強い型チェックに対して私が聞く唯一の真剣な異論は,それが意味的に正しいプログラムを拒否してしまう可能性があるということだ.実際には,このようなことは滅多に起きない上に,どんな言語もこういうことが真に必要なケースにおいてはバックドアを用意しているものである.Haskell にすら unsafeCoerce がある.しかしそのような機能を使うことには慎重でなければいけない.カフカが描いた人物グレゴール・ザムザは,巨大な昆虫に変身するときに型システムを破壊してしまい,その結末がどうなるかは誰もが知るところだ.

もう一つよく聞く異論は,型の扱いはプログラマに過剰に負担をかけているというものだ.これは共感できる,特に C++ で iterator の宣言を自分で書かなきゃいけないときに.しかし今は 型推論 (type inference) という技術があり,型を明示しなくてもコンパイラが推論してくれるのだ.C++ でも今は変数を auto で宣言して,コンパイラにその型を推論させることができる.

Haskell では,例外的な状況を除いて,型注釈をつけることは任意である.プログラマはどちらにせよそれを使う傾向がある,なぜならコードの意味が分かりやすくなり,コンパイルエラーが読みやすくなるから.Haskell ではまず型の設計からプロジェクトを始めるのが慣例だ.後に,型注釈は実装を推進し,コンパイラによって強化されたコメントとなる.

強い型付けはコードのテストをしない言い訳によく使われる.Haskell プログラマは時折言う,"コンパイルが通るなら,それは正しいはずだ".もちろん,型が正しいプログラムが正しい結果を出力する保証はない.このような紳士的な態度[1]の結果は,いくつかの調査によると,コードの品質に関して多くの人が期待するほどに群を抜いているということもなかった.どうやら,商業的な観点からは,バグを抑制する圧力は一定のレベルまでしか働かず,それはソフトウェア開発の経済力とエンドユーザの寛容さだけで決まるもので,プログラミング言語や開発手法とはほぼ関係がない.より良い指標は,どれだけのプロジェクトがスケジュールに間に合わなかったかや,大幅な機能削減と共にリリースされたかだろう.

単体テストが強い型付けの代わりになるという主張に関しては,次のよくあるリファクタリングの状況を考えてみればいい:特定の関数の型を変えること.強く型付けされた言語では,関数の宣言を変更し,ビルドエラーを全て修正すれば良い.弱く型付けされた言語では,その関数が別のデータを受け付けるようになったという事実は,その呼び出し元まで伝播されない.単体テストはいくらかのミスを見つけるかも知れないが,テストは確率的なプロセスであって,決定的なものではない.テストは証明の代替としては貧弱だ.

(和訳:@taketo1024

脚注
  1. 原文:cavalier attitude ↩︎