Exceptions

Exceptions are objects that represent the occurrence of an error or unexpected behavior. They interrupt the normal flow of the program and need to be handled properly so that the program doesn't crash.

Declaring exception type

extend with #exception-type-declaration;

To use exceptions, you first need to define what kind of exceptions your program might throw so that exception handling can also be type safe. All exceptions thrown in your program have to be (a subtype) of this declared type. This declaration looks like so:

exception type = <| error_code : Nat, good : Bool |>

where you can use any type on the right side of = (not just variants). There can only be one such declaration in the code.

To mimic the Linux style of error signaling, you could simply use:

exception type = Nat

Open variant exceptions

extend with #open-variant-exceptions;

Open variant exceptions allow you to declare variants of exceptions that can be thrown in your code. Each declaration is on a separate line and adds to the global exception variant type.

In other words, this:

exception variant error_code : Nat
exception variant good : Bool

is functionally equivalent to this:

exception type = <| error_code : Nat, good : Bool |>

The difference is that exception variants can appear before and after other declarations (they don't have to be grouped together), and a throw can only recognize the exception variants declared before it.

This means that the following code typechecks:

language core;

extend with #exceptions, #open-variant-exceptions;

exception variant error_code : Nat

fn main(n : Nat) -> Bool {
    return throw(<| error_code = 1 |>)
}

while this doesn't:

language core;

extend with #exceptions, #open-variant-exceptions;

exception variant error_code : Nat

fn main(n : Nat) -> Bool {
    return throw(<| good = true |>)
}

exception variant good : Bool

The exception type declaration and open variant exception extensions are mutually exlusive, you cannot enable them both simultaneously.

Throwing exceptions

extend with #exceptions;

To throw exceptions, just use the throw function with an expression that satisfies the declared type.

Handling exceptions

Try-catch

To capture thrown exceptions, wrap the failure-prone expression in a try-catch block, which looks like:

try { might_fail() } catch { pattern => fallback_value }

The pattern must match the thrown exception value or the exception will be rethrown. If it matches, the specified expression is returned instead.

For example:

language core;

extend with #exceptions, #exception-type-declaration;

exception type = Nat

fn fail(n : Nat) -> Bool {
  return throw(succ(0))
}

fn main(n : Nat) -> Bool {
  return try {
    fail(n)
  } catch {
    0 => true
  }
}

Try-with

Another expression that is used to capture exceptions is the try-with block:

try { might_fail() } with { fallback_value }

It works similarly to the try-catch except that it captures any exception without the need to specify a pattern to match.

language core;

extend with #exceptions, #exception-type-declaration;

exception type = Nat

fn fail(n : Nat) -> Bool {
  return throw(succ(0))
}

fn main(n : Nat) -> Bool {
  return try { fail(n) } with { false }
}

Panic

A panic is an unrecoverable error that cannot be caught with try-catch or try-with. To induce anxiety and a panic attack in your program, use the special panic! expression:

language core;

extend with #comparison-operators, #panic;

fn div(n : Nat) -> fn(Nat) -> Nat {
  return fn(m : Nat) {
    return if m == 0 then panic! else panic! // division is not implemented yet 😁
  };
}

fn main(n : Nat) -> Nat {
  return div(n)(0);
}