whoami

PhD student at EPFL, co-advised by:

• Martin Odersky (LAMP/Scala)
• Viktor Kunčak (LARA/Stainless)

What is this about?

A prototype implementation of refinement types for Scala.

type Pos = {x: Int with x > 0}

Syntax

Long form, with an explicit binder:

type NonEmpty[A] = {l: List[A] with l.nonEmpty}

val x: (Int with x % 2 == 0) = 42
// desugars to:
val x: {v: Int with v % 2 == 0} = 42

Example 1: Sized lists

def zip[A, B](
  xs: List[A],
  ys: List[B] with ys.size == xs.size
): {zs: List[(A, B)] with zs.size == xs.size}

def concat[T](
  xs: List[T],
  ys: List[T]
): {zs: List[T] with zs.size == xs.size + ys.size}

val xs: List[Int] = ???
val ys: List[Int] = ???
zip(concat(xs, ys), concat(ys, xs)) // ✅
zip(concat(xs, ys), concat(xs, xs)) // ⛔️ found size xs.size + xs.size,
                                    //    required xs.size + ys.size

OOPSLA 2026 paper

Refinement vs. Assertions

def zip[A, B](
  xs: List[A],
  ys: List[B]
) : List[(A, B)] = {
  require(xs.size == ys.size)
  ???
}.ensuring(_.size == xs.size)

Example 2: Fansi

From Li Haoyi’s Fansi library for colored terminal strings:

def True(r: Int, g: Int, b: Int) =
  True0(r, g, b, trueIndex(r, g, b))

def trueIndex(r: Int, g: Int, b: Int) =
  require(0 <= r && r < 256)
  require(0 <= g && g < 256)
  require(0 <= b && b < 256)
  r << 16 | g << 8 | b

True(256, 0, 0) // 💥 at run time

type Comp = {v: Int with 0 <= v && v < 256}

def True(r: Comp, g: Comp, b: Comp) =
  True0(r, g, b, trueIndex(r, g, b))

def trueIndex(r: Comp, g: Comp, b: Comp) =
  r << 16 | g << 8 | b




True(256, 0, 0) // ⛔️ at compile time

Example 3: Overload resolution

@targetName("minSorted")
def min(l: List[Int] with l.isSorted) =
  l.head // O(1)

def min(l: List[Int]) =
  l.min // O(n)

def ex1(l: List[Int] with l.isSorted) =
  min(l) // calls the first overload

Refinement types vs. libraries

With Iron, example 3 also works, but predicates are type-level constraints:

final class IsSorted
given Constraint[List[Int], IsSorted] with
  override inline def test(inline l: List[Int]): Boolean = l.isSorted
  override inline def message: String = "List must be sorted"

def min(l: List[Int] :| IsSorted): Int = l.head

What we want

Strong specifications for agents

Strong specifications for agents

What are valid predicates?

var x = 3
val y: (Int with y == x) = x // ⛔️ x is mutable

class Box(val value: Int)
val b: Box with b == Box(3) = Box(3) // ⛔️ Box has equality by reference

Purity of predicates

By default, functions called in predicates are assumed to be pure:

class Cell { var field: Int = 0 }
def test(c: Cell) =
  def getAndBump(): Int = { c.field += 1; c.field }
  val v: Int with v == getAndBump() = getAndBump() // ✅ accepted

import language.experimental.{captureChecking, separationChecking}
class Cell extends caps.Stateful { var field: Int = 0 }
def test(c: Cell^) =
  def getAndBump(): Int = { c.field += 1; c.field }
  val v: Int with v == getAndBump() = getAndBump() // ⛔️ not pure: uses {c}

When are refinements inferred?

val x = 42
// x: Int, not {v: Int with v == 42}

val x: (Int with x == 42) = 42

Flow-sensitive typing

The condition of an if is assumed in its branches:

def pos(x: Int): {v: Int with v > 0} =
  if x > 0 then x else 1

