「この関数は配列型を引数に取るが、その要素数はn以上でないといけない」的な型を書ける

Haskell

参考

refinedを使った概説

できること

配列の要素数の静的検査

空配列かどうかを型で表現

ex. head に空配列を適用すると実行時エラーになるが、それを防ぐ

ゼロ除算の防止

etc.

Refinement Typesを「篩型」と訳した経緯

五十嵐淳, 末永幸平

Liquid typesはべつもの？

Scala