是否可以通过创建类似PositiveInt的东西来限制Int并在Scala中进行编译时检查？

Question

是否可以创建一个受限制的 Int,例如PositiveInt,并对其进行编译时检查？换句话说,可以定义一个方法,例如:

def myMethod(x: PositiveInt) = x + 1

然后有类似的东西:

myMethod(-5) // does not compile
myMethod(0)  // does not compile
myMethod(5)  // compiles

如果这是可能的,我应该如何开始定义PositiveInt,我的意思是在Scala中有一个方便的技术吗？

Answer 1

这种事情被称为依赖类型,不,它在Scala中不可用.

Answer 2

您可以通过以下方式在原始类型上使用标记特征

trait Positive
type PosInt = Int with Positive
def makePositive(i: Int): Option[PosInt] = if(i < 0) None else Some(i.asInstanceOf[PosInt])
def succ(i: PosInt): PosInt = (i + 1).asInstanceOf[PosInt]

但是您只会在写入时遇到运行时错误makePositive(-5)。写入时您将收到编译时错误succ(5)。

可能可以编写一个编译器插件，将正整数文字“提升”为标记类型。

编辑

我还没有测试以这种方式标记基本类型是否有任何运行时开销。

Answer 3

如果你有编译时依赖的类型检查，你解决了停机问题，或者你的编译器并不总是保证完成编译，或者你的编程语言的语法需要图灵完备，所有这些都是荒谬的。

这是运行时依赖类型的合理替代方案

object ScalaDependentTyping extends App {

  implicit class NaturalNumber(val x: Int) {
    assume(x >= 0)
  }

  implicit def toInt(y: NaturalNumber): Int = y.x

  def addOne(n: NaturalNumber) = n+1

  println(addOne(0))
  println(addOne(1))
  println(addOne(2))

  println(addOne(-1))  //exception
}