def merge[T: Ordering as ord](left: SafeSeq[T], right: SafeSeq[T]): SafeSeq[T] =
  if left.len > 0 && right.len > 0 then
    if ord.lt(left.head, right.head) then SafeSeq(left.head) ++ merge(left.tail, right)
    else SafeSeq(right.head) ++ merge(left, right.tail)
  else if left.len == 0 then right
  else left

Solver

{v: Int with v == a && a == b}
  <: {v: Int with v == b}
{v: Int with a == b}
  <: {v: Int with f(a) == f(b)}

{v: Int with v == x + 3 * y}
  <: {v: Int with v == 2 * y + (x + y)}

Run-time checks

Pattern matching branches on whether the predicate holds at run time:

val idRegex = "[0-9a-f]{4}-[0-9a-f]{4}"
type ID = {s: String with s.matches(idRegex)}

"a2e7-e89b" match
  case id: ID => ... // holds, id has type ID
  case _      => ... // does not hold

Run-time checks: .runtimeChecked

You can also use .runtimeChecked (SIP-57) when you expect the check to always pass:

val id: ID = "a2e7-e89b".runtimeChecked

val id: ID =
  if ("a2e7-e89b".matches(idRegex)) "a2e7-e89b".asInstanceOf[ID]
  else throw new IllegalArgumentException()

Gradual typing

By default, a refinement that cannot be verified statically is a type error:

val x: {v: Int with v == 1} = readInt() // ⛔️ type error

import language.experimental.qualifiedTypes.runtimeChecks // or warn, or silent

Verifying with Stainless

The Stainless verifier can use Dotty’s refinement types, thanks to Kasia Marek!

It compiles in silent mode, then verifies refinements itself with SMT solvers:

def sum(n: BigInt with n >= 0): {r: BigInt with 2 * r == n * (n + 1)} =
  if n == 0 then BigInt(0) else n + sum(n - 1) // ✅ verified

def abs(x: Int): {r: Int with r >= 0} =
  if x >= 0 then x else -x // ⛔️ counter-example: x = -2147483648

Example 4: Memoized Fibonacci

A map whose values are related to their keys by a predicate p:

case class DepMap[K, V](p: (K, V) => Boolean):
  def put(n: K, v: V with p(n, v)): Unit = ???
  def get(n: K): Option[{res: V with p(n, res)}] = ???

def fib(n: Int): {r: Int with r == (if n <= 1 then 1 else fib(n - 1) + fib(n - 2))} =
  if n <= 1 then 1 else fib(n - 1) + fib(n - 2)

Example 4: Memoized Fibonacci (2)

A memoized version, checked to always return fib(n):

val cache: (DepMap[Int, Int] with (cache == DepMap[Int, Int]((k, v) => v == fib(k)))) =
  DepMap[Int, Int]((k, v) => v == fib(k))

def fibMemo(n: Int): {res: Int with res == fib(n)} =
  cache.get(n) match
    case Some(res) => res
    case None =>
      val res: (Int with (res == fib(n))) =
        if n <= 1 then 1 else fibMemo(n - 1) + fibMemo(n - 2)
      cache.put(n, res)
      res

Evaluation

Compilation overhead, against each system’s own unchecked baseline:

Future work

• Pre-SIP and SIP to make refinement types part of Scala.

• Better solver for what our lightweight solver cannot do.

• A termination checker (Master semester project from Ozair Faizan to be included).

• Term-parameterized types, to modularize predicates:

    type Range(from: Int, to: Int) =
      {v: Int with v >= from && v < to}

How to use

Try it online in the playground, and report issues at github.com/epfl-lara/dotty.

//> using scalaOrganization ch.epfl.lara
//> using scala 3.10.1-RC1-bin-20260903-e1f9361-NIGHTLY
//> using options -language:experimental.qualifiedTypes

scalaOrganization := "ch.epfl.lara"
scalaVersion := "3.10.1-RC1-bin-20260903-e1f9361-NIGHTLY"
scalacOptions += "-language:experimental.qualifiedTypes"

Thank you!

Examples available at github.com/mbovel/scala-days-refinement-types.