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

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.

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

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…

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

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

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.

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

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.

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

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

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

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.