タイプを別のタイプのサブセットに拘束する方法は？

Question

私はそれを持っていますこれはダムの質問感じですが、ここに行く...別のタイプの要素のサブセットであるタイプを定義することはできますか？ここでは簡単な例を示します。

scala> class Even(i: Int) { 
    | assert(i % 2 == 0) 
    | } 
defined class Even 

scala> new Even(3) 
java.lang.AssertionError: assertion failed 

これはランタイムチェックです。コンパイル時にチェックされるような型を定義できますか？ IEの入力パラメータiは常に偶数であることがわかりますか？

Answer 1

Scalaではなく、CoqやAgdaなどの言語で値に依存した型指定を行うことができます。

正確なユースケースにもよりますが、タイプシステムでは、あなたを助けるかもしれないピーノ数字をエンコードする方法があります。

また、いくつかの密閉された抽象スーパータイプ（おそらくOddOrEven）と任意の整数から正しいインスタンスを返すファクトリメソッドと一緒にEvenとOddの両方を定義しようとする場合があります。

もう1つの可能性は、抽出器としてEvenを定義することです。