型は仕様
型と仕様の間の乖離をなくす
型を完全に信頼できるものとして定義する
「型エラーがないなら、何を入れてもok」という状態にする
仕様に変更が加わった時は、まず型を直す
そうすれば型エラーが出るので、そこだけ直しにいけばいい
これを実現するためには、
使用している言語が持っている型システムの能力にも依存するし、
型の設計の仕方にも依存する
これは型システムが持っている複数の能力の内、InterfaceやModelingのみに着目した話をしているmrsekut.icon
型安全性とは独立してマシにしたい
「型エラーがないなら、実行時エラーもない」状態が理想
すべての型システムでそれができるわけではないが、それに近づくように設計したい
ただし、型安全性は実行時エラーを起こさないための最低限(?)のコンパイラの要請であって、「仕様」とまでは言えないmrsekut.icon
data Nat = Zero | Succ Nat は自然数の型として最良ではない
x = Succ xという値が書けてしまう
例えばUserEntityのage propertyはnumberでは弱い
-1歳を入れることができてしまう
依存型とか篩型とかがあればどうにかなる
仕様、設計として、「この型に準拠さえしていれば何を入れてもok」という状態にしたい
型で数値の制約を作る
branded typesやOpaque Type
型と型生成関数を用意しておけば実現できる
この生成関数を使う以外でこの型を生成できないようにしないといけない
その言語の型でカバーできない場合は、
テストを頼る
Linterを頼る
などもする