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

Language Design
1

There’s so much I’m liking about Scala 3 (the Optional Braces feature most of all, to my surprise) but I’m a little concerned that one “unofficial” feature of Scala 2 - Tagged Types - is missing, that is more important than it superficially appears.

There are a few versions of Tagged Types around but I’ve tended to use the Shapeless one.

What tagged types provide in Scala2 is “Poor Man’s Refinement Types” without introducing boxing for primitives (fwiw “Poor Man” here riffs on this landmark talk early in Scala’s history).

There’s also the excellent Refined library but IIUC that does induce boxing which is problematic in performance-sensitive or numerical code.

Refinement types are super useful to follow the statically-typed discipline to its logical conclusion, because they let you attach additional info about a value to its type, without changing its runtime representation.

The everyday use case is just qualifying the range of an Int. Just because the JVM offers signed 32bit slots at machine layer, doesn’t mean every integer in our systems is sensibly defined as +/-2billion. It’s crucial for correct software to be able to declare, in types, that a value should be positive, or non-zero, or within some arbitrary range.

Some officially blessed means of expressing refined types in Scala3 is needed, without having to worry about impacts on performance or memory consumption.

Dedicated language-level support would of course be welcome, but alternatively, a tag-based mechanism could be made to serve. My understanding is that Scala2-style type tags don’t work in Scala 3.

2 
opaque type PositiveInt <: Int = Int
def PositiveInt(x: Int): Option[PositiveInt] =
  if x > 0 then Some(x) else None

cf http://dotty.epfl.ch/docs/reference/other-new-features/opaques.html#bounds-for-opaque-type-aliases

1 Like
4

Hey, that PositiveInt <: Int is a neat trick I didn’t know about.

The next question I had was, can I extend this to include trait abstractions in the bound, so as to generalize across different tagged types? it seems the answer’s Yes:

trait Positive
opaque type PositiveInt <: Int & Positive = Int & Positive
def PositiveInt(x: Int): Option[PositiveInt] =
  if x > 0 then Some(x.asInstanceOf[Int & Positive]) else None
val p: Positive = PositiveInt(4).get

But I’m not yet confident that Opaque types will prove suitable as general-purpose refinements.

That’s because the intent of the feature seems different: opaque types forget their original type (unless as here we remind them with bound <: Int), whereas tagged-subtypes need not forget, they just need to attach additional type info that is erased at runtime. So I’m pessimistically waiting for the abstraction to leak…

A catch I can think of right away is the prohibition on combining inline with opaque types. People are bumping their head on that one already. Martin has stated that this constraint is fundamental to how opaque types forget their old selves, and is unlikely to be possible to “fix”.

Tagged subtypes, that have their original type plus some refinements, might not suffer this constraint…

5

