篩型
Refinement Types
「この関数は配列型を引数に取るが、その要素数はn以上でないといけない」的な型を書ける
Haskell
refined
参考
Announcing the refinement types library – Functional programming debugs you
refined
を使った概説
#WIP
できること
配列の要素数の静的検査
空配列かどうかを型で表現
ex.
head
に空配列を適用すると実行時エラーになるが、それを防ぐ
ゼロ除算
の防止
etc.
https://ucsd-progsys.github.io/liquidhaskell-tutorial/
LiquidHaskell
http://nikita-volkov.github.io/refined/
Liquid Haskell: Haskell as a Theorem Prover
https://escholarship.org/uc/item/8dm057ws
https://twitter.com/ksuenaga/status/558205113743863808
Refinement Typesを「篩型」と訳した経緯
https://twitter.com/y_taka_23/status/969515905737621506
五十嵐淳
,
末永幸平
#??
Liquid types
はべつもの？
https://en.wikipedia.org/wiki/Refinement_type
https://7colou.red/blog/2018/07-07-difference/index.html
https://goto.ucsd.edu/~nvazou/refinement_types_for_haskell.pdf
https://engineering.visional.inc/blog/168/scala-refined-newtype/
Scala