type witness
>#WIP
runtime evidenceとかもだいたい同じものを指していそう
とある値？
多相的な値に対する型情報を使って、型検査時にそれを利用できる
>In simple terms, a runtime witness is a value that in some way holds some type-level information associated with a polymorphic value and makes it available to the type checking process.
先にGADTsをちゃんと理解したい
GADTを使った幽霊型のような感じがある
仕様を満たした型の作り方のいち案として、↓こういうのもあるよ、というのを提案している
hsdata User (ut :: UserPrivilege) = User { userId :: Integer, userName :: String }これ、値のfieldにadminとかを持たせずに、型でのみやるということだけど、
わざわざこれを選択する理由はなにか？
値で持っているか否かは、ここではあまり重要ではない
重要なのは、型レベルで「そのUserはAdminである」ことを判別できるかどうか
↓このような定義だとそれができない
hsdata User = User { userId :: Integer, userName :: String, userPrivilege :: UserPrivilege } if userPrivilege == Admin みたいなことを書けば分岐はできるけど、型レベルでそれができていないこのままだとアドミンのみを受け取る関数を型安全に定義できない
GADT復習してもっかい読もう
てをうごかして確認したほうがいい