型安全性

https://postd.cc/wp/wp-content/uploads/2014/09/typing-venn.jpg

型検査を通過したなら、意味論的に未定義な状態にならない

検査済みのバグは実行時には絶対に起こらない

そもそも安全性とは

(型関係なく一般に)プログラムが言語で定義していない状態にならない性質

ランタイムやインタプリタが検出して異常終了するような場合も「安全」

型検査で検査する範囲と、実行時に検査する範囲が決まっている

この両方の枠を超えたところが未定義な箇所

未定義な箇所にいくのは「安全ではない」

「型安全性」は型検査を通過したプログラムが、実行時にチェックできない感じにならなければいい

実行時にチェックしない箇所を、型検査でもチェックしなければ、「型安全」とは言えない

例えば、演算の型が不整合だと、演算できなくてエラーになる

例えば無理やり型検査器を外して実行させたら、未定義な状態になる

これは実行時に↑こういう演算の処理が未定義の場合

動的型付けの言語の場合は、実行時に動的に型検査をする

実行時に具体的な値を見て型検査をする

実行時の検査で、値が不整合だとわかると、計算を止めること、ができるから

定義により、これは型安全といえる

値が型情報を持ち回っている

動的型付けの言語は型安全

よって「型システムがなくても、型安全」という状況はあり得る？

実行環境の定義を強くすればいい

これが動的型付けの言語のようなもの

型エラーがないとき、バグがあるかどうかは言ってない

型エラーがあるときに、バグがあるか、バグがないかは言っていない

こっちも同じ

ということを言っている

なので目指すべきは健全性と完全性を兼ね備えた型システムなのである

型システムの健全性

逆に言えば、正しく型付けされていれば行き詰まり状態にはならない

一方で、これは型エラーが強力すぎるケースもある

code:ts

// この関数の戻り地はstring

const returnString = (): string => {

if (true) {

return 'string'; // 条件がtrueなので100%こちらが評価される

} else {

return 42; // error: Type '42' is not assignable to type 'string'.

}

};

つまり、実際にはバグはないのに、型エラーになることもある

then/else節の型が異なるから。

実際は動くのにも関わらず、型エラーと言われる

逆に、型エラーがあるならば、バグがあるかもしれない

バグはあるかもしれないし、ないかもしれない

意味論的に未定義な状態ってなんやねん

言語による

言語によってバグの定義が異なる

その言語が定義していない、未定義な挙動のこと

例えば

暗黙的な型変換

nullポインタ

danglingポインタ

環境に束縛されていないような変数を参照することによるエラー

操作と値の種類の不整合のエラー

算術計算の引数に数値以外の値が与えられる

if式の条件部に真偽値以外の値が与えられる

etc.

etc.

参考

型安全でない言語の例

「弱い型付け」と紹介される言語

つまり、CやC++

型安全でない言語は何のために型があるのか

そもそも型は別にそれだけの用途ではない

null安全ではないだけで、intとcharとかは間違っていれば怒ってくれるのか

castしたら無意味だったりする？

メモリ確保時のサイズの判定になるのか

それとも例えばラムダ計算のような計算モデルとか、言語とは？みたいな意味論のところの追求がモチベなの？

最初は計算モデルのところから発祥して、お、これ静的検査に使えるやん！ってなったとか？

構文規則をもっと厳密に定義していけば、意味解析の必要はなくなったりする？

めっちゃ複雑にはなりそうだけども

参考

途中までしか読んでないけど良さそう

専門家の間でも「型安全」の議論がわかれる