Syntax and Runtime Checks for Qualified Types in Scala 3

Quentin Bernet @LARA, EPFL

Oktober 2, 2023

Slides

These slides can be found at go.epfl.ch/QT-slides.

Their source code: Sporarum/slides-master-project on github.



Implementation PRs: go.epfl.ch/QT-code

Introduction

Our mascot:

Le type qualifié,

The qualified guy

What are qualified types ?

More precise types, inspired by sets builders: \{x \in \mathbb{Z}\;|\;x > 0\}

type Pos = Int with _ > 0
4: Pos
type NonEmptyString = String with s => !s.isEmpty
"Nilla Wafer Top Hat Time": NonEmptyString
type PoliteString = NonEmptyString with s =>
    s.head.isUpper &&
    s.takeRight(6) == "please"
"Pass me the butter, please": PoliteString

:::

Why not contracts ?

def divideQualified(x: Int, y: Int with y != 0):
  Int with _ * y == x
def divideContract(x: Int, y: Int): Int = {
  require(y != 0)
  ???
}.ensuring(_ * y == x)

Signature and code are mixed

def divideQualified(x: Int, y: Int with y != 0):
  Int with _ * y == x
def divideContract(x: Int, y: Int): Int = {
  require(y != 0)
  ???
}.ensuring(_ * y == x)

Re-use predicates

type NonZero = Int with _ != 0
def divideQualified(x: Int, y: NonZero):
  Int with _ * y == x
def nonZero(y: Int) = y != 0
def divideContract(x: Int, y: Int): Int = {
  require(nonZero(y))
  ???
}.ensuring(_ * y == x)

Predicate polymorphism

def smallest[T](l: List[T]): T

def smallestPos(l: List[Pos]) = smallest(l)
def smallestPosContract(l: List[Int]): Int = {
  require(l.forall(_ > 0))
  ???
}.ensuring(_ > 0)

In Brief

Looks like:

type Pos = Int with _ > 0

Behaves like contracts

Powerful thanks to polymorphism

The compiler

Main phases:

  • Parser
  • Typer
  • Pattern Matcher
  • Qualifier Checker
  • Erasure
  • Bytecode generator

Our work

Trying to make qualified types approachable:

  • Finding a friendly syntax
    • 2 implemented syntaxes
    • 1 proposed syntax
  • Runtime checks & Pattern matching
    • isInstanceOf, asInstanceOf
    • comparison with pattern guards

Even without a solver, that’s already enough for some applications !

Syntax

type NonEmptyString = String with s => !s.isEmpty

Elements:

  • Base type (String)
  • Identifier (s)
  • Qualifier (!s.isEmpty)

Internal representation:

String @qualified[String]((s: String) => !s.isEmpty)

Consensus

Naming is hard => Don’t do it if you don’t have to

Boolean expressions:

type Trivial = Int with true
type Empty   = Int with false

Available identifiers:

def foo(x: Int with x > 0, y: Int with y > x): Int = y - x

Postfix Lambda

import scala.language.experimental.postfixLambda

type Pos = Int with x => x > 0
// or
type Pos = Int with _ > 0

type Digit = Int with x => 0 <= x && x < 10
type IncreasingPair = (Int, Int) with _ < _
// desugared
type IncreasingPair = (Int, Int) with (x, y) => x < y
// untupled to
type IncreasingPair = (Int, Int) with p => p._1 < p._2

Postfix Lambda Problems

(Int with x => x > 0) => (Int with y => y < 0) => Int
val f = x => x > 0

type Valid = Int with x => x > 0
type Invalid = Int with f
// desugars to
type Invalid = Int with x => f

Set Notation

Inspired by math \{x \in \mathbb{Z}\;|\;x > 0\}
And other programming languages {v:Int | v > 0}

import scala.language.experimental.setNotation

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

type Digit = {x: Int with 0 <= x && x < 10}

Set Notation Situations

