如何將一個類型約束爲另一個類型的子集？

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

Coq和Agda等語言中的依賴於值的鍵入可以做到這一點，但不是Scala。

根據確切的使用情況，可以在類型系統中編碼peano數字，但可以幫助您。

你也可能會想嘗試一些密封抽象超（OddOrEven也許），並返回從任何給定整數正確的實例工廠方法沿着限定兩個Even和Odd。

另一種可能性是將Even定義爲提取器。