型安全性とは何か−簡単な考察

型安全性とは何か、という議論は時々起きるのだけど、なんだか(個人的には)分かりにくい議論だなあと思ってみていた。この辺、TAPLにはもちろんきちんと定義してあるのだけど、ちょっと狭いというか、型ってもっといろんなことができるのになあ、という気がしてしまう。

というわけで、ここでは

という整理を提案してみたい。あくまで提案なので、これがどこかの研究者コミュニティが使っている定義であるとか、そういう主張はしない。

TAPLでの定義

TAPLではまず、プログラムが未定義な状態になることを、項の評価が途中で止まって値にまで落ちないことで、モデル化している(3.5.15)。さらにこの定義から型安全性を次のように定義している。

もっと広義の型安全性

ただ、この定義はちょっと狭いように感じられる。つまり、項の評価が途中でとまらない(実際のコンピュータでは未定義な状態にならない)、という性質だけを保証しようとしているけれど、型体系を使うともっといろいろなことができるはず。

例えば単純型付きλ計算やSystem Fでは、型が付く項は、かならず演算が停止することが保証されている。

また、依存型を使えば、ほぼあらゆる仕様が、その項が型をもつことで書ける。 もっと実用的な例で言うと、抽象型を使うことで、その内部データ構造にあるinvariantがいつも成り立つように出来る。まあたとえば、文字列処理の時に複数の文字コードが混ざらないようにする、といったことができる。

提案

というわけで、型安全性を次のpreservationだけを意味することしてはどうか

まあダメな例とかすぐ出てくるかもしれないけど。