型安全性
型検査における健全性
正しく型付けできたなら、行き詰まり状態にならない性質
型検査を通過したなら、意味論的に未定義な状態にならない
検査済みのバグは実行時には絶対に起こらない
そもそも安全性とは
(型関係なく一般に)プログラムが言語で定義していない状態にならない性質
ランタイムやインタプリタが検出して異常終了するような場合も「安全」
型検査で検査する範囲と、実行時に検査する範囲が決まっている
この両方の枠を超えたところが未定義な箇所
未定義な箇所にいくのは「安全ではない」
「型安全性」は型検査を通過したプログラムが、実行時にチェックできない感じにならなければいい
例えば配列の境界検査は多くの場合、「実行時に検査する」と定義されているので、型検査でスルーされること自体は問題ではない
実行時にチェックしない箇所を、型検査でもチェックしなければ、「型安全」とは言えない
例えば、演算の型が不整合だと、演算できなくてエラーになる
例えば無理やり型検査器を外して実行させたら、未定義な状態になる
1+true は定義されてないのに無理やり演算させるこれは実行時に↑こういう演算の処理が未定義の場合
動的型付けの言語の場合は、実行時に動的に型検査をする
実行時に具体的な値を見て型検査をする
演算によって未定義な状態にならないのか
実行時の検査で、値が不整合だとわかると、計算を止めること、ができるから
定義により、これは型安全といえる
値が型情報を持ち回っている
動的型付けの言語は型安全
よって「型システムがなくても、型安全」という状況はあり得る？
実行環境の定義を強くすればいい
これが動的型付けの言語のようなもの
静的な環境ではuni-typedだと考えられる
ex. PythonのPyObject
型エラーがないとき、バグがあるかどうかは言ってない
型エラーがあるときに、バグがあるか、バグがないかは言っていない
こっちも同じ
ということを言っている
なので目指すべきは健全性と完全性を兼ね備えた型システムなのである
実際難しいらしい
型システムの健全性
正しく型付けされた項は行き詰まり状態になることはない、という性質
逆に言えば、正しく型付けされていれば行き詰まり状態にはならない
一方で、これは型エラーが強力すぎるケースもある
ts// この関数の戻り地はstring
const returnString = (): string => {
if (true) {
return 'string'; // 条件がtrueなので100%こちらが評価される
} else {
return 42; // error: Type '42' is not assignable to type 'string'.
}
};つまり、実際にはバグはないのに、型エラーになることもある
例えば
if true then 0 else false などもちろん規則にも依るが、TaPLp.70のT-IFのように定義されていれば型エラーになる
then/else節の型が異なるから。
実際は動くのにも関わらず、型エラーと言われる
ここで言っているのは、必ず
then 節が評価されるから「この式は絶対にnumberを返すので、バグはない」って意味であって、条件のところが本当に
true/false どちらになるかわからないときはこの式は明らかにバグである(型的に)逆に、型エラーがあるならば、バグがあるかもしれない
バグはあるかもしれないし、ないかもしれない
意味論的に未定義な状態ってなんやねん
言語による
言語によってバグの定義が異なる
その言語が定義していない、未定義な挙動のこと
例えば
暗黙的な型変換
メモリリークとか
nullポインタ
danglingポインタ
環境に束縛されていないような変数を参照することによるエラー
操作と値の種類の不整合のエラー
算術計算の引数に数値以外の値が与えられる
if式の条件部に真偽値以外の値が与えられる
etc.
etc.
Rustの未定義な挙動の例 ref
参考
型安全性入門 p.10
今作ったある型システムが、ちゃんと型安全性を満たしているかどうかを、進行定理と型保存定理を使って示す、という感じなのかな
型安全でない言語の例
「弱い型付け」と紹介される言語
つまり、CやC++
型安全でない言語は何のために型があるのか
そもそも型は別にそれだけの用途ではない
null安全ではないだけで、intとcharとかは間違っていれば怒ってくれるのか
castしたら無意味だったりする？
メモリ確保時のサイズの判定になるのか
型理論の研究って、コンパイル時の静的検査がモチベなの？
それとも例えばラムダ計算のような計算モデルとか、言語とは？みたいな意味論のところの追求がモチベなの？
最初は計算モデルのところから発祥して、お、これ静的検査に使えるやん！ってなったとか？
1+true のような意味論的未定義が起こるのは、構文規則がショボいからという見方もできる？構文規則をもっと厳密に定義していけば、意味解析の必要はなくなったりする？
めっちゃ複雑にはなりそうだけども
コンパイルのフェーズをどこで分けるか問題だな
動的型付けの言語を自作すればわかるのか
参考
何度でも読み返したい
TaPL p.72
途中までしか読んでないけど良さそう
専門家の間でも「型安全」の議論がわかれる