Actually, are intersection types sufficient for tagged-subtypes? In this example a value typed Positive & Int gets stored in a JVM Int array ([I shows this).

trait Positive
object Test extends App:
  println(Array(1.asInstanceOf[Positive & Int]).getClass)  //class [I
6

Opaque types provide other options too. Typesafe, no casting:

object tags {
  opaque type Tagged[+V, +Tag] = Any
  type @@[+V, +Tag] = V & Tagged[V, Tag]

  def tag[Tag]: [V] => V => V @@ Tag = 
    [V] => (v: V) => v
}

import tags._
trait Positive
val a: Int @@ Positive = tag[Positive](42)

A simpler, more ad-hoc version would be to make your tags opaque types.

opaque type Positive = Any
def tag(i: Int): Int & Positive = i

Again no casting.

3 Likes
7

Please don’t do this, there is no guarantee that A & B will always erase to A it might also erase to B and then this will fail at runtime, do something like what @Jasper-M suggested instead.

8

Without the possibility of combining inline and opaque types, the best course of action is through the compiletime-ops mechanism:

All we need is an Error type

9

Jasper, looks promising, thanks for sharing!

I guess it’s too early to know what interaction tagging would have with boxing in Scala3, given that the approach for Specialization (ie unboxed execution pathways for computations over primitives) is still being worked out… Then the JVM Valhalla project, “user-defined primitives”, which is on the radar but distant, will also cause a lot of ripples in this space.

10

Soronpo, could you elaborate on what you mean by “best course of action” above? ie what use cases you’re thinking of?

11

This is the example from the PR:

import scala.compiletime.ops.string.{+, Error}
import scala.compiletime.ops.int.{>=, ToString}

object Test {
  opaque type Positive = Int
  object Positive {
    def apply[T <: Int](value: T)(given RequirePositive[T]): Positive = value

    type RequirePositive[T <: Int] <: Any = (T >= 0) match {
      case true => Any
      case false => Error["The provided value (" + ToString[T] + ") isn't positive"]
    }
  }

  val compiles: Positive = Positive[1](1)
  val doesNotCompile: Positive = Positive[-1](-1) 
                                   // error: ^ The provided value (-1) isn't positive
}

You mentioned the boxing problem of Refined. In the example above there is no boxing and you get compile-time refinement.

2 Likes
12

It seems tagging interacts nicely with Dotty Numeric Literals. In the example below, we declare purchase to take a PosInt parameter, a tagged subtype of Int.

The FromDigits implicit is used to parse the literal, offering another potential opportunity for compile-time validation of refined numeric literals.

Given that PosInt <: Int, I was doubtful if FromDigits would be used going by the currently published rules. If this is a bug, I’m hoping maintainers don’t notice it. Shhh! :stuck_out_tongue_closed_eyes:

object tags {
  opaque type Tagged[+V, +Tag] = Any
  type @@[+V, +Tag] = V & Tagged[V, Tag]

  def tag[Tag]: [V] => V => V @@ Tag = 
    [V] => (v: V) => v
}

import tags._
trait Positive
type PosInt = Int @@ Positive

def purchase(amount: PosInt) = ???
val result = purchase(-4)

given scala.util.FromDigits[Int @@ Positive]:
  def fromDigits(digits: String): PosInt = 
    val n = scala.util.FromDigits.intFromDigits(digits)
    if n >= 0 then tag[Positive](n)
    else throw new RuntimeException(s"negative: $digits")
1 Like
13

That’s cool, although I think it’s recommended to use a subclass of FromDigitsException, as given here, or a compile-time error using a macro.

14

Nowadays, you can create an elegant PositiveInt that won’t compile for negative values thanks to inline.

object PositiveIntType:

  opaque type PositiveInt = Int

  object PositiveInt:
    inline def apply(n: Int): PositiveInt =
      inline if n > 0 then n // Won't compile for 0 and for negative Ints
      else throw new IllegalArgumentException(s"Impossible to build PositiveInt($n): $n is not strictly positive.")

  extension (n: PositiveInt)
    def asInt: Int = n

Bonus: IDE like IntelliJ will let you know there is a mistake if you try to do something like:

PositiveInt(-1)
1 Like
15

But note that his approach does not work at runtime:

val runtimeValue: Int = 5
val pos = PositiveInt(runtimeValue)

Cannot reduce `inline if` because its condition is not a constant value: Playground.PositiveIntType.runtimeValue.>(0)

Also it actually compiles for negative ints:

PositiveInt(-4) //Compiles and will only fail at runtime

You should use scala.compiletime.error instead of your IllegalArgumentException:

import scala.compiletime.error

object PositiveIntType:

  opaque type PositiveInt = Int

  object PositiveInt:
    inline def apply(n: Int): PositiveInt =
      inline if n > 0 then n // Won't compile for 0 and for negative Ints
      else error("Should be positive.")

  extension (n: PositiveInt)
    def asInt: Int = n

import PositiveIntType.*

PositiveInt(-5) //Compile-time error: Should be positive

And another potential enhancement: you can make your opaque type a subtype of your underlying type. For instance:

opaque type PositiveInt <: Int = Int

//...

val x = PositiveInt(4)
val y: Int = x //Compiles
5 Likes
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