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

Language Design
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