BOB ATKEY

Simple semantics for defaults in Catala

Catala is a programming language for the law.

As described in an ICFP 2021 paper by Merigoux et al., Catala has multiple features designed for making it easy to write code that implements legal texts.

The feature I want to talk about here is Catala's support for default reasoning.

Default reasoning involves rules like “X is the case, except when Y, Z, ...”. Apparently, such patterns are common in the law.

The ICFP paper points out that default reasoning is analogous to exceptions in normal programming languages. The paper describes how to translate default reasoning into exceptions.

I think that a good way to see how it works is in terms of a simple “exceptions monad”.

Default Calculus

The authors define the “default calculus”, which is the λ-calculus extended with constants for undefinedness and conflict and a default operator.

The default operator looks like this:

〈e1, ..., en | j :- c〉

where the intended meaning is “if j is true then evaluate to c and if j is undefined or false then evaluate to undefined, unless any of e1 to en are defined, in which case if exactly one ei is defined then evaluate to ei, if more than one is defined then evaluate to conflict”.

The Catala ICFP paper defines an operational semantics for the default operator. The authors give a translation into a λ-calculus with exceptions. They have proved the translation correct using F star.

Catala values

I think a more perspicious way of looking at how the default operator works is to think of it in terms of a simple monad.

I'll use OCaml syntax.

A “Catala value” is either Conflict, Undefined or an actual Value:

type 'a catala =
  | Conflict
  | Undefined
  | Value of 'a

This definition is basically the Maybe/option/exceptions monad with two exception values.

There is an “information” ordering on Catala values, with Undefined at the bottom, Conflict at the top, and the Values in between.

I'll not use the monad structure much, but we can decompose Catala's default operator into three simpler operators on Catala values.

The first is a conflict-adverse combination operator, which can be used to combine two Catala values into one:

let (<+>) x y = match x, y with
  | Undefined, x | x, Undefined -> x
  | Conflict, _ | _, Conflict -> Conflict
  | Value _, Value _ -> Conflict

Undefined always loses, Conflict always wins, and two attempts at a value (even if they are equal) results in conflict.

This is a commutative monoid with Undefined as the unit, and it is monotone in both arguments.

It'll be useful to be able to combine a list of Catala values using <+>:

let combine_list xs =
  List.fold_left (<+>) Undefined xs

The guard operator is a sort of gate that evaluates to its second argument if the first is true, and undefined otherwise (unless there was a conflict).

let guard x y = match x with
  | Conflict -> Conflict
  | Value true -> y
  | Value false
  | Undefined -> Undefined

This is also monotone in both arguments.

Finally, the unless operator acts like a backwards try-catch. unless x y defaults to x unless y is defined or is in conflict. Operationally, it tries y first, and if it throws the Undefined exception x is used instead.

let unless x y = match y with
  | Conflict -> Conflict
  | Undefined -> x
  | Value y -> Value y

This is not monotone in its second argument.

With these operators, we can recover Catala's default operator. It defaults to a guarded value, unless an exception is defined. In the event of multiple potential definitions, conflict is signaled.

let default value ~justification ~exceptions =
  unless (guard justification value) (combine_list exceptions)

I think this gives a simpler account of Catala's default operator than the ICFP paper.

We can see that the non-monotone behaviour of the default operator arises from the unless operator, which you might expect from a try-catch like operator that rescues definition from undefinedness.

The unless operator is a kind of “try this if that didn't work” operator, like exception handling and ordered choice in PEGs. I reckon that a semantics of data types with negation would be helpful in understanding such operators by recording “that didn't work” as a negation.

Some questions.