Можно ли ограничить Int, создавая что-то вроде PositiveInt и проверяя время компиляции в 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

Другие ответы касаются в основном вопроса о создании типа «положительное число», которое относится к типу «число» таким образом, чтобы компилятор мог гарантировать корректность.Например, с зависимыми типами вы можете доказать, что реализация таких функций, как abs, является правильной.Вы не можете сделать это с помощью scala.

Однако вы можете создать тип, представляющий положительные целые числа и ничего больше.Например:

abstract class Pos {
  def toInt: Int
}

case object Zero extends Pos {
  def toInt: Int = 0
}

case class Next(x: Pos) extends Pos {
  def toInt: Int = 1 + x.toInt
}

object Pos {
  def apply(x: Int): Pos =
    x match {
      case n if (n < 0) => throw new IllegalArgumentException(s"$x is not a positive integer")
      case 0 => Zero
      case n => Next(Pos(n-1))
    }
}

Это похоже на то, что предложил ziggystar, с той разницей, что правильность типа гарантируется его собственной конструкцией, а не конструктором.То есть невозможно представить отрицательное число с этим типом.

Этот подход, вероятно, не будет практичным для ваших целей.Вам либо нужно реализовать все операции для него, либо добавить значение Int, которое затем эквивалентно простой проверке во время выполнения, поскольку вы теряете всю безопасность типов, которую выиграли, представляя таким образом положительные целые числа.

Топо сути, то, что произошло бы в вашем примере.Поскольку Pos.apply не является безопасным типом, вы не можете получить ошибку компиляции в

myMethod(-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
}

Answer 4

Вы можете использовать черту маркера для типов примитивов следующим образом

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).

Вероятно, можно написать плагин компилятора, который "поднимает" положительные целочисленные литералы к помеченному типу.

Редактировать

Я не проверял, существуют ли какие-либо издержки времени выполнения для маркировки примитивных типов таким способом.