Poor (or Rich) Man's Refinement Types in Scala 3.x?

Language Design
17

Yes exactly!
Actually I noticed the problem and already fixed my code, but it was too late to update my post.

[Edited]

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)

Btw, I integrated your idea of subtyping the underlying type.
This is nice !

I also added extension to be able to deal with variables when tou can provide a default value.
As a result now you can do:

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.
1 Like