Pythonで関数型言語の依存型と篩型の型クラスを宣言する方法 - Qiita

問題意識の所在 自作クラスを宣言するときに、定義するクラスが用いるデータ型に制約を与えるだけでなく、そのクラスのインスタンスが__持ちうる値の範囲や、長さの範囲についても制約を与える__ことができる言語は、__依存型や篩型の型クラスを宣言できる言語__として、知られています。篩型は、「ふるい」型と読みます。 __データ型に「要素数」や「長さ」といった数的な制約条件を持ち込むことで、どんな実用的なご利益があるのか？という素朴な疑問__に答える上で、次の記事が参考になります。 @junjihashimoto@githubさん 「依存型の紹介と応用としてのClashの紹介」 型に値を埋め込むだけだとありがたみがないですが、カリー＝ハワード同型対応で「プログラム＝証明」(proofs-as-programs)・「型＝命題」(formulae-as-types)といわれているので、証明をやるにはリッ