このメモの目的
「型システム入門 プログラミング言語と型の理論」を読む読書会に参加してしまったのですが、単純に読んでもアレなのでメモを取っていくことにします。
嗚呼、これは危険な読書会に参加してしまった･･･（感想）
あまり章立てにこだわらずに書きます。また、数学よりもそれが示す意味についてメモしていきます。
第一章
「型システム」とは
型システムは、プログラムが期待された動作をすることを保証する手助けをする「形式手法」の一種である。他の形式手法に比べて、軽量であり遥かに普及した手法である。（プログラムに関する推論として見た場合）
型システムは、値の性質によって項を分類し、そこから振る舞いの静的な近似を求める。
型システムとはプログラムの悪部分を、それが計算する値の種類に沿って分類することにより、プログラムが有る種の振る舞いを起こさないことを保証する、計算量的に扱いやすい構文的手法である。
型システムは、"ある種の動きを「起こさない」"ことを断定することができる。逆に、"ある種の動きを「起こすこと」"を断定することは出来ない。多分計算結果がもたらす事までは型システムで検査できないということ。
型がコンパイル時に解析されるものを「動的型付け」と呼ぶ。対して、実行時に型を検査してタグとして付けられるものを「静的型付け」と呼ぶ。
型システムの機能
エラーの早期検出
数値解析など扱う情報の種類が少ない場合を除き、型がvalidならばプログラムは期待したとおりに動くことが多い。(経験的に)
抽象化
プログラムのコンポーネントを切り離してモジュールと見なすことを助ける。
そのように見ることで、モジュールと実装を切り離して、プログラムを抽象的に観察できる。
ドキュメント化
プログラムの振る舞いを人間が推測するためのドキュメントになる。
言語の安全性
言語の安全性とは、自らがもたらす抽象を保護していること。(定義に議論はある)
Cの様に型が表現している抽象性を容易に破壊する(メモリを抽象化した型よりも外に書き込める等)ような仕組みは安全ではないと言える。安全であるためには、静的な型検査だけでなく動的に型の抽象性を保護していなければならない。そのため、静的型付け言語・動的型付け言語のどちらであるかは安全性の論点にならない。
効率性
型によって数値の性格を明らかにできるため、適切な機械語を生成できる。
感想
コードを書くときに、型は必ず使う概念だが、具体的にどのようなモノなのか形式的な理解は無かった。そこら辺が補強できたと思う。
また、「言語の安全性」とはどういう概念かフワフワしていたが「言語が提供する抽象化を破壊しない」という所でピンと来た。
数学が苦手な僕にはこの本を読み進めるのは難しそうだ。