型と仕様の間の乖離をなくす

型を完全に信頼できるものとして定義する

「型エラーがないなら、何を入れてもok」という状態にする

型レベルで間違った操作をさせないデザインをする

仕様に変更が加わった時は、まず型を直す

そうすれば型エラーが出るので、そこだけ直しにいけばいい

型エラーをToDoリストとして使うことができる

最初に定義する際に仕様変更時に型エラーを生じさせるように実装しておく必要がある

これを実現するためには、

使用している言語が持っている型システムの能力にも依存するし、

型の設計の仕方にも依存する

これは型システムが持っている複数の能力の内、InterfaceやModelingのみに着目した話をしている

型安全性とは独立してマシにしたい

「型エラーがないなら、実行時エラーもない」状態が理想

いわゆる型安全性(健全性)

すべての型システムでそれができるわけではないが、それに近づくように設計したい

ただし、型安全性は実行時エラーを起こさないための最低限(?)のコンパイラの要請であって、「仕様」とまでは言えない

例えばここでも言及されているが

data Nat = Zero | Succ Nat は自然数の型として最良ではない

x = Succ x という値が書けてしまう

例えばUserEntityのage propertyは number では弱い

-1 歳を入れることができてしまう

依存型とか篩型とかがあればどうにかなる

仕様、設計として、「この型に準拠さえしていれば何を入れてもok」という状態にしたい

型で数値の制約を作る

branded typesやOpaque Type

『関数プログラミング実践入門』7章にも書いてる

型と型生成関数を用意しておけば実現できる

この生成関数を使う以外でこの型を生成できないようにしないといけない

その言語の型でカバーできない場合は、

テストを頼る

Linterを頼る

などもする