Exceptions - lrytz/efftp GitHub Wiki

The exceptions effect domain is enabled using the compiler option -P:effects:domains:exceptions.

Exceptions checking works like checked exceptions in Java. The main difference is that Scala supports lightweight syntax for effect-polymorphism using relative effect annotations.

Note: the current implementation does not distinguish between checked and unchecked exceptions, see see #12.

Effects are annotated using the @throws annotation

• Purity is annotated as @throws[Nothing] (or @pure, but this annotation ranges across all effect domains)
• If a method can throw multiple kinds of exceptions it can be either annotated with @throws[E1 | E2], or with @throws[E1] @throws[E2]

def g(x): Unit @throws[E1] = { ... }
def f(x: Int): Unit @throws[E1 | E2] = {
  if (x < 0) throw new E2
  else g()
}

Catching Exceptions

The compiler plugin will compute which effects are masked by try-catch clauses:

def h(x: Int): Unit @throws[E1] = try {
  f(x)
} catch {
  case e: E2 => ()
}

However, unlike in Java, the catch clause in Scala supports not only type tests, but arbitrary patterns. In case the plugin cannot determine if an exception will be caught or not it will do a conservative approximation:

catch {
  case e: E2 if condition(e) =>
}

In this example, the exception E2 will not be masked - it might be caught or not, depending on the evaluation of condition(e).

Limitations of effect inference can be overcome using effect casts.