Catala

Introduction

Catala is a programming language adapted for socio-fiscal legislative literate programming. By annotating each line of the legislative text with its meaning in terms of code, one can derive an implementation of complex socio-fiscal mechanisms that enjoys a high level of assurance regarding the code-law faithfulness.

Concretely, you have to first gather all the laws, executive orders, previous cases, etc. that contain information about the socio-fiscal mechanism that you want to implement. Then, you can proceed to annotate the text article by article, in your favorite text editor :

Once your code is complete and tested, you can use the Catala compiler to produce a lawyer-readable PDF version of your implementation. The Catala language has been specially designed in collaboration with law professionals to ensure that the code can be reviewed and certified correct by the domain experts, which are in this case lawyers and not programmers.

The Catala language is special because its logical structure mimics the logical structure of the law. Indeed, the core concept of "definition-under-conditions" that builds on default logic has been formalized by Professor Sarah Lawsky in her article A Logic for Statutes. The Catala language is the only programming language to our knowledge that embeds default logic as a first-class feature, which is why it is the only language perfectly adapted to literate legislative programming.

The language is named after Pierre Catala, a professor of law who pionneered the French legaltech by creating a computer database of law cases, Juris-Data. The research group that he led in the late 1960s, the Centre d’études et de traitement de l’information juridique (CETIJ), has also influenced the creation by state conselor Lucien Mehl of the Centre de recherches et développement en informatique juridique (CENIJ), which eventually transformed into the entity managing the LegiFrance website, acting as the public service of legislative documentation.

Installation

Docker

Basic installation of the compialer vie Dockerfile provided in the 'catala' repository. Uses the examples from 'catala-examples' as a mounted volume.

bash git clone https://github.com/CatalaLang/catala.git && cd catala mkdir examples && cd exmplaes && git clone https://github.com/CatalaLang/catala-examples.git cd .. docker build . -t catala docker run -it --name catala -v $(pwd)/playground:/home/ocaml/catala/playground catala

The generated binaries will be in ~/catala/_build/install/default. Get started by running:

bash ./_build/install/default/bin/catala --help

Some features of the Catala repository also require the following executables to be present. On debian, arch or apline-based distributions, the above command should already take care of them.

groff python3 pip rsync colordiff nodejs npm

Warning: the make dependencies command does not include the z3 dependency required to enable the proof platform feature of Catala. If you wish to enable support for the Proof command of the Catala compiler, you should instead execute make dependencies-with-z3 prior to building the compiler.

The Python dependencies are installed inside a local virtual environment (venv). To use it, for example to run Python code generated by Catala, you should run the following command once in every new shell session:

. _python_venv/bin/activate

The Makefile contains useful information about the intended use and dependencies used.

Local opam installation

You can skip this step if you used the Docker option above, it is already taken care of.

Catala is available as an opam package! If opam is installed on your machine, simply execute:

opam install catala

However, if you wish to get the latest developments of the compiler, you probably want to compile it from the sources of this repository:

opam install ./

To uninstall, use

opam remove ./

If you are using opam on bare-metal, first install all the packages Catala depends on with:

make dependencies

This should ensure everything is set up for developing on the Catala compiler!

The project is distributed as a Dune artifact. Use standard dune commands to build and install the library. Makefile aliases are here to help you: running

make build

builds the compiler from its OCaml sources.

Development cycle

Syntax

1. Look into the directory 'playground/src'.
2. In there, create a master source file 'FILE1.catala_en' (depending on your language) that will be the root of your Catala program.
3. (optional) We can split up your example into multiple files. 'FILE1.catala_en' must only contain a list of modules:

```ocaml

Master file

Include: FILE2.catala_en ```