(x: Int) => x.type
(x: Int with x > 0) => x.type
{x: Int with x > 0} => x.type

Syntax Proposal

it

Simple idea: a more legible _ that you can repeat

type Pos = Int with it > 0

type Digit = Int with 0 <= it && it < 10
(Int with it > 0) => (Int with it < 0) => Int
(x: Int with x > 0) => Int with x > 0
    Int with it > 0 => Int with x > 0

it may be nested

type Outer = Int with
  type Smaller = Int with it < it?

  ???

it is actually fine

type Outer = Int with
  type Smaller = Int with it < super.it

  ???

id

Different simple idea: identifiers for any type

type Function = (x: Int) => x.type
type Alias = (x: Int)
type Pos = (x: (y: Int) with y > 0)
type Pos = (x: Int with x > 0)

type Digit = (x: Int with 0 <= x && x < 10)

it & id

They are compatible, and can even be translated one into the other:

id to it:

type Pos = (x: Int with x > 0)
// transformed into
type Pos = (x: (Int with it > 0))

it to id:

type Pos = Int with it > 0
// transformed into
type Pos = (it$1: Int) with it$1 > 0

Runtime Checks

Type test:

x.isInstanceOf[T] // Boolean


Cast:

x.asInstanceOf[T] // T

Type test on qualified type

x.isInstanceOf[Int with _ > 0]
// after erasure
x.isInstanceOf[Int] && x > 0

… won’t work:

{println("❤️");}.isInstanceOf[Int with _ > 0]
// after erasure
{println("❤️");}.isInstanceOf[Int] && ({println("❤️");} > 0)

Type test on qualified type for real

{println("❤️");}.isInstanceOf[Int with _ > 0]
// after erasure
val fresh1 = {println("❤️");}
fresh1.isInstanceOf[Int] && {
  val fresh2 = fresh1.asInstanceOf[Int]
  fresh2 > 0
}

Implementation

