如何将一个类型约束为另一个类型的子集？

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定义为提取器。