Inside each file we can write legislative texts we want to use as a reference (Markdown style, e.g. # headings) as well as code blocks (catala ) or Catala metadata (catala-metadata; While all the code sections are equivalent in terms of execution, you can mark some as "metadata" so that they are printed differently on lawyer-facing documents) and modules ('> Module X'), imports ('>Using X as Y`) and external files ('>Include: foo.vatala_en')

```catala

In code sections, comments start with

scope Foo: ```

```catala-metadata declaration structure FooBar: data foo content boolean data bar content money

```

You can also live-test the programs you wrote by feeding them to the interpreter; this will also type-check the programs, which is useful for debugging them.

Syntax

Examples: - Tutorial - US Tax Code

Compiler

The installed catala executable inside this Docker container is a binary. Get started by running '--help' (Quit the manpage by typing 'q'.)

bash ./_build/install/default/bin/catala --help

The Catala Compiler manpage contains all available commands and options. The basic command structure is:

bash catala [COMMAND] <FILE.catala_en> [OPTION]…

Our 'entrypoint' for the executable is (replace 'catala' with our custom entrypoint):

bash ./_build/install/default/bin/catala

Usage

If you want to deploy a Catala program inside an application written in programming language X. The Catala compiler will translate the source Catala program into X, yielding a new .x source code file. This .x file will export functions corresponding to the scopes of the original Catala program. You can then reuse those exported functions in your application written in X.

The catala compiler[1] is structured around many intermediate representations connected by successive translations: 1. The surface representation: from source code to abstract syntax tree (lexing [sedlex]; parsing [menhir], with custom error messages). This representation can also be weaved into literate programming outputs using the literate programming modules: - HTML: The 'Literate.Html' module weaves the source code and the legislative text together into a document that law professionals can understand. - LaTex: The 'Literate.Latex' module weaves the source code and the legislative text together into a document that law professionals can understand. 2. The desugared representation: from abstract syntax tree to desugared representation. The legislative text has been discarded and all the definitions of each variables have been collected in the same place. 3. The scope language (Scopelang): Produces an ordered list of the scope definitions compatible with the computation order. All the graph computations are done using the Ocamlgraph library. It also checks that within a scope, there is no computational circular dependency between the variables of the scope. 4. The default calculus (Dcalc): Where they typing is performed (deduce the types of variables, expressions and functions from programs written in an entirely untyped style) - Scopes have been lowered into regular functions, and enums and structs have been lowered to sum and product types. - Interpreter 5. The lambda calculus (Lcalc) - OCaml: Lcalc.Toocaml Formats a lambda calculus program into a valid OCaml program 6. The statement calculus (Scalc) - Python: The 'Scalc.Topython' module formats a lambda calculus program into a valid Python program

The Catala runtimes documentation is available here: - Runtimeocaml.Runtime: The OCaml runtime. - Runtimejsoo.Runtime: A jsofocaml wrapper around the Runtimeocaml.Runtime. This plugin generates a jsofocaml wrapper from the lcalc representation of a Catala program. First it generates the OCaml module, then an 'apiweb.ml' module which contains all the class types and conversion functions between the OCaml types and their corresponding JS objects. At the end the module exposes all methods in a JS lib <modulename> Lib.

Other plugins: - JSON schema generator: This plugin generates a JSON schema corresponding to a scope of a Catala program.

Documentation

[1] A compiler is a program whose sole job is to translate from one language into another. The target language does not have to be an executable language.

Example commands

Runs the interpreter on the Catala program, executing the scope specified by the -s option:

bash catala Interpret -s TwoBracketsTaxComputation examples/test/test.catala_en

Generates an OCaml translation of the Catala program., specifying the output drectory:

bash catala Ocaml -o examples/target/test_ocaml.ml examples/test/test.catala_en

Catala plugin for generating web APIs. It generates OCaml code before the associated [jsofocaml] wrapper:

bash catala api_web [OPTION]… FILE

Example projects

This repository presents a working example of how Catala could be distributed and deployed inside existing applications: French Law Libraries

Prebuilt artefacts are available here: - OCaml - npm: Example usage 1. 'npm install french-lawnpm.tar.gz' will install the package and add to our 'nodemodules' directory as well as 'package.json'. 2. To run we can 'node js/examples.js'. The french-law npm package exposes: - an event manager: exposes 3 methods - a list of sub-libraries: "Allocations familiales" and "aides logement" 3. Date values are encoded to JS string according the ISO8601 format: 'YYYY-MM-DD'. - Python: 1. Python version expected to run the Python code is above 3.6. 2. For the commands noted below to run, you are expected to setup a virtual Python environment 3. Then activate the environment (needs to be done every time you open a new shell session): bash . _python_venv/bin/activate 4. The src/ folder contains the Python files generated by the Catala compiler. The Python files generated by the Catala compiler depends on the catala.runtime package, whose source code can be found in runtimes/python/catala from the root of the Catala repository. 5. To use the algorithms of this library, you can take a look at the example provided in main.py. All the algorithms are centralized with wrappers in api.py, as it is very important internally to wrap all of the input parameters using src/catala.py conversion functions.

Syntax highlighting

The Catala language also comes with syntax highlighting to ease program development. The syntax highlighting is done, among other techniques, with the Iro compiler that allows writing the syntax only once, and then export it to formats understood by various IDE.

VSCode

To get Catala syntax highlighting in VSCode, simply enter from the root of the repository, depending on the language you want to use :

make vscode_en

You can now reload VSCode and check that you have syntax highlighting on any .catala file.

Pygments

Pygments is a Python-based versatile lexer for various programming languages. To use a version of Pygments augmented with the Catala plugin, simply enter from the root of the repository

make pygments

This will setup a Python virtual environment ("venv"), and install the syntax highlighting plugins that allow Pygments to handle Catala files. Those are defined in syntax_highlighting/XX/pygments/.

Pygments is used for instance by the minted LaTeX package. To make sure it is available, you need to "activate" the python venv each time using:

. _python_venv/bin/activate

Miscellaneous

Clerk

Use clerk --help if you have installed it to get more information about the command line options available. To get the development version of the help, run make help_clerk after make build. The clerk binary corresponds to the Catala build system, responsible for testing among other things.

To get more information about Clerk, see the dedicated readme

Catleg

Catleg is a command line utility providing useful integration with LégiFrance, the official repository of French legal documentation. See the decidated repository for more information.