def transformTypeTest(expr: Tree, testType: Type, ...): Tree =
  testType.dealiasKeepQualifyingAnnots match {
    ...
    case refine.EventuallyQualifiedType(baseType,
                             closureDef(qualifier: DefDef)) =>
      evalOnce(expr) { e =>
        transformTypeTest(e, baseType, flagUnrelated).and(
          BetaReduce(qualifier, List(List(e.asInstance(baseType)))))
      }
    ...

Pattern Matching

Is just syntactic sugar

costlyCall() match
  case i: Int if i > 0 =>
    i + 1
val x = costlyCall()
if x.isInstanceOf[Int] && {
  val i = x.asInstanceOf[Int]
  i > 0
} then
  val i = x.asInstanceOf[Int]
  i + 1
else
  throw new MatchError(x)

Implementation





This slide intentionally left blank

Pattern guards & qualified types

case y: Int if
    0 <= y && y < 10 =>
if x.isInstanceOf[Int] && {
  val y = x.asInstanceOf[Int]
  0 <= y && y < 10
} then ...
case y: Int with
    0 <= y && y < 10 =>
if x.isInstanceOf[Int with y => 
    0 <= y && y < 10]
then ...
if x.isInstanceOf[Int] && {
  val y = x.asInstanceOf[Int]
  0 <= y && y < 10
} then ...

Before

def answerRequest(x: Any): Either[String, String] =
  x match
    case s: PoliteString => Right("Of course !")
    case _               => Left("Please be polite ...")
type NonEmptyString = String with s => !s.isEmpty

type PoliteString = NonEmptyString with s => s.head.isUpper &&
                                             s.takeRight(6) == "please"

After

def answerRequest(x: Object): scala.util.Either =
  if
    x1.isInstanceOf[String] &&
    {
      val _$1: String = x1.asInstanceOf[String]
      !(_$1.isEmpty)
    } &&
    {
      val s: String = x1.asInstanceOf[String]
      s.head.isUpper &&
      s.takeRight(6) == "please"
    }
  then
    val s: String = x1.asInstanceOf[String]
    return Right("Of course !")
  
  return Left("Please be polite ...")

Ducks

If it quacks like a pattern guard, why not make it look like one:

type Pos = Int if it > 0
x match
  case (x: Int) if x > 0 =>
  case x: (Int if x > 0) =>

Flow typing for free !

Syntax + Checks =

type Nat = Int with _ >= 0

def log(x: Nat): Int = ???
def logUnsafe(x: Int) =
  log(x) // error
def logSafe(x: Int) = x match
  case x: Nat => Some(log(x))
  case _      => None

Conclusion

  • Implemented syntaxes
    • postfix lambda: Int with _ > 0
    • set notation: {x: Int with x > 0} Proposed syntax
    • it: Int with it > 0
    • id: (x: Int) with x > 0
    • And potentially if as keyword
  • Pattern matching:
    • qualified types as “compiletime pattern guards”

Future work: Solver

Extra Slides

JSON schema

Works for both syntaxes:

case class LongitudeAndLatitudeValues(
  latitude: Double with -90 <= latitude && latitude <= 90,
  longitude: Double with -180 <= longitude && longitude <= 180,
  city: String with raw"^[A-Za-z . ,'-]+$$".r.matches(city)
) extends Obj

Shape: Postfix Lambda

type Shape = List[Int with _ > 0]

extension (s: Shape)
  def nbrElems = s.fold(1)(_ * _)
  def reduce(axes: List[Int with x => s.indices.contains(x)]) = s.zipWithIndex.filter((_, i) => axes.contains(i)).map(_._1)

Tensor: Postfix Lambda

trait Tensor[T]:
  val shape: Shape
  def sameShape(t: Tensor[T]): Boolean = ???
  def add(t: Tensor[T] with t.sameShape(this)):
    Tensor[T] with _.sameShape(this)

  def mean(axes: List[Int with x => shape.indices.contains(x)]):
    Tensor[T] with _.shape == shape.reduce(axes)

  def reshape(newShape: Shape with newShape.nbrElems == shape.nbrElems):
    Tensor[T] with _.shape == newShape

Shape: Set Notation

type Shape = List[{x: Int with x > 0}]

extension (s: Shape)
  def nbrElems = s.fold(1)(_ * _)
  def reduce(axes: List[{x: Int with s.indices.contains(x)}]) = s.zipWithIndex.filter((_, i) => axes.contains(i)).map(_._1)

Tensor: Set Notation

trait Tensor[T]:
  val shape: Shape
  def sameShape(t: Tensor[T]): Boolean = ???
  def add(t: Tensor[T] with t.sameShape(this)):
    {res: Tensor[T] with res.sameShape(this)}

  def mean(axes: List[{x: Int with shape.indices.contains(x)}]):
    {res: Tensor[T] with res.shape == shape.reduce(axes)}

  def reshape(newShape: Shape with newShape.nbrElems == shape.nbrElems):
    {res: Tensor[T] with res.shape == newShape}

this doesn’t work

trait Tensor[T]:
  def add(t: Tensor[T] with t.sameShape(Tensor.this)):
    Tensor[T] with this.sameShape(Tensor.this)

Overloading Resolution

def f(x: Any) = "f1"
def f(x: Pos) = "f2"

f(-1)

During typing: Pos =:= Int, f1 gets chosen

During QualChecking: Pos < Int, and type mismatch

But f2 would have been fine !

Irrefutability

type Pos = Int with x > 0

object Extractor:
  def unapply(x: Pos): Some[Pos] = Some(x)

-1 match
  case Extractor(x) => x
  case _ => None // warning: unreachable case

it and de Bruijn indices

\lambda f.\:\lambda g.\:\lambda x.\:f (g x)

\lambda\:\lambda\:\lambda\:3\:(2\:1)

... with ...
  ... with ...
    ... with ...
      super.super.it( super.it( it ) )

But please don’t do that