グローバルプロパティのためのローカル推論
ソフトウェア設計において、グローバルな性質（プロパティ）を保証するためには、コードベース全体を理解するのではなく、局所的な（ローカルな）推論によってそれを実現する方法が重要である。本記事では、関数型プログラミングや型システムを活用することで、大域的な不変条件を局所的な構造に埋め込み、スケーラブルで保守性の高いシステムを構築する手法について論じる。
背景メモ
- ローリー・トラット（Laurie Tratt）は、英国のプログラミング言語研究者で、Convergeやパターンマッチング言語の設計で知られる。本稿は、ソフトウェアにおける「ローカル推論（局所的なコード変更から全体の振る舞いを判断する能力）」と「グローバルプロパティ（システム全体にわたる性質）」のジレンマを論じている。
- 例として、代入禁止の純粋関数型言語なら参照透明性が保証されるが、現実の多くの言語（Python、Java、Rust等）は可変状態やエイリアスを許すため、ある関数の内部だけ見ても副作用やスレッド安全性を確信できない。
- 現代の型システム（Rustの借用チェッカー、HaskellのIOモナド、Ponyの参照ケイパビリティ）は、伝統的なオブジェクト指向言語よりこの問題を改善する試みだが、それでも完全なローカル推論には至らないことが多い。
- この話題は、プログラム検証、言語設計のトレードオフ、そして「変更に強いコード」をどう書くかというソフトウェア工学分野の根幹に関わる。