Is it possible to restrict Int by creating something like PositiveInt and have compile-time checks in Scala?

Question

Is it possible to create a restricted Int such as PositiveInt and have compile-time checks for it? In other words is it possible to define a method such as:

def myMethod(x: PositiveInt) = x + 1

and then have something like:

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

If this is possible how should I start with defining PositiveInt, I mean is there a convenient technique for this in Scala?

Answer 1

This kind of thing is called dependent typing, and no, it's not available in Scala.

Answer 2

You can use a marker trait on primitve types in the following way

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]

But you will only get a runtime error for writing makePositive(-5). You will get a compile time error for writing succ(5).

It is probably possible to write a compiler plugin that "lifts" positive integer literals to a marked type.

Edit

I have not tested whether there is any runtime overhead for marking primitive types in such a way.

Answer 3

If you have compile time dependent type checking, you solved the halting problem or your compiler is not always guaranteed to finish compiling or the grammer of your programming language needs to be Turing complete all of which are ridiculous things.

Here is a reasonable alternative for dependent typing during runtime

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

There are several ways to avoid an Int to be negative, but it always comes with some drawbacks. Refined lib is very powerful but, currently, it still has some compatibility issues with Scala 3, as far as I know.

However, I'm very satisfied with Scala 3, because nowadays you can use inline keyword to prevent compilation for negative numbers like this:

opaque type PositiveInt <: Int = Int

object PositiveInt:
  inline
  def apply(inline n: Int): PositiveInt =
    inline if n == 0
    then compiletime.error("Impossible to build PositiveInt(0)")
    else if n < 0
    then compiletime.error("Impossible to build PositiveInt(-n): negative value.")
    else n: PositiveInt

  def make(n: Int): Option[PositiveInt] =
    Option.when(n > 0)(n)

  extension (nOpt: Option[PositiveInt])
    inline
    def orDefault[T <: PositiveInt](default: T): PositiveInt =
      nOpt.getOrElse(default)

  extension (inline n: Int)
    inline
    def asPositive: PositiveInt =
      PositiveInt(n)

Both good IDE (like IntelliJ) and compilator will let you know there is a mistake if you try to do something forbidden.

import PositiveInt.*

// Compiles
val a = PositiveInt(4)
val b: Int = a
val c = 99.asPositive
val d: Int = -5
val e = PositiveInt.make(d).orDefault(c) //Assigns: 99


// Won't compile
val e = PositiveInt(0) //Compile-time error: Impossible to build PositiveInt(0)
val f = -2.asPositive //Compile-time error: Impossible to build PositiveInt(-n): negative value.

Answer 5

The other answers refer mostly to the issue of creating a "positive number" type that relates to a "number" type in a way the compiler can guarantee correctness. For example with dependent types you can proof that the implementation of functions like abs are correct. You can't do that with scala.

You can, however, build a type that represents positive integers and nothing else. For example:

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

This is similar to what ziggystar proposed, with the difference that is the correctness of the type is guaranteed by its own construction, not by the constructor. That is, it is impossible to represent a negative number with this type.

This approach is likely not to be practical for your purposes. You either need to implement all the operations for it or piggyback to the Int value, which then is equivalent to just have a runtime check since you lose all type safety you won by representing positive integers in this way.

That is essentially what would happen in your example. Since Pos.apply is not type safe, you cannot get a compile error in

myMethod(-5)

Answer 6

Yes. They are called Refined types. Please check: https://github.com/fthomas/refined for more details.

No need to implement anything by yourself, no apply methods etc. Just use it.. :)