OCaml Planet

The OCaml Planet aggregates various blogs from the OCaml community. If you would like to be added, read the Planet syndication HOWTO.

1206 blog posts are available. You can read the 30 more recent ones below or view older ones.

Coq 8.11+beta1 is out — Coq, Dec 06, 2019

The first beta release of Coq 8.11 is available for testing.

There are two main changes brought by Coq version 8.11. First, it introduces Ltac2, a new tactic language for writing more robust larger scale tactics, with built-in support for datatypes and the multi-goal tactic monad. Second, primitive floats are integrated in terms and follow the binary64 format of the IEEE 754 standard, as specified in the `Coq.Float.Floats` library. Many other cleanups and improvements have been performed and a…

Deep-Learning the Hardest Go Problem in the World — Jane Street, Dec 06, 2019

Updates and a New Run

Frama-C 20.0 (Calcium) is out. Download it here. — Frama-C, Dec 04, 2019

Testing OCaml releases with opamcheck — GaGallium (Florian Angeletti), Dec 03, 2019

I (Florian Angeletti) have started working at Inria Paris this August. A part of my new job is to help deal with the day-to-day care for the OCaml compiler, particularly during the release process. This blog post is a short glimpse into the life of an OCaml release.

OCaml and the opam repository

Currently, the song of the OCaml development process is a canon with two voices: a compiler release spends the first 6 months of its life as the trunk branch of the OCaml compiler git repository…

OCaml and the opam repository

Currently, the song of the OCaml development process is a canon with two voices: a compiler release spends the first 6 months of its life as the trunk branch of the OCaml compiler git repository. Then after those 6 first months, it is named and given a branch on its own. For instance, this happened on October 18 2019 for OCaml 4.10. Starting from this point, the branch is feature-frozen: only bug fixes are merged, whereas new feature development happens in trunk. Our objective is then to release the new version 3 months later. If we succeed, there are at most two branches active at the same time.

    Dev
    Dev
    Dev
    Dev
    Dev
    Dev
    Bug  Dev
    Bug  Dev
    RCs  Dev
         Dev
         Dev
         Dev
         Bug  Dev
         Bug  Dev
         RCs  Dev
              Dev
              Dev
              Dev
              Bug
              Bug
              Rcs

However, the OCaml compiler does not live in isolation. It makes little point to release a new version of OCaml which is not compatible with other parts of the OCaml ecosystem.

The release cycle of OCaml 4.08 was particularly painful from this point of view: we refactored parts of the compiler API that were not previously versioned by ocaml-migrate-parsetree, making it more difficult to update. In turn, without a working version of ocaml-migrate-parsetree, ppxses could not be built, breaking all packages that depend on them. It took months to correct the issue. This slip of schedule affected the 4.09.0 release and can still be felt on the 4.11 schedule.

Catching knifes before the fall

Lesson learned, we need to test the packages in the opam repository more often. Two tools in current usage can automate such testing: opamcheck and opam-health-check.

The two tools attack the problem with a different angle. The opam-health-check monitoring tool is developed to check the coherency of the opam repository, for released OCaml versions.

In a complementary way, opamcheck was written by Damien Doligez to check how well new versions of the OCaml compiler fare in terms of building the packages in the opam repository.

A typical difference between opamcheck and opam-health-check is that opamcheck is biased towards newer versions of the compiler: if an opam package builds on the latest unreleased version of the compiler, we don’t need to test it with older compilers. After all, we are mostly interested in packages that are broken by the new release. The handful of packages that may be coincidentally fixed by an unreleased compiler are at most a curiosity; pruning those unlikely events saves us some precious time.

Since I started at Inria, in the midst of the first beta of OCaml 4.09.0, I have been working with opamcheck to monitor the state of the opam repository.

The aim here is twofold. First, we want to detect expected breakages that are just a sign that a package needs to be updated before the final release of the new compiler version. The earliest we catch those, the more time the maintainers have to patch their packages. Second, we want to detect unexpected compatibility issues and breakages.

One fun example of such unexpected compatibility issue appeared in the 4.09.0 release cycle. When I first used opamcheck to test the state of the first 4.09.0 beta, there was a quite problematic broken package: dune. This was quite stunning at first, because the 4.09.0 version of OCaml contained mostly bug fixes and small quality-of-life improvements. That was at least what I had told a few worried people a few days earlier…

So what was happening here? The issue stemmed from a small change of behaviour in presence of missing compiled interface (cmi) files : dune was relying on an unspecified OCaml compiler behaviour in such cases, and this behaviour had been altered by a mostly unrelated improvement in the typechecker.

This change of behaviour was patched and dune worked fine in the second beta release of 4.09.0. And this time, the next run of opamcheck confirmed that that 4.09.0 was a quiet release.

This is currently the main use of opamcheck: check the health status of the opam repository on unreleased version of OCaml before opam-health-check more extensive coverage takes the relay. One of our objectives for the future 4.10.0 release is to achieve a much more extensive test coverage, before the first beta.

Opam and the PRs

There is another possible use of opamcheck that is probably much more useful to the anxious OCaml developer: opamcheck can be used to check that a PR or an experimental branch does not break opam packages. A good example is #8900: this PR proposes to remove the special handling of abstract types defined inside the current module. This special case looks nice locally, but it allows to write some code which is valid if and only if it is located in the right module, without any possibility to correct this behaviour by making module signatures more precise.

It is therefore quite tempting to try to remove this special case from the typechecker, but is it reasonable?

This was another task for opamcheck. First, I added a new opamcheck option to easily check any pull request on the OCaml compiler. After some work, there was some good news: this pattern is mostly unused in the current opam repository.

Knowing whether there are any opam packages that rely on this feature is definitively a big help when taking these decisions.

Using opamcheck

So if you are a worried OCaml developer and want to test your fancy compiler PR on the anvil of the opam repositoy, what are the magical incantations?

One option is to download the docker image octachron/opamcheck with

docker pull octachron/opamcheck

Beware that the image weighs around 7 GiB. It is also possible to build and run opamcheck locally as detailed in the readme. However, in this short blog post, I will present the latter option. It has the advantages of being relatively lightweight in terms of configuration, and makes it easier to test your legions of PRs simultaneously (you don’t have legions of PRs, do you?)

Once the image is downloaded, there are three main ways to run it. If you want to compare several versions of the compiler (given as switch names), let’s say 4.05, and 4.08.1+flambda and 4.10.0+trunk, you can run:

docker run -v opamcheck:/app/log -p 8080:80 --name=opamcheck opamcheck run -online-summary=10 4.05.0 4.08.1+flambda 4.10.0

The -name option is the docker container name. The -p option maps the port 80 of the container to the port 8080 of the host, this is used to connect to the http server embedded in the image. Finally, the -v flag let us choose the location of opamcheck log directory in the host file system. (If you forget this option, a random docker volume name will be used.) Here, it will be at /var/lib/docker/volumes/opamcheck.

While opamcheck is runnning, its progress can be checked with either

sudo tail -f /var/lib/docker/volumes/opamcheck_log/_data/results

or by pointing a web browser to localhost:8080/fullindex.html. Note that the first summary is only generated after the OCaml compiler is built and all uninstallable packages have been discovered. On my machine, this rounds up at a 15 minutes wait before the first summary is generated. Later updates should be more frequent.

The result should look like this summary run for OCaml 4.10.0. The integer parameter in -online-summary=n corresponds to the update period for this html summary. If the option is not provided, the html summary is only built at the end of the run.

If you are more interested by testing a specific PR, for instance #8900, the prmode mode works better

docker run -p 80:8080 opamcheck --name=opamcheck prmode -online-summary=10 -pr 8900 4.09.0

This command tries to rebase the given PR on top of the given OCaml version (switch name); it fails immediately if the PR cannot be rebased; in this case you should use the latest trunk switch as base or use the branch option, described below. When possible, it is a good idea to use a released version as the base: with a released version, there are more unbroken packages to test your patch against.

If the branch that you want to test is not yet a PR, or needs some manual rebasing to be compared against a specific compiler version, there is a -branch flag. For instance, let’s say that you have a branch my_very_experimental_branch at the location nowhere.org. You can run

docker run -p 80:8080 opamcheck --name=opamcheck prmode -online-summary=10 -branch https://nowhere.org:my_very_experimental_branch 4.09.0

This command downloads the branch at nowhere.org and compare it against the 4.09.0 switch.

Currently, a full run of opamcheck takes one or two days: you will likely get the results before your first PR review. A limitation is the false positive rate: most opam package descriptions are incomplete or out of date, so packages will fail for reasons unrelated to your PR. Unfortunately, this means that there is still some manual triage needed after an opamcheck run.

There are four main objectives for opamcheck in the next months:

improve its usability
share more code with opam-health-check, at least on the frontend
reduce the false positive rate
reduce the time required by a CI run

If you want to check on future development for opamcheck, and a potentially more up-to-date readme, you can have a look at Octachron/opamcheck.

Hide

Coq 8.10.2 is out — Coq, Nov 29, 2019

The 8.10.2 release of Coq is available.

Main changes:

Fixed a critical bug of template polymorphism and nonlinear universes
Fixed a few anomalies
Fixed an 8.10 regression related to the printing of coercions associated to notations
Fixed uneven dimensions of CoqIDE panels when window has been resized
Fixed queries in CoqIDE

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

Announcing Irmin 2.0.0 — MirageOS (Anil Madhavapeddy), Nov 26, 2019

We are pleased to announce Irmin 2.0.0, a major release of the Git-like distributed branching and storage substrate that underpins MirageOS. We began the release process for all the components that make up Irmin back in May 2019, and there have been close to 1000 commits since Irmin 1.4.0 release back in June

To celebrate this milestone, we have a new logo and opened a dedicated website: irmin.org.

You can read more details about the new features in the Irmin v2 blog post. Enjoy the new releas…

BAP 2.0 is released — The BAP Blog, Nov 19, 2019

The Carnegie Mellon University Binary Analysis Platform (CMU BAP) is a suite of utilities and libraries that enables analysis of programs in their machine representation. BAP is written in OCaml, relies on dynamically loaded plugins for extensibility, and is widely used for security analysis, program verification, and reverse engineering.

This is a major update that includes lots of new features, libraries, and tools, as well as improvements and bug fixes to the existing code. The following sma…

This is a major update that includes lots of new features, libraries, and tools, as well as improvements and bug fixes to the existing code. The following small demo showcases the modern BAP look and feel. In this announcement we would like to focus on two very important features of BAP 2.0:

The Knowledge Base

The Knowledge Representation and Reasoning System, or the Knowledge Base (KB) for short, is the central part of our new architecture. The KB is a step forward from the conventional approach to staging multiple analyses in which dependent analyses (aka passes) are ordered topologically, based on their dependencies. The KB is inspired by logic programming and enables an optimal and seamless staging of mutually dependent analyses. Mutually dependent analyses are also present in the source-based program analysis but are much more evident in the field of binary analysis and reverse engineering, where even such basic artifacts as control flow graph and call graph are not available as ground truth (and in general are not even computable).

Object properties in the KB are represented with directed-complete partially ordered sets. The KB also imposes the monotonicity restriction that requires that all updates to the property are monotonic, i.e., each consequent value of the same property is a refinement of the previous value. These restrictions enable the KB to compute the least fixed point of any property, is computed. A property representation could be optionally refined into a complete lattice, which gives the KB users extra control on how properties are computed.

By storing all information in an external location the KB addresses the scalability issue so relevant to binary analysis and reverse engineering. In the future, we plan to implement a distributed storage for our Knowledge Base as well as experiment with other inference engines. Soon, it should also possible to work with the knowledge base in non-OCaml programs, including our BAP Lisp dialect. That, practically, turns the knowledge base into a common runtime for binary analysis. In the current version of BAP, the Knowledge Base state is fully serializable and portable between different versions of BAP, OCaml, and even between native and bytecode runtimes. The Knowledge Base state could be imported into an application and is integrated with the BAP caching system.

New Program Representation

Employing the tagless final embedding together with our new Knowledge Base we were able to achieve our main goal - to switch to an extensible program representation without compromising any existing code that uses the current, non-extensible, BAP Intermediate Language (BIL). The new representation allows us to add new language features (like floating-point operations or superscalar pipeline manipulations) without breaking (or even recompiling) the existing analyses. The new representation also facilitates creation of new intermediate languages which all can coexist with each other, making it easier to write formally verified analyses.

Links

Hide

CI/CD pipelines: Monad, Arrow or Dart? — Thomas Leonard, Nov 14, 2019

In this post I describe three approaches to building a language for writing CI/CD pipelines. My first attempt used a monad, but this prevented static analysis of the pipelines. I then tried using an arrow, but found the syntax very difficult to use. Finally, I ended up using a light-weight alternative to arrows that I will refer to here as a dart (I don’t know if this has a name already). This allows for static analysis like an arrow, but has a syntax even simpler than a monad.

Table of Con…

Table of Contents

( this post also appeared on Reddit and Lobsters )

Introduction

I was asked to build a system for creating CI/CD pipelines. The initial use for it was to build a CI for testing OCaml projects on GitHub (testing each commit against multiple versions of the OCaml compiler and on multiple operating systems). Here’s a simple pipeline that gets the Git commit at the head of a branch, builds it, and then runs the tests:

The colour-scheme here is that green boxes are completed, orange ones are in progress and grey means the step can’t be started yet.

Here’s a slightly more complex example, which also downloads a Docker base image, builds the commit in parallel using two different versions of the OCaml compiler, and then tests the resulting images. Here the red box indicates that this step failed:

A more complex example is testing the project itself and then searching for other projects that depend on it and testing those against the new version too:

Here, the circle means that we should wait for the tests to pass before checking the reverse dependencies.

We could describe these pipelines using YAML or similar, but that would be very limiting. Instead, I decided to use an Embedded Domain Specific Language, so that we can use the host language’s features for free (e.g. string manipulation, variables, functions, imports, type-checking, etc).

The most obvious approach is making each box a regular function. Then the first example above could be (here, using OCaml syntax):

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

The second could be:

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  build "4.07";
  build "4.08"

And the third might look something like this:

let example3 commit =
  let src = fetch commit in
  let image = build src in
  test image;
  let revdeps = get_revdeps src in
  List.iter example1 revdeps

However, we’d like to add some extras to the language:

Pipeline steps should run in parallel when possible. The example2 function above would do the builds one at a time.
Pipeline steps should be recalculated whenever their input changes. e.g. when a new commit is made we need to rebuild.
The user should be able to view the progress of each step.
The user should be able to trigger a rebuild for any step.
We should be able to generate the diagrams automatically from the code, so we can see what the pipeline will do before running it.
The failure of one step shouldn’t stop the whole pipeline.

The exact extras don’t matter too much to this blog post, so for simplicity I’ll focus on just running steps concurrently.

Attempt one: a monad

Without the extra features, we have functions like this:

val fetch : commit -> source
val build : source -> image

You can read this as “build is a function that takes a source value and returns a (Docker) image”.

These functions compose together easily to make a larger function that will fetch a commit and build it:

let fab c =
  let src = fetch c in
  build src

We could also shorten this to build (fetch c) or to fetch c |> build. The |> (pipe) operator in OCaml just calls the function on its right with the argument on its left.

To extend these functions to be concurrent, we can make them return promises, e.g.

val fetch : commit -> source promise
val build : source -> image promise

But now we can’t compose them easily using let (or |>), because the output type of fetch doesn’t match the input of build.

However, we can define a similar operation, let* (or >>=) that works with promises. It immediately returns a promise for the final result, and calls the body of the let* later, when the first promise is fulfilled. Then we have:

let fab c =
  let* src = fetch c in
  build src

In order words, by sprinkling a few * characters around we can turn our plain old pipeline into a new concurrent one! The rules for when you can compose promise-returning functions using let* are exactly the same as the rules about when you can compose regular functions using let, so writing programs using promises is just as easy as writing regular programs.

Just using let* doesn’t add any concurrency within our pipeline (it just allows it to execute concurrently with other code). But we can define extra functions for that, such as all to evaluate every promise in a list at once, or an and* operator to indicate that two things should run in parallel:

let example2 commit =
  (* Fetch the source code and Docker base image in parallel: *)
  let* src = fetch commit
  and* base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let* image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  (* Build and test against each compiler version in parallel: *)
  all [
    build "4.07";
    build "4.08"
  ]

As well as handling promises, we could also define a let* for functions that might return errors (the body of the let is called only if the first value is successful), or for live updates (the body is called each time the input changes), or for all of these things together. This is the basic idea of a monad.

This actually works pretty well. In 2016, I used this approach to make DataKitCI, which was used initially as the CI system for Docker-for-Mac. Later, Anil Madhavapeddy used it to create opam-repo-ci, which is the CI system for opam-repository, OCaml’s main package repository. This checks each new PR to see what packages it adds or modifies, tests each one against multiple OCaml compiler versions and Linux distributions (Debian, Ubuntu, Alpine, CentOS, Fedora and OpenSUSE), and then finds all versions of all packages depending on the changed packages and tests those too.

The main problem with using a monad is that we can’t statically analyse the pipeline. Consider the example2 function above. Until we have queried GitHub to get a commit to test, we cannot run the function and therefore have no idea what it will do. Once we have commit we can call example2 commit, but until the fetch and docker_pull operations complete we cannot evaluate the body of the let* to find out what the pipeline will do next.

In other words, we can only draw diagrams showing the bits of the pipeline that have already executed or are currently executing, and we must indicate opportunities for concurrency manually using and*.

Attempt two: an arrow

An arrow makes it possible to analyse pipelines statically. Instead of our monadic functions:

val fetch : commit -> source promise
val build : source -> image promise

we can define an arrow type:

type ('a, 'b) arrow

val fetch : (commit, source) arrow
val build : (source, image) arrow

An ('a, 'b) arrow is a pipeline that takes an input of type 'a and produces a result of type 'b. If we define type ('a, 'b) arrow = 'a -> 'b promise then this is the same as the monadic version. However, we can instead make the arrow type abstract and extend it to store whatever static information we require. For example, we could label the arrows:

type ('a, 'b) arrow = {
  f : 'a -> 'b promise;
  label : string;
}

Here, arrow is a record. f is the old monadic function and label is the “static analysis”.

Users can’t see the internals of the arrow type, and must build up pipelines using functions provided by the arrow implementation. There are three basic functions available:

val arr : ('a -> 'b) -> ('a, 'b) arrow
val ( >>> ) : ('a, 'b) arrow -> ('b, 'c) arrow -> ('a, 'c) arrow
val first : ('a, 'b) arrow -> (('a * 'c), ('b * 'c)) arrow

arr takes a pure function and gives the equivalent arrow. For our promise example, that means the arrow returns a promise that is already fulfilled. >>> joins two arrows together. first takes an arrow from 'a to 'b and makes it work on pairs instead. The first element of the pair will be processed by the given arrow and the second component is returned unchanged.

We can have these operations automatically create new arrows with appropriate f and label fields. For example, in a >>> b, the resulting label field could be the string {a.label} >>> {b.label}. This means that we can display the pipeline without having to run it first, and we could easily replace label with something more structured if needed.

With this our first example changes from:

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

let example1 =
  fetch >>> build >>> test

That seems quite pleasant, although we did have to give up our variable names. But things start to get complicated with larger examples. For example2, we need to define a few standard combinators:

(** Process the second component of a tuple, leaving the first unchanged. *)
let second f =
  let swap (x, y) = (y, x) in
  arr swap >>> first f >>> arr swap

(** [f *** g] processes the first component of a pair with [f] and the second
    with [g]. *)
let ( *** ) f g =
  first f >>> second g

(** [f &&& g] processes a single value with [f] and [g] in parallel and
    returns a pair with the results. *)
let ( &&& ) f g =
  arr (fun x -> (x, x)) >>> (f *** g)

Then, example2 changes from:

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile = make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  build "4.07";
  build "4.08"

to:

let example2 =
  let build ocaml_version =
    first (arr (fun base -> make_dockerfile ~base ~ocaml_version))
    >>> build_with_dockerfile ~label:ocaml_version
    >>> test
  in
  arr (fun c -> ((), c))
  >>> (docker_pull "ocaml/opam2" *** fetch)
  >>> (build "4.07" &&& build "4.08")
  >>> arr (fun ((), ()) -> ())

We’ve lost most of the variable names and instead have to use tuples, remembering where our values are. It’s not too bad here with two values, but it gets very difficult very quickly as more are added and we start nesting tuples. We also lost the ability to use an optional labelled argument in build ~dockerfile src and instead need to use a new operation that takes a tuple of the dockerfile and the source.

Imagine that running the tests now requires getting the test cases from the source code. In the original code, we’d just change test image to test image ~using:src. In the arrow version, we need to duplicate the source before the build step, run the build with first build_with_dockerfile, and make sure the arguments are the right way around for a new test_using.

Attempt three: a dart

I started wondering whether there might be an easier way to achieve the same static analysis that you get with arrows, but without the point-free syntax, and it seems that there is. Consider the monadic version of example1. We had:

val build : source -> image promise
val test : image -> results promise

let example1 commit =
  let* src = fetch commit in
  let* image = build src in
  test image

If you didn’t know about monads, there is another way you might try to do this. Instead of using let* to wait for the fetch to complete and then calling build with the source, you might define build and test to take promises as inputs:

val build : source promise -> image promise
val test : image promise -> results promise

After all, fetching gives you a source promise and you want an image promise, so this seems very natural. We could even have example1 take a promise of the commit. Then it looks like this:

let example1 commit =
  let src = fetch commit in
  let image = build src in
  test image

That’s good, because it’s identical to the simple version we started with. The problem is that it is inefficient:

We call example1 with the promise of the commit (we don’t know what it is yet).
Without waiting to find out which commit we’re testing, we call fetch, getting back a promise of some source.
Without waiting to get the source, we call build, getting a promise of an image.
Without waiting for the build, we call test, getting a promise of the results.

We return the final promise of the test results immediately, but we haven’t done any real work yet. Instead, we’ve built up a long chain of promises, wasting memory.

However, in this situation what we want is to perform a static analysis. i.e. we want to build up in memory some data structure representing the pipeline… and this is exactly what our “inefficient” use of the monad produces!

To make this useful, we need the primitive operations (such as fetch) to provide some information (e.g. labels) for the static analysis. OCaml’s let syntax doesn’t provide an obvious place for a label, but I was able to define an operator (let**) that returns a function taking a label argument. It can be used to build primitive operations like this:

let fetch commit =
  "fetch" |>
  let** commit = commit in
  (* (standard monadic implementation of fetch goes here) *)

So, fetch takes a promise of a commit, does a monadic bind on it to wait for the actual commit and then proceeds as before, but it labels the bind as a fetch operation. If fetch took multiple arguments, it could use and* to wait for all of them in parallel.

In theory, the body of the let** in fetch could contain further binds. In that case, we wouldn’t be able to analyse the whole pipeline at the start. But as long as the primitives wait for all their inputs at the start and don’t do any binds internally, we can discover the whole pipeline statically.

We can choose whether to expose these bind operations to application code or not. If let* (or let**) is exposed, then applications get to use all the expressive power of monads, but there will be points where we cannot show the whole pipeline until some promise resolves. If we hide them, then applications can only make static pipelines.

My approach so far has been to use let* as an escape hatch, so that any required pipeline can be built, but I later replace any uses of it by more specialised operations. For example, I added:

val list_map : ('a t -> 'b t) -> 'a list t -> 'b list t

This processes each item in a list that isn’t known until runtime. However, we can still know statically what pipeline we will apply to each item, even though we don’t know what the items themselves are. list_map could have been implemented using let*, but then we wouldn’t be able to see the pipeline statically.

Here are the other two examples, using the dart approach:

let example2 commit =
  let src = fetch commit in
  let base = docker_pull "ocaml/opam2" in
  let build ocaml_version =
    let dockerfile =
      let+ base = base in
      make_dockerfile ~base ~ocaml_version in
    let image = build ~dockerfile src ~label:ocaml_version in
    test image
  in
  all [
    build "4.07";
    build "4.08"
  ]

Compared to the original, we have an all to combine the results, and there’s an extra let+ base = base when calculating the dockerfile. let+ is just another syntax for map, used here because I chose not to change the signature of make_dockerfile. Alternatively, we could have make_dockerfile take a promise of the base image and do the map inside it instead. Because map takes a pure body (make_dockerfile just generates a string; there are no promises or errors) it doesn’t need its own box on the diagrams and we don’t lose anything by allowing its use.

let example3 commit =
  let src = fetch commit in
  let image = build src in
  let ok = test image in
  let revdeps = get_revdeps src in
  gate revdeps ~on:ok |>
  list_iter ~pp:Fmt.string example1

This shows another custom operation: gate revdeps ~on:ok is a promise that only resolves once both revdeps and ok have resolved. This prevents it from testing the library’s revdeps until the library’s own tests have passed, even though it could do this in parallel if we wanted it to. Whereas with a monad we have to enable concurrency explicitly where we want it (using and*), with a dart we have to disable concurrency explicitly where we don’t want it (using gate).

I also added a list_iter convenience function, and gave it a pretty-printer argument so that we can label the cases in the diagrams once the list inputs are known.

Finally, although I said that you can’t use let* inside a primitive, you can still use some other monad (that doesn’t generate diagrams). In fact, in the real system I used a separate let> operator for primitives. That expects a body using non-diagram-generating promises provided by the underlying promise library, so you can’t use let* (or let>) inside the body of a primitive.

Comparison with arrows

Given a “dart” you can create an arrow interface from it easily by defining e.g.

type ('a, 'b) arrow = 'a promise -> 'b promise

Then arr is just map and f >>> g is just fun x -> g (f x). first can be defined easily too, assuming you have some kind of function for doing two things in parallel (like our and* above).

So a dart API (even with let* hidden) is still enough to express any pipeline you can express using an arrow API.

The Haskell Arrow tutorial uses an example where an arrow is a stateful function. For example, there is a total arrow that returns the sum of its input and every previous input it has been called with. e.g. calling it three times with inputs 1 2 3 produces outputs 1 3 6. Running a pipeline on a sequence of inputs returns the sequence of outputs.

The tutorial uses total to define a mean1 function like this:

mean1 = (total &&& (arr (const 1) >>> total)) >>> arr (uncurry (/))

So this pipeline duplicates each input number, replaces the second one with 1, totals both streams, and then replaces each pair with its ratio. Each time you put another number into the pipeline, you get out the average of all values input so far.

The equivalent code using the dart style would be (OCaml uses /. for floating-point division):

let mean values =
  let t = total values in
  let n = total (const 1.0) in
  map (uncurry (/.)) (pair t n)

That seems more readable to me. We can simplify the code slightly by defining the standard operators let+ (for map) and and+ (for pair):

let (let+) x f = map f x
let (and+) = pair

let mean values =
  let+ t = total values
  and+ n = total (const 1.0) in
  t /. n

This is not a great example of an arrow anyway, because we don’t use the output of one stateful function as the input to another, so this is actually just a plain applicative.

We could easily extend the example pipeline with another stateful function though, perhaps by adding some smoothing. That would look like mean1 >>> smooth in the arrow notation, and values |> mean |> smooth (or smooth (mean values)) in the dart notation.

Note: Haskell does also have an Arrows syntax extension, which allows the Haskell code to be written as:

mean2 = proc value -> do
    t <- total -< value
    n <- total -< 1
    returnA -< t / n

That’s more similar to the dart notation.

Larger examples

I’ve put up a library using a slightly extended version of these ideas at ocurrent/ocurrent. The lib_term subdirectory is the part relevant to this blog post, with the various combinators described in TERM. The other directories handle more concrete details, such as integration with the Lwt promise library, and providing the admin web UI or the Cap’n Proto RPC interface, as well as plugins with primitives for using Git, GitHub, Docker and Slack.

OCaml Docker base image builder

ocurrent/docker-base-images contains a pipeline that builds Docker base images for OCaml for various Linux distributions, CPU architectures, OCaml compiler versions and configuration options. For example, to test OCaml 4.09 on Debian 10, you can do:

$ docker run --rm -it ocurrent/opam:debian-10-ocaml-4.09

:~$ ocamlopt --version
4.09.0

:~$ opam depext -i utop
[...]

:~$ utop
----+-------------------------------------------------------------+------------------
    | Welcome to utop version 2.4.2 (using OCaml version 4.09.0)! |
    +-------------------------------------------------------------+

Type #utop_help for help about using utop.

-( 11:50:06 )-< command 0 >-------------------------------------------{ counter: 0 }-
utop # 

Here’s what the pipeline looks like (click for full-size):

It pulls the latest Git commit of opam-repository each week, then builds base images containing that and the opam package manager for each distribution version, then builds one image for each supported compiler variant. Many of the images are built on multiple architectures (amd64, arm32, arm64 and ppc64) and pushed to a staging area on Docker Hub. Then, the pipeline combines all the hashes to push a multi-arch manifest to Docker Hub. There are also some aliases (e.g. debian means debian-10-ocaml-4.09 at the moment). Finally, if there is any problem then the pipeline sends the error to a Slack channel.

You might wonder whether we really need a pipeline for this, rather than a simple script run from a cron-job. But having a pipeline allows us to see what the pipeline will do before running it, watch the pipeline’s progress, restart failed jobs individually, etc, with almost the same code we would have written anyway.

You can read pipeline.ml if you want to see the full pipeline.

OCaml CI

ocurrent/ocaml-ci is an (experimental) GitHub app for testing OCaml projects. The pipeline gets the list of installations of the app, gets the configured repositories for each installation, gets the branches and PRs for each repository, and then tests the head of each one against multiple Linux distributions and OCaml compiler versions. If the project uses ocamlformat, it also checks that the commit is formatted exactly as ocamlformat would do it.

The results are pushed back to GitHub as the commit status, and also recorded in a local index for the web and tty UIs. There’s quite a lot of red here mainly because if a project doesn’t support a particular version of OCaml then the build is marked as failed and shows up as red in the pipeline, although these failures are filtered out when making the GitHub status report. We probably need a new colour for skipped stages.

Conclusions

It’s convenient to write CI/CD pipelines as if they were single-shot scripts that run the steps once, in series, and always succeed, and then with only minor changes have the pipeline run the steps whenever the input changes, in parallel, with logging, error reporting, cancellation and rebuild support.

Using a monad allows any program to be converted easily to have these features, but, as with a regular program, we don’t know what the program will do with some data until we run it. In particular, we can only automatically generate diagrams showing steps that have already started.

The traditional way to do static analysis is to use an arrow. This is a little more limited than a monad, because the structure of the pipeline can’t change depending on the input data, although we can add limited flexibility such as optional steps or a choice between two branches. However, writing pipelines using arrow notation is difficult because we have to program in a point-free style (without variables).

We can get the same benefits of static analysis by using a monad in an unusual way, here referred to as a “dart”. Instead of functions that take plain values and return wrapped values, our functions both take and return wrapped values. This results in a syntax that looks identical to plain programming, but allows static analysis (at the cost of not being able to manipulate the wrapped values directly).

If we hide (or don’t use) the monad’s let* (bind) function then the pipelines we create can always be determined statically. If we use a bind, then there will be holes in the pipeline that may expand to more pipeline stages as the pipeline runs.

Primitive steps can be created by using a single “labelled bind”, where the label provides the static analysis for the atomic component.

I haven’t seen this pattern used before (or mentioned in the arrow documentation), and it seems to provide exactly the same benefits as arrows with much less difficulty. If this has a proper name, let me know!

This work was funded by OCaml Labs.

Hide

On fixed-point theorems in synthetic computability — Andrej Bauer, Nov 06, 2019

I forgot to record the fact that already two years ago I wrote a paper on Lawvere's fixed-point theorem in synthetic computability:

Andrej Bauer: On fixed-point theorems in synthetic computability. Tbilisi Mathematical Journal, Volume 10: Issue 3, pp. 167–181.

It was a special issue in honor of Professors Peter J. Freyd and F. William Lawvere on the occasion of their 80th birthdays.

Lawvere's paper "Diagonal arguments and cartesian closed categories proves a beautifully simple fixed poi…

Runners in action — Andrej Bauer, Oct 27, 2019

It has been almost a decade since Matija Pretnar and I posted the first blog posts about programming with algebraic effects and handlers and the programming language Eff. Since then handlers have become a well-known control mechanism in programming languages.

Handlers and monads excel at simulating effects, either in terms of other effects or as pure computations. For example, the familiar state monad implements mutable state with (pure) state-passing functions, and there are many more examples. But I have always felt that handlers and monads are not very good at explaining how a program interacts with its external environment and how it gets to perform real-world effects.

Danel Ahman and I have worked for a while on attacking the question on how to better model external resources and what programming constructs are appropriate for working with them. The time is right for us to show what we have done so far. The theoretical side of things is explained in our paper Runners in action, Danel implemented a Haskell library Haskell-Coop to go with the paper, and I implemented a programming language Coop.

General-purpose programming languages, even the so-called pure ones, have to have some account of interaction with the external environment. A popular choice is to provide a foreign-function interface that connects the language with an external library, and through it with an operating system and the universe. A more nuanced approach would differentiate between a function that just happens to be written in a different language, and one that actually performs an effect. The latter kind is known as an algebraic operation in the algebraic-effects-and-handlers way of doing things.

A bad approach to modeling the external world is to pretend that it is internal to the language. One would think that this is obvious but it is not. For instance, Haskell represents the interface to the external world through the IO monad. But what is this monad really? How does it get to interact with the external world? The Haskell Wiki page which answers this question has the following disclaimer:

"Warning: The following story about IO is incorrect in that it cannot actually explain some important aspects of IO (including interaction and concurrency). However, some people find it useful to begin developing an understanding."

The Wiki goes on to say how IO is a bit like a state monad with an imaginary RealWorld state, except that of course RealWorld is not really a Haskell type, or at least not one that actually holds the state of the real world.

The situation with Eff is not much better: it treats some operations at the top-level in a special way. For example, if print percolates to the top level, it turns into a real print that actually causes an effect. So it looks like there is some sort of "top level handler" that models the real world, but that cannot be the case: a handler may discard the continuation or run it twice, but Eff hardly has the ability to discard the external world, or to make it bifurcate into two separate realities.

If IO monad is not an honest monad and a top-level handler is not really a handler, then what we have is a case of ingenious hackery in need of proper programming-language design.

How precisely does an operation call in the program cause an effect in the external world? As we have just seen, some sort of runtime environment or top level needs to relate it to the external world. From the viewpoint of the program, the external world appears as state which is not directly accessible, or even representable in the language. The effect of calling an operation $\mathtt{op}(a,\kappa)$ is to change the state of the world, and to get back a result. We can model the situation with a map $\overline{\mathtt{op}} : A \times W \to B \times W$, where $W$ is the set of all states of the world, $A$ is the set of parameters, and $B$ the set of results of the operation. The operation call $\mathtt{op}(a, \kappa)$ is "executed" in the current world $w \in W$ by computing $\overline{\mathtt{op}}(a,w) = (b, w')$ to get the next world $w'$ and a result $b$. The program then proceeds with the continuation $\kappa\,b$ in the world $w'$. Notice how the world $w$ is an external entity that is manipulated by the external map $\overline{\mathtt{op}}$ realistically in a linear fashion, i.e., the world is neither discarded nor copied, just transformed.

What I have just described is not a monad or a handler, but a comodel, also known as a runner, and the map $\overline{\mathtt{op}}$ is not an operation, but a co-operation. This was all observed a while ago by Gordon Plotkin and John Power, Tarmo Uustalu, and generalized by Rasmus Møgelberg and Sam Staton, see our paper for references. Perhaps we should replace "top-level" handlers and "special" monads with runners?

Danel and I worked out how effectful runners (a generalization of runners that supports other effects in addition to state) provide a mathematical model of resource management. They also give rise to a programming concept that models top-level external resources, as well as allows programmers to modularly define their own “virtual machines” and run code inside them. Such virtual machines can be nested and combined in interesting ways. We capture the core ideas of programming with runners in an equational calculus $\lambda_{\mathsf{coop}}$, that guarantees the linear use of resources and execution of finalization code.

An interesting practical aspect of $\lambda_{\mathsf{coop}}$, that was begotten by theory, is modeling of extra-ordinary circumstances. The external environment should have the ability to signal back to the program an extra-ordinary circumstance that prevents if from returning a result. This is normally accomplished by an exception mechanism, but since the external world is stateful, there are two ways of combining it with exceptions, namely the sum and the tensor of algebraic theories. Which one is the right one? Both! After a bit of head scratching we realized that the two options are (analogous to) what is variously called "checked" and "non-checked" exceptions, errors and signals, or synchronous and asynchronous exceptions. And so we included in $\lambda_{\mathsf{coop}}$ both mechanisms: ordinary exceptions, which are special events that disrupt the flow of user code but can be caught and attended to, and signals which are unrecoverable failures that irrevocably kill user code, but can still be finalized. We proved a finalization theorem which gives strong guarantees about resources always being properly finalized.

If you are familiar with handlers, as a first approximation you can think of runners as handlers that use the continuation at most once in a tail-call position. Many handlers are already of this form but not all. Non-determinism, probability, and handlers that hijack the continuation (delimcc, threads, and selection functionals) fall outside of the scope of runners. Perhaps in the future we can resurrect some of these (in particular it seems like threads, or even some form of concurrency would be worth investigating). There are many other directions of possible future investigations: efficient compilation, notions of correctness, extensions to the simple effect subtyping discipline that we implemented, etc.

To find out more, we kindly invite you to have a look at the paper, and to try out the implementations. The prototype programming language Coop implements and extends $\lambda_{\mathsf{coop}}$. You can start by skimming the Coop manual and the examples. If you prefer to experiment on your own, you might prefer the Haskell-Coop library, as it allows you to combine runners with everything else that Haskell has to offer.

Hide

Coq 8.10.1 is out — Coq, Oct 25, 2019

The 8.10.1 release of Coq is available.

Main changes:

fix proof of False when using SProp;
fix an anomaly when unsolved evar in Add Ring;
fix Ltac regression in binding free names in uconstr;
fix handling of unicode input before space;
fix custom extraction of inductives to JSON.

All details can be found in the user manual.

Feedback and bug reports are extremely welcome.

Announcing MirageOS 3.6.0 — MirageOS (Martin Lucina), Oct 18, 2019

MirageOS 3.6.0 release

We are pleased to announce the release of MirageOS 3.6.0. This release updates MirageOS to support Solo5 0.6.0 and later.

New features:

Support for the Solo5 spt (sandboxed process tender) target via mirage configure -t spt. The spt target runs MirageOS unikernels in a minimal strict seccomp sandbox on Linux x86_64, aarch64 and ppc64le hosts.
Support for the Solo5 application manifest, enabling support for multiple network and block storage devices on the hvt, spt and muen

Commas in big numbers everywhere: An OpenType adventure — Jane Street, Oct 14, 2019

My job involves a lot of staring at large numbers, mostly latencies in nanoseconds, and picking out magnitudes like microseconds. I noticed myself constantly counting digits in my text editor, in my terminal, and in Jupyter notebooks in my browser.

Coq 8.10.0 is out — Coq, Oct 07, 2019

The 8.10.0 release of Coq is available.

Main changes:

some quality-of-life bug fixes;
a critical bug fix related to template polymorphism;
native 63-bit machine integers;
a new sort of definitionally proof-irrelevant propositions: SProp;
private universes for opaque polymorphic constants;
string notations and numeral notations;
a new simplex-based proof engine for the tactics lia, nia, lra and nra;
new introduction patterns for SSReflect;
a tactic to rewrite under binders: under;
easy input of…

OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

In our endeavour to encourage professional programmers to understand and use OCaml, OCamlPro will be giving two training sessions, in French, in our Paris offices:

OCaml Beginner course for professional programmers (5-6 Nov)
OCaml Expertise (7-8 Nov).

The “Expert” OCaml course is for already experienced OCaml programmers to better understand advanced type system possibilities (objects, GADTs), discover GC internals, write “compiler-optimizable” code.

These sessions are …

Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

We're glad to announce the first release of `mrmime`, a parser and a generator of emails. This library provides an OCaml way to analyze and craft an email. The eventual goal is to build an entire unikernel-compatible stack for email (such as SMTP or IMAP).

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the h…

In this article, we will show what is currently possible with mrmime and present a few of the useful libraries that we developed along the way.

An email parser

Some years ago, Romain gave a talk about what an email really is. Behind the human-comprehensible format (or rich-document as we said a long time ago), there are several details of emails which complicate the process of analyzing them (and can be prone to security lapses). These details are mostly described by three RFCs:

Even though they are cross-compatible, providing full legacy email parsing is an archaeological exercise: each RFC retains support for the older design decisions (which were not recognized as bad or ugly in 1970 when they were first standardized).

The latest email-related RFC (RFC5322) tried to fix the issue and provide a better formal specification of the email format – but of course, it comes with plenty of obsolete rules which need to be implemented. In the standard, you find both the current grammar rule and its obsolete equivalent.

An extended email parser

Even if the email format can defined by "only" 3 RFCs, you will miss email internationalization (RFC6532), the MIME format (RFC2045, RFC2046, RFC2047, RFC2049), or certain details needed to be interoperable with SMTP (RFC5321). There are still more RFCs which add extra features to the email format such as S/MIME or the Content-Disposition field.

Given this complexity, we took the most general RFCs and tried to provide an easy way to deal with them. The main difficulty is the multipart parser, which deals with email attachments (anyone who has tried to make an HTTP 1.1 parser knows about this).

A realistic email parser

Respecting the rules described by RFCs is not enough to be able to analyze any email from the real world: existing email generators can, and do, produce non-compliant email. We stress-tested mrmime by feeding it a batch of 2 billion emails taken from the wild, to see if it could parse everything (even if it does not produce the expected result). Whenever we noticed a recurring formatting mistake, we updated the details of the ABNF to enable mrmime to parse it anyway.

A parser usable by others

One demonstration of the usability of mrmime is `ocaml-dkim`, which wants to extract a specific field from your mail and then verify that the hash and signature are as expected.

ocaml-dkim is used by the latest implementation of `ocaml-dns` to request public keys in order to verify email.

The most important question about ocaml-dkim is: is it able to verify your email in one pass? Indeed, currently some implementations of DKIM need 2 passes to verify your email (one to extract the DKIM signature, the other to digest some fields and bodies). We focused on verifying in a single pass in order to provide a unikernel SMTP relay with no need to store your email between verification passes.

An email generator

OCaml is a good language for making little DSLs for specialized use-cases. In this case, we took advantage of OCaml to allow the user to easily craft an email from nothing.

The idea is to build an OCaml value describing the desired email header, and then let the Mr. MIME generator transform this into a stream of characters that can be consumed by, for example, an SMTP implementation. The description step is quite simple:

#require "mrmime" ;;
#require "ptime.clock.os" ;;

open Mrmime

let romain_calascibetta =
  let open Mailbox in
  Local.[ w "romain"; w "calascibetta" ] @ Domain.(domain, [ a "gmail"; a "com" ])

let john_doe =
  let open Mailbox in
  Local.[ w "john" ] @ Domain.(domain, [ a "doe"; a "org" ])
  |> with_name Phrase.(v [ w "John"; w "D." ])

let now () =
  let open Date in
  of_ptime ~zone:Zone.GMT (Ptime_clock.now ())

let subject =
  Unstructured.[ v "A"; sp 1; v "Simple"; sp 1; v "Mail" ]

let header =
  let open Header in
  Field.(Subject $ subject)
  & Field.(Sender $ romain_calascibetta)
  & Field.(To $ Address.[ mailbox john_doe ])
  & Field.(Date $ now ())
  & empty

let stream = Header.to_stream header

let () =
  let rec go () =
    match stream () with
    | Some buf -> print_string buf; go ()
    | None -> ()
  in
  go ()

This code produces the following header:

Date: 2 Aug 2019 14:10:10 GMT
To: John "D." <john@doe.org>
Sender: romain.calascibetta@gmail.com
Subject: A Simple Mail

78-character rule

One aspect about email and SMTP is about some historical rules of how to generate them. One of them is about the limitation of bytes per line. Indeed, a generator of mail should emit at most 80 bytes per line - and, of course, it should emits entirely the email line per line.

So mrmime has his own encoder which tries to wrap your mail into this limit. It was mostly inspired by Faraday and Format powered with GADT to easily describe how to encode/generate parts of an email.

A multipart email generator

Of course, the main point about email is to be able to generate a multipart email - just to be able to send file attachments. And, of course, a deep work was done about that to make parts, compose them into specific Content-Type fields and merge them into one email.

Eventually, you can easily make a stream from it, which respects rules (78 bytes per line, stream line per line) and use it directly into an SMTP implementation.

This is what we did with the project `facteur`. It's a little command-line tool to send with file attachement mails in pure OCaml - but it works only on an UNIX operating system for instance.

Behind the forest

Even if you are able to parse and generate an email, more work is needed to get the expected results.

Indeed, email is a exchange unit between people and the biggest deal on that is to find a common way to ensure a understable communication each others. About that, encoding is probably the most important piece and when a French person wants to communicate with a latin1 encoding, an American person can still use ASCII.

Rosetta

So about this problem, the choice was made to unify any contents to UTF-8 as the most general encoding of the world. So, we did some libraries which map an encoding flow to Unicode code-point, and we use uutf (thanks to dbuenzli) to normalize it to UTF-8.

The main goal is to avoid a headache to the user about that and even if contents of the mail is encoded with latin1 we ensure to translate it correctly (and according RFCs) to UTF-8.

This project is `rosetta` and it comes with:

`uuuu` for ISO-8859 encoding
`coin` for KOI8-{R,U} encoding
`yuscii` for UTF-7 encoding

Pecu and Base64

Then, bodies can be encoded in some ways, 2 precisely (if we took the main standard):

A base64 encoding, used to store your file
A quoted-printable encoding

So, about the base64 package, it comes with a sub-package base64.rfc2045 which respects the special case to encode a body according RFC2045 and SMTP limitation.

Then, pecu was made to encode and decode quoted-printable contents. It was tested and fuzzed of course like any others MirageOS's libraries.

These libraries are needed for an other historical reason which is: bytes used to store mail should use only 7 bits instead of 8 bits. This is the purpose of the base64 and the quoted-printable encoding which uses only 127 possibilities of a byte. Again, this limitation comes with SMTP protocol.

Conclusion

mrmime is tackling the difficult task to parse and generate emails according to 50 years of usability, several RFCs and legacy rules. So, it still is an experimental project. We reach the first version of it because we are currently able to parse many mails and then generate them correctly.

Of course, a bug (a malformed mail, a server which does not respect standards or a bad use of our API) can appear easily where we did not test everything. But we have the feeling it was the time to release it and let people to use it.

The best feedback about mrmime and the best improvement is yours. So don't be afraid to use it and start to hack your emails with it.

Hide

A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

As you already know if you’ve read our last blogpost, we have updated our OCaml cheat sheets starting with the language and stdlib ones. We know some of you have students to initiate in September and we wanted these sheets to be ready for the start of the school year! We’re working on more sheets for OCaml tools like opam or Dune and important libraries such as Obj Lwt or Core. Keep an eye on our blog or the repo on GitHub to follow all the updates.

Going through the documentation was a jour…

Going through the documentation was a journey to the past: we have looked back on 8 years of evolution of the OCaml language and library. New feature after new feature, OCaml has seen many changes. Needless to say, upgrading our cheat sheets to OCaml 4.08.1 was a trip down memory lane. We wanted to share our throwback experience with you!

2011

Fabrice Le Fessant first published our cheat sheets in 2011, the year OCamlPro was created! At the time, OCaml was in its 3.12 version and just got its current name agreed upon. First-class modules were the new big thing, Camlp4 and Camlp5 were battling for the control of the syntax extension world and Godi and Oasis were the packaging rage.

2012

Right after 3.12 came the switch to OCaml 4.00 which brought a major change: GADTs (generalized algebraic data types). Most of OCaml’s developers don’t use their almighty typing power, but the possibilities they provide are really helpful in some cases, most notably the format overhaul. They’re also a fun way to troll a beginner asking how to circumvent the typing system on Stack Overflow. Since most of us might lose track of their exact syntax, GADTs deserve their place in the updated sheet (if you happen to be OCamlPro’s CTO, of course the writer of this blogpost remembers how to use GADTs at all times).

On the standard library side, the big change was the switch of Hashtbl to Murmur 3 and the support for seeded randomization.

2013

With OCaml 4.01 came constructor disambiguation, but there isn’t really a way to add this to the sheet. This feature allows you to avoid misguided usage of polymorphic variants, but that’s a matter of personal taste (there’s a well-known rule that if you refresh the comments section enough times, someone —usually called Daniel— will appear to explain polymorphic variants’ superiority to you). -ppx rewriters were introduced in this version as well.

The standard library got a few new functions. Notably, Printexc.get_callstack for stack inspection, the optimized application operators |> and @@ and Format.asprintf.

2014

Gabriel Scherer, on the Caml-list, end of January:

TL;DR: During the six next months, we will follow pull requests (PR) posted on the github mirror of the OCaml distribution, as an alternative to the mantis bugtracker. This experiment hopes to attract more people to participate in the extremely helpful and surprisingly rewarding activity of patch reviews.

Can you guess which change to the cheat-sheets came with 4.02? It’s a universally-loved language feature added in 2014. Still don’t know? It is exceptional! Got it?

Drum roll… it is the match with exception construction! It made our codes simpler, clearer and in some cases more efficient. A message to people who want to improve the language: please aim for that.

This version also added the {quoted|foo|quoted} syntax (which broke comments), generative functors, attributes and extension nodes, extensible data types, module aliases and, of course, immutable strings (which was optional at the time). Immutable strings is the one feature that prompted us to remove a line from the cheat sheets. More space is good. Camlp4 and Labltk moved out of the distribution.

In consequence of immutable strings, Bytes and BytesLabel were added to the library. For the great pleasure of optimization addicts, raise_notrace popped up. Under the hood, the format type was re-implemented using GADTs.

2015

This release was so big that 4.02.2 feels like a release in itself, with the adding of nonrec and #... operators.

The standard library was spared by this bug-fix themed release. Note that this is the last comparatively slow year of OCaml as the transition to GitHub would soon make features multiply, as hindsight teaches us.

2016

Speaking of a major release, we’re up to OCaml 4.03! It introduced inline records, a GADT exhaustiveness check on steroids (with -> . to denote unreachability) and standard attributes like warning, inlined, unboxed or immediate. Colors appeared in the compiler and last but not least, it was the dawn of a new option called Flambda.

The library saw a lot of useful new functions coming in: lots of new iterators for Array, an equal function in most basic type modules, Uchar, the *_ascii alternatives and, of course, Ephemeron.

4.04 was much more restrained, but it was the second release in a single year. Local opening of module with the M.{} syntax was added along with the let exception ... in construct. String.split_on_char was notably added to the stdlib which means we don’t have to rewrite it anymore.

2017

We now get to 4.05… which did not change the language. Not that the development team wasn’t busy, OCaml just got better without any change to the syntax.

On the library side however, much happened, with the adding of *_opt functions pretty much everywhere. If you’re using the OCaml compiler from Debian, this is where you might think the story ends. You’d be wrong…

…because 4.06 added a lot! My own favorite feature from this release has to be user-defined indexing operators. This is also when safe-string became the default, giving worthwhile work to every late maintainer in the community. This release also added one awesome function in the standard library: Map.update.

2018

4.07 was aimed towards solidifying the language. It added empty variants and type-based selection of GADT constructors to the mix.

On the library side, one old and two new modules were added, with the integration of Bigarray, Seq and Float.

2019

And here we are with 4.08, in the present day! We can now put exceptions under or-patterns, which is the only language change from this release we propagated to the sheet. Time will tell if we need to add custom binding operators or [@@alert]. Pervasives is now deprecated in profit of Stdlib and new modules are popping up (Int, Bool, Fun, Result… did we miss one?) while Sort made its final deprecation warning.

We did not add 4.09 to this journey to the past, as this release is still solidly in the now at the time of this blogpost. Rest assured, we will see much more awesome features in OCaml in the future! In the meantime, we are working on updating more cheat sheets: keep posted!

Hide

Frama-C 19.1 (Potassium) is out. Download ithere. — Frama-C, Sep 17, 2019

Coq 8.10+beta3 is out — Coq, Sep 16, 2019

The third beta release of Coq 8.10 is available for testing.

This third β version includes various bug fixes and improvements, including:

improved warning on coercion path ambiguity;
support for OCaml extraction of primitive machine integers;
fix for the soundness issue with template polymorphism;
fix extraction of dependent record projections to OCaml.

More details are given in the user manual.

Feedback and bug reports are extremely welcome.

Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

In 2011, we shared several cheat sheets for OCaml. Cheat sheets are helpful to refer to, as an overview of the documentation when you are programming, especially when you’re starting in a new language. They are meant to be printed and pinned on your wall, or to be kept in handy on a spare screen. We hope they will help you out when your rubber duck is rubbish at debugging your code!

Since we first shared them, OCaml and its related tools have evolved. We decided to refresh them and started…

Frama-Clang 0.0.7 is out. Download ithere. — Frama-C, Sep 13, 2019

Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

In our first article we mostly discussed the API design of decompress and did not talk too much about the issue of optimizing performance. In this second article, we will relate our experiences of optimizing decompress.

As you might suspect, decompress needs to be optimized a lot. It was used by several projects as an underlying layer of some formats (like Git), so it can be a real bottleneck in those projects. Of course, we start with a footgun by using a garbage-collected language; comparing t…

However, using something like decompress instead of C implementations can be very interesting for many purposes, especially when thinking about unikernels. As we said in the previous article, we can take the advantage of the runtime and the type-system to provide something safer (of course, it's not really true since zlib has received several security audits).

The main idea in this article is not to give snippets to copy/paste into your codebase but to explain some behaviors of the compiler / runtime and hopefully give you some ideas about how to optimize your own code. We'll discuss the following optimizations:

specialization
inlining
untagged integers
exceptions
unrolling
hot-loop
caml_modify
representation sizes

Cautionary advice

Before we begin discussing optimization, keep this rule in mind:

Only perform optimization at the end of the development process.

An optimization pass can change your code significantly, so you need to keep a state of your project that can be trusted. This state will provide a comparison point for both benchmarks and behaviors. In other words, your stable implementation will be the oracle for your benchmarks. If you start with nothing, you'll achieve arbitrarily-good performance at the cost of arbitrary behavior!

We optimized decompress because we are using it in bigger projects for a long time (2 years). So we have an oracle (even if zlib can act as an oracle in this special case).

Specialization

One of the biggest specializations in decompress is regarding the min function. If you don't know, in OCaml min is polymorphic; you can compare anything. So you probably have some concerns about how min is implemented?

You are right to be concerned: if you examine the details, min calls the C function do_compare_val, which traverses your structure and does a comparison according the run-time representation of your structure. Of course, for integers, it should be only a cmpq assembly instruction. However, some simple code like:

let x = min 0 1

will produce this CMM and assembly code:

(let x/1002 (app{main.ml:1,8-15} "camlStdlib__min_1028" 1 3 val)
   ...)

.L101:
        movq    $3, %rbx
        movq    $1, %rax
        call    camlStdlib__min_1028@PLT

Note that beta-reduction, inlining and specialization were not done in this code. OCaml does not optimize your code very much – the good point is predictability of the produced assembly output.

If you help the compiler a little bit with:

external ( <= ) : int -> int -> bool = "%lessequal"
let min a b = if a <= b then a else b [@@inline]

let x = min 0 1

We have:

(function{main.ml:2,8-43} camlMain__min_1003 (a/1004: val b/1005: val)
 (if (<= a/1004 b/1005) a/1004 b/1005))

(function camlMain__entry ()
 (let x/1006 1 (store val(root-init) (+a "camlMain" 8) 1)) 1a)

.L101:
        cmpq    %rbx, %rax
        jg      .L100
        ret

So we have all optimizations, in this produced code, x was evaluated as 0 (let x/... (store ... 1)) (beta-reduction and inlining) and min was specialized to accept only integers – so we are able to emit cmpq.

Results

With specialization, we won 10 Mb/s on decompression, where min is used in several places. We completely avoid an indirection and a call to the slow do_compare_val function.

This kind of specialization is already done by `flambda`, however, we currently use OCaml 4.07.1. So we decided to this kind of optimization by ourselves.

Inlining

In the first example, we showed code with the [@@inline] keyword which is useful to force the compiler to inline a little function. We will go outside the OCaml world and study C code (gcc 5.4.0) to really understand inlining.

In fact, inlining is not necessarily the best optimization. Consider the following (nonsensical) C program:

#include <stdio.h>
#include <string.h>
#include <unistd.h>
#include <time.h>
#include <stdlib.h>

#ifdef HIDE_ALIGNEMENT
__attribute__((noinline, noclone))
#endif
void *
hide(void * p) { return p; }

int main(int ac, const char *av[])
{
  char *s = calloc(1 << 20, 1);
  s = hide(s);

  memset(s, 'B', 100000);

  clock_t start = clock();

  for (int i = 0; i < 1280000; ++i)
    s[strlen(s)] = 'A';

  clock_t end = clock();

  printf("%lld\n", (long long) (end-start));

  return 0;
}

We will compile this code with -O2 (the second level of optimization in C), once with -DHIDE_ALIGNEMENT and once without. The assembly emitted differs:

.L3:
    movq    %rbp, %rdi
    call    strlen
    subl    $1, %ebx
    movb    $65, 0(%rbp,%rax)
    jne    .L3

.L3:
    movl    (%rdx), %ecx
    addq    $4, %rdx
    leal    -16843009(%rcx), %eax
    notl    %ecx
    andl    %ecx, %eax
    andl    $-2139062144, %eax
    je    .L3

In the first output (with -DHIDE_ALIGNEMENT), the optimization pass decides to disable inlining of strlen; in the second output (without -DHIDEAlIGNEMENT), it decides to inline strlen (and do some other clever optimizations). The reason behind this complex behavior from the compiler is clearly described here.

But what we want to say is that inlining is not an automatic optimization; it might act as a pessimization. This is the goal of flambda: do the right optimization under the right context. If you are really curious about what gcc does and why, even if it's very interesting, the reverse engineering of the optimization process and which information is relevant about the choice to optimize or not is deep, long and surely too complicated.

A non-spontaneous optimization is to annotate some parts of your code with [@@inline never] – so, explicitly say to the compiler to not inline the function. This constraint is to help the compiler to generate a smaller code which will have more chance to fit under the processor cache.

For all of these reasons, [@@inline] should be used sparingly and an oracle to compare performances if you inline or not this or this function is necessary to avoid a pessimization.

In `decompress`

Inlining in decompress was done on small functions which need to allocate to return a value. If we inline them, we can take the opportunity to store returned value in registers (of course, it depends how many registers are free).

As we said, the goal of the inflator is to translate a bit sequence to a byte. The largest bit sequence possible according to RFC 1951 has length 15. So, when we process an inputs flow, we eat it 15 bits per 15 bits. For each packet, we want to recognize an existing associated bit sequence and then, binded values will be the real length of the bit sequence and the byte:

val find : bits:int -> { len: int; byte: int; }

So for each call to this function, we need to allocate a record/tuple. It's why we choose to inline this function. min was inlined too and some other small functions. But as we said, the situation is complex; where we think that inlining can help us, it's not systematically true.

NOTE: we can recognize bits sequence with, at most, 15 bits because a Huffman coding is prefix-free.

Untagged integers

When reading assembly, the integer 0 is written as $1. It's because of the GC bit needed to differentiate a pointer and an unboxed integer. This is why, in OCaml, we talk about a 31-bits integer or a 63-bits integer (depending on your architecture).

We will not try to start a debate about this arbitrary choice on the representation of an integer in OCaml. However, we can talk about some operations which can have an impact on performances.

The biggest example is about the mod operation. Between OCaml and C, % or mod should be the same:

let f a b = a mod b

The output assembly is:

.L105:
        movq    %rdi, %rcx
        sarq    $1, %rcx     // b >> 1
        movq    (%rsp), %rax
        sarq    $1, %rax     // a >> 1
        testq   %rcx, %rcx   // b != 0
        je      .L107
        cqto
        idivq   %rcx         // a % b
        jmp     .L106
.L107:
        movq    caml_backtrace_pos@GOTPCREL(%rip), %rax
        xorq    %rbx, %rbx
        movl    %ebx, (%rax)
        movq    caml_exn_Division_by_zero@GOTPCREL(%rip), %rax
        call    caml_raise_exn@PLT
.L106:
        salq    $1, %rdx     // x << 1
        incq    %rdx         // x + 1
        movq    %rbx, %rax

where idiomatically the same C code produce:

.L2:
        movl    -12(%rbp), %eax
        cltd
        idivl   -8(%rbp)
        movl    %edx, -4(%rbp)

Of course, we can notice firstly the exception in OCaml (Divided_by_zero) - which is pretty good because it protects us against an interrupt from assembly (and keep the trace). Then, we need to untag a and b with sarq assembly operation. We do, as the C code, idiv and then we must retag returned value x with salq and incq.

So in some parts, it should be more interesting to use Nativeint. However, by default, a nativeint is boxed. boxed means that the value is allocated in the OCaml heap alongside a header.

Of course, this is not what we want so, if our nativeint ref (to have side-effect, like x) stay inside a function and then, you return the real value with the deref ! operator, OCaml, by a good planet alignment, can directly use registers and real integers. So it should be possible to avoid these needed conversions.

Readability versus performance

We use this optimization only in few parts of the code. In fact, switch between int and nativeint is little bit noisy:

hold := Nativeint.logor !hold Nativeint.(shift_left (of_int (unsafe_get_uint8 d.i !i_pos)) !bits)

In the end, we only gained 0.5Mb/s of inflation rate, so it's not worthwhile to do systematically this optimization. Especially that the gain is not very big. But this case show a more troubling problem: loss of readability.

In fact, we can optimize more and more a code (OCaml or C) but we lost, step by step, readability. You should be afraid by the implementation of strlen for example. In the end, the loss of readability makes it harder to understand the purpose of the code, leading to errors whenever some other person (or you in 10 years time) tries to make a change.

And we think that this kind of optimization is not the way of OCaml in general where we prefer to produce an understandable and abstracted code than a cryptic and super fast one.

Again, flambda wants to fix this problem and let the compiler to do this optimization. The goal is to be able to write a fast code without any pain.

Exceptions

If you remember our article about the release of base64, we talked a bit about exceptions and used them as a jump. In fact, it's pretty common for an OCaml developer to break the control-flow with an exception. Behind this common design/optimization, it's about calling convention.

Indeed, choose the jump word to describe OCaml exception is not the best where we don't use setjmp/longjmp.

In the details, when you start a code with a try .. with, OCaml saves a trap in the stack which contains information about the with, the catcher. Then, when you raise, you jump directly to this trap and can just discard several stack frames (and, by this way, you did not check each return codes).

In several places and mostly in the hot-loop, we use this pattern. However, it completely breaks the control flow and can be error-prone.

To limit errors and because this pattern is usual, we prefer to use a local exception which will be used only inside the function. By this way, we enforce the fact that exception should not (and can not) be caught by something else than inside the function.

    let exception Break in

    ( try while !max >= 1 do
          if bl_count.(!max) != 0 then raise_notrace Break
        ; decr max done with Break -> () ) ;

This code above produce this assembly code:

.L105:
        pushq   %r14
        movq    %rsp, %r14
.L103:
        cmpq    $3, %rdi              // while !max >= 1
        jl      .L102
        movq    -4(%rbx,%rdi,4), %rsi // bl_count,(!max)
        cmpq    $1, %rsi              // bl_count.(!max) != 0
        je      .L104
        movq    %r14, %rsp
        popq    %r14
        ret                           // raise_notrace Break
.L104:
        addq    $-2, %rdi             // decr max
        movq    %rdi, 16(%rsp)
        jmp     .L103

Where the ret is the raise_notrace Break. A raise_notrace is needed, otherwise, you will see:

        movq    caml_backtrace_pos@GOTPCREL(%rip), %rbx
        xorq    %rdi, %rdi
        movl    %edi, (%rbx)
        call    caml_raise_exn@PLT

Instead the ret assembly code. Indeed, in this case, we need to store where we raised the exception.

Unrolling

When we showed the optimization done by gcc when the string is aligned, gcc did another optimization. Instead of setting the string byte per byte, it decides to update it 4 bytes per 4 bytes.

This kind of this optimization is an unroll and we did it in decompress. Indeed, when we reach the copy opcode emitted by the lz77 compressor, we want to blit length byte(s) from a source to the outputs flow. It can appear that this memcpy can be optimized to copy 4 bytes per 4 bytes – 4 bytes is generally a good idea where it's the size of an int32 and should fit under any architectures.

let blit src src_off dst dst_off =
  if dst_off – src_off < 4
  then slow_blit src src_off dst dst_off
  else
    let len0 = len land 3 in
    let len1 = len asr 2 in

    for i = 0 to len1 – 1
    do
      let i = i * 4 in
      let v = unsafe_get_uint32 src (src_off + i) in
      unsafe_set_uint32 dst (dst_off + i) v ;
    done ;

    for i = 0 to len0 – 1
    do
      let i = len1 * 4 + i in
      let v = unsafe_get_uint8 src (src_off + i) in
      unsafe_set_uint8 dst (dst_off + i) v ;
    done

In this code, at the beginning, we copy 4 bytes per 4 bytes and if len is not a multiple of 4, we start the trailing loop to copy byte per byte then. In this context, OCaml can unbox int32 and use registers. So this function does not deal with the heap, and by this way, with the garbage collector.

Results

In the end, we gained an extra 10Mb/s of inflation rate. The blit function is the most important function when it comes to inflating the window to an output flow. As the specialization on the min function, this is one of the biggest optimization on decompress.

hot-loop

A common design about decompression (but we can find it on hash implementation too), is the hot-loop. An hot-loop is mainly a loop on the most common operation in your process. In the context of decompress, the hot-loop is about a repeated translation from bits-sequence to byte(s) from the inputs flow to the outputs flow and the window.

The main idea behind the hot-loop is to initialize all information needed for the translation before to start the hot-loop. Then, it's mostly an imperative loop with a pattern-matching which corresponds to the current state of the global computation.

In OCaml, we can take this opportunity to use int ref (or nativeint ref), and then, they will be translated into registers (which is the fastest area to store something).

Another deal inside the hot-loop is to avoid any allocation – and it's why we talk about int or nativeint. Indeed, a more complex structure like an option will add a blocker to the garbage collection (a call to caml_call_gc).

Of course, this kind of design is completely wrong if we think in a functional way. However, this is the (biggest?) advantage of OCaml: hide this ugly/hacky part inside a functional interface.

In the API, we talked about a state which represents the inflation (or the deflation). At the beginning, the goal is to store into some references essentials values like the position into the inputs flow, bits available, dictionary, etc. Then, we launch the hot-loop and only at the end, we update the state.

So we keep the optimal design about inflation and the functional way outside the hot-loop.

caml_modify

One issue that we need to consider is the call to caml_modify. In fact, for a complex data-structure like an int array or a int option (so, other than an integer or a boolean or an immediate value), values can move to the major heap.

In this context, caml_modify is used to assign a new value into your mutable block. It is a bit slower than a simple assignment but needed to ensure pointer correspondence between minor heap and major heap.

With this OCaml code for example:

type t = { mutable v : int option }

let f t v = t.v <- v

We produce this assembly:

camlExample__f_1004:
        subq    $8, %rsp
        movq    %rax, %rdi
        movq    %rbx, %rsi
        call    caml_modify@PLT
        movq    $1, %rax
        addq    $8, %rsp
        ret

Where we see the call to caml_modify which will be take care about the assignment of v into t.v. This call is needed mostly because the type of t.v is not an immediate value like an integer. So, for many values in the inflator and the deflator, we mostly use integers.

Of course, at some points, we use int array and set them at some specific points of the inflator – where we inflated the dictionary. However, the impact of caml_modify is not very clear where it is commonly pretty fast.

Sometimes, however, it can be a real bottleneck in your computation and this depends on how long your values live in the heap. A little program (which is not very reproducible) can show that:

let t = Array.init (int_of_string Sys.argv.(1)) (fun _ -> Random.int 256)

let pr fmt = Format.printf fmt

type t0 = { mutable v : int option }
type t1 = { v : int option }

let f0 (t0 : t0) =
  for i = 0 to Array.length t – 1
  do let v = match t0.v, t.(i) with
             | Some _ as v, _ -> v
             | None, 5 -> Some i
             | None, _ -> None in
     t0.v <- v
  done; t0

let f1 (t1 : t1) =
  let t1 = ref t1 in
  for i = 0 to Array.length t – 1
  do let v = match !t1.v, t.(i) with
             | Some _ as v, _ -> v
             | None, 5 -> Some i
             | None, _ -> None in
     t1 := { v }
  done; !t1

let () =
  let t0 : t0 = { v= None } in
  let t1 : t1 = { v= None } in
  let time0 = Unix.gettimeofday () in
  ignore (f0 t0) ;
  let time1 = Unix.gettimeofday () in
  ignore (f1 t1) ;
  let time2 = Unix.gettimeofday () in

  pr "f0: %f ns\n%!" (time1 -. time0) ;
  pr "f1: %f ns\n%!" (time2 -. time1) ;

  ()

In our bare-metal server, if you launch the program with 1000, the f0 computation, even if it has caml_modify will be the fastest. However, if you launch the program with 1000000000, f1 will be the fastest.

$ ./a.out 1000
f0: 0.000006 ns
f1: 0.000015 ns
$ ./a.out 1000000000
f0: 7.931782 ns
f1: 5.719370 ns

About `decompress`

At the beginning, our choice was made to have, as @dbuenzli does, mutable structure to represent state. Then, @yallop did a big patch to update it to an immutable state and we won 9Mb/s on inflation.

However, the new version is more focused on the hot-loop and it is 3 times faster than before.

As we said, the deal about caml_modify is not clear and depends a lot about how long your data lives in the heap and how many times you want to update it. If we localize caml_modify only on few places, it should be fine. But it still is one of the most complex question about (macro?) optimization.

Smaller representation

We've discussed the impact that integer types can have on the use of immediate values. More generally, the choice of type to represent your values can have significant performance implications.

For example, a dictionary which associates a bits-sequence (an integer) to the length of it AND the byte, it can be represented by a: (int * int) array, or more idiomatically { len: int; byte: int; } array (which is structurally the same).

However, that means an allocation for each bytes to represent every bytes. Extraction of it will need an allocation if find : bits:int -> { len: int; byte: int; } is not inlined as we said. And about memory, the array can be really heavy in your heap.

At this point, we used spacetime to show how many blocks we allocated for a common inflation and we saw that we allocate a lot. The choice was made to use a smaller representation. Where len can not be upper than 15 according RFC 1951 and when byte can represent only 256 possibilities (and should fit under one byte), we can decide to merge them into one integer (which can have, at least, 31 bits).

let static_literal_tree = [| (8, 12); (8, 140); (8, 76); ... |]
let static_literal_tree = Array.map (fun (len, byte) -> (len lsl 8) lor byte) static_literal_tree

In the code above, we just translate the static dictionary (for a STATIC DEFLATE block) to a smaller representation where len will be the left part of the integer and byte will be the right part. Of course, it's depends on what you want to store.

Another point is readability. `cstruct-ppx` and `bitstring` can help you but decompress wants to depend only on OCaml.

Conclusion

We conclude with some closing advice about optimising your OCaml programs:

Optimization is specific to your task. The points highlighted in this article may not fit your particular problem, but they are intended to give you ideas. Our optimizations were only possible because we completely assimilated the ideas of zlib and had a clear vision of what we really needed to optimize (like blit).

As your first project, this article can not help you a lot to optimize your code where it's mostly about micro-optimization under a specific context (hot-loop). But it helps you to understand what is really done by the compiler – which is still really interesting.
Optimise only with respect to an oracle. All optimizations were done because we did a comparison point between the old implementation of decompress and zlib as oracles. Optimizations can change the semantics of your code and you should systematically take care at any step about expected behaviors. So it's a long run.
Use the predictability of the OCaml compiler to your advantage. For sure, the compiler does not optimize a lot your code – but it sill produce realistic programs if we think about performance. For many cases, you don't need to optimize your OCaml code. And the good point is about expected behavior.

The mind-link between the OCaml and the assembly exists (much more than the C and the assembly sometimes where we let the C compiler to optimize the code). The cool fact is to keep a mental-model about what is going on on your code easily without to be afraid by what the compiler can produce. And, in some critical parts like eqaf, it's really needed.

We have not discussed benchmarking, which is another hard issue: who should you compare with? where? how? For example, a global comparison between zlib and decompress is not very relevant in many ways – especially because of the garbage collector. This could be another article!

Finally, all of these optimizations should be done by flambda; the difference between compiling decompress with or without flambda is not very big. We optimized decompress by hand mostly to keep compatibility with OCaml (since flambda needs another switch) and, in this way, to gain an understanding of flambda optimizations so that we can use it effectively!

Hide

On complete ordered fields — Andrej Bauer, Sep 08, 2019

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

A complete ordered field is archimedean.
Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in …

Joel Hamkins advertised the following theorem on Twitter:

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

A complete ordered field is archimedean.
Using the fact that the rationals are dense in an archimedean field, we construct an isomorphism between any two complete ordered fields.

The second step is constructive, but the first one is proved using excluded middle, as follows. Suppose $F$ is a complete ordered field. If $b \in F$ is an upper bound for the natural numbers, construed as a subset of $F$, then so $b - 1$, but then no element of $F$ can be the least upper bound of $\mathbb{N}$. By excluded middle, above every $x \in F$ there is $n \in \mathbb{N}$.

So I asked myself and the constructive news mailing list what the constructive status of the theorem is. But something was amiss, as Fred Richman immediately asked me to provide an example of a complete ordered field. Why would he do that, don't we have the MacNeille reals? After agreeing on definitions, Toby Bartels gave the answer, which I am taking the liberty to adapt a bit and present here. I am probably just reinventing the wheel, so if someone knows an original reference, please provide it in the comments.

The theorem holds constructively, but for a bizarre reason: if there exists a complete ordered field, then the law of excluded middle holds, and the standard proof is valid!

As there are many constructive versions of order and completeness, let me spell out the definitions that are well adapted to the oddities of constructive mathematics. In classical logic these are all equivalent to the usual ones. Having to disentangle definitions when passing to constructive mathematics is a bit like learning how to be careful when passing from commutative to non-commutative algebra.

A partial order $\leq$ on a set $P$ is a reflexive, transitive and antisymmetric relation on $P$.

We are interested in linearly ordered fields, but constructively we need to take care, as the usual linearity, $x \leq y \lor y \leq x$, is quite difficult to satisfy, and may fail for reals.

A strict order on a set $P$ is a relation $<$ which is:

irreflexive: $\lnot (x < x)$,
tight: $\lnot (x < y \lor y < x) \Rightarrow x = y$,
weakly linear: $x < y \Rightarrow x < z \lor z < y$

The associated partial order is defined by $x \leq y \Leftrightarrow \lnot (y < x)$. The reflexivity, antisymmetry and transitivity of $\leq$ follow respectively from irreflexivity, tightness, and weak linearity of $<$.

Next, an element $x \in P$ is an upper bound for $S \subseteq P$ when $y \leq x$ for all $y \in P$. An element $x \in P$ is the supremum of $S \subseteq P$ if it is an upper bound for $S$, and for every $y < x$ there exists $z \in S$ such that $y < z$. A poset $P$ is (Dedekind-MacNeille) complete when every inhabited bounded subset has a supremum (for the classically trained, $S \subseteq P$ is inhabited when there exists $x \in S$, and this is not the same as $S \neq \emptyset$).

A basic exercise is to give a non-trivial complete order, i.e., a strict order $<$ whose associated partial order $\leq$ is complete.

Theorem: If there exists a non-trivial complete order then excluded middle holds.

Proof. Suppose $<$ is a strict order on a set $P$ whose associated order $\leq$ is complete, and there exist $a, b \in P$ such that $a < b$. Let $\phi$ be any proposition. Consider the set $S = \lbrace x \in P \mid x = a \lor (\phi \land x = b)\rbrace$. Observe that $\phi$ is equivalent to $b \in S$. Because $a \in S \subseteq \lbrace a, b\rbrace$, the set $S$ is inhabited and bounded, so let $s$ be its supremum. We know that $a < s$ or $s < b$, from which we can decide $\phi$:

If $a < s$ then $b \in S$: indeed, there exists $c \in S$ such that $a < c$, but then $c = b$. In this case $\phi$ holds.
If $s < b$ then $\lnot(b \in S)$: if we had $b \in S$ then $S = \lbrace a, b \rbrace$ and $b = s < b$, which is impossible. In this case $\lnot\phi$. $\Box$

This immediately gives us the desired theorem.

Theorem (constructive): All complete ordered fields are isomorphic.

Proof. The definition of a complete ordered field requires $0 < 1$, therefore excluded middle holds. Now proceed with the usual classical proof. $\Box$

This is very odd, as I always thought that the MacNeille reals form a MacNeille complete ordered field. Recall that a MacNeille real is a pair $(L, U)$ of subsets of $\mathbb{Q}$ such that:

$U$ is the set of upper bounds of $L$: $u \in U$ if, and only if, $\ell \leq u$ for all $\ell \in L$,
$L$ is the set of lower bounds of $U$: $\ell \in L$ if, and only if, $\ell \leq u$ for all $u \in U$,
$L$ and $U$ are inhabited.

Furthermore, the MacNeille reals are complete, as they are just the MacNeille completion of the rationals. We may define a strict order on them by stipulating that, for $x = (L_x, U_x)$ and $y = (L_y, U_y)$, $$x < y \iff \exists q \in U_x . \exists r \in L_y \,.\, q < r.$$ According to Peter Johnstone (Sketches of an Elephant, D4.7), the MacNeille reals form a commutative unital ring in which $x$ is invertible if, and only if, $x < 0 \lor x > 0$. So apparently, the weak linearity of the strict order is problematic.

What if we relax completeness? Two standard notions of completeness are:

An ordered field $F$ is Cauchy-complete if every Cauchy sequence has a limit in $F$.
An ordered field $F$ is Dedekind-complete if every Dedekind cut determines an element of $F$.

It is easy enough to find non-isomorphic Cauchy-complete fields. Order the field $\mathbb{Q}(x)$ of rational functions with rational coefficients by stipulating that it extends the order of $\mathbb{Q}$ and that $q < x$ for all $q \in \mathbb{Q}$. The Cauchy-completion of $\mathbb{Q}(x)$ is a Cauchy complete field which is not isomorphic to $\mathbb{Q}$. Caveat: I am speaking off the top of my head, do not trust this paragraph! (Or any other for that matter.)

Regarding Dedekind completeness, it is important constructively that we take two-sided Dedekind cuts, i.e., pairs $(L, U)$ of subsets of $F$ such that

$L$ is lower-rounded: $q \in L \iff \exists r \in L . q < r$,
$U$ is upper-rounded: $r \in U \iff \exists q \in U . q < r$,
the cut is bounded: $L$ and $U$ are inhabited,
the cut is disjoint: $L \cap U = \emptyset$,
the cut is located: if $q < r$ then $L \in q$ or $r \in U$.

Dedekind completeness states that for every Dedekind cut $(L, U)$ in $F$ there exists a unique $x \in F$ such that $L = \lbrace y \in F \mid y < x\rbrace$ and $U = \lbrace y \in F \mid x < y\rbrace$. Constructively this is a weaker form of completeness than the Dedekind-MacNeille one, but classically they coincide. Thus we cannot hope to exhibit constructively two non-isomorphic Dedekind-complete ordered fields (because constructive results are also classically valid). But perhaps there is a model of constructive mathematics where such strange fields exist. Does anyone know of one?

Hide

An introduction to fuzzing OCaml with AFL, Crowbar and Bun — Tarides (Nathan Rebours), Sep 04, 2019

American Fuzzy Lop or AFL is a fuzzer: a program that tries to find bugs in other programs by sending them various auto-generated inputs. This article covers the basics of AFL and shows an example of fuzzing a parser written in OCaml. It also introduces two extensions: the Crowbar library which can be used to fuzz any kind of OCaml program or function and the Bun tool for integrating fuzzing into your CI.

All of the examples given in this article are available on GitHub at ocaml-afl-examples. Th…

All of the examples given in this article are available on GitHub at ocaml-afl-examples. The README contains all the information you need to understand, build and fuzz them yourself.

What is AFL?

AFL actually isn't just a fuzzer but a set of tools. What makes it so good is that it doesn't just blindly send random input to your program hoping for it to crash; it inspects the execution paths of the program and uses that information to figure out which mutations to apply to the previous inputs to trigger new execution paths. This approach allows for much more efficient and reliable fuzzing (as it will try to maximize coverage) but requires the binaries to be instrumented so the execution can be monitored.

AFL provides wrappers for the common C compilers that you can use to produce the instrumented binaries along with the CLI fuzzing client: afl-fuzz.

afl-fuzz is straight-forward to use. It takes an input directory containing a few initial valid inputs to your program, an output directory and the instrumented binary. It will then repeatedly mutate the inputs and feed them to the program, registering the ones that lead to crashes or hangs in the output directory.

Because it works in such a way, it makes it very easy to fuzz a parser.

To fuzz a parse.exe binary, that takes a file as its first command-line argument and parses it, you can invoke afl-fuzz in the following way:

$ afl-fuzz -i inputs/ -o findings/ /path/to/parse.exe @@

The findings/ directory is where afl-fuzz will write the crashes it finds, it will create it for you if it doesn't exist. The inputs/ directory contains one or more valid input files for your program. By valid we mean "that don't crash your program". Finally the @@ part tells afl-fuzz where on the command line the input file should be passed to your program, in our case, as the first argument.

Note that it is possible to supply afl-fuzz with more detail about how to invoke your program. If you need to pass it command-line options for instance, you can run it as:

$ afl-fuzz -i inputs/ -o findings/ -- /path/to/parse.exe --option=value @@

If you wish to fuzz a program that takes its input from standard input, you can also do that by removing the @@ from the afl-fuzz invocation.

Once afl-fuzz starts, it will draw a fancy looking table on the standard output to keep you updated about its progress. From there, you'll mostly be interested in is the top right corner which contains the number of crashes and hangs it has found so far:

Example output from afl-fuzz

You might need to change some of your CPU settings to achieve better performance while fuzzing. afl-fuzz's output will tell you if that's the case and guide you through the steps required to make that happen.

Using AFL to fuzz an OCaml parser

First of all, if you want to fuzz an OCaml program with AFL you'll need to produce an instrumented binary. afl-fuzz has an option to work with regular binaries but you'd lose a lot of what makes it efficient. To instrument your binary you can simply install a +afl opam switch and build your executable from there. AFL compiler variants are available from OCaml 4.05.0 onwards. To install such a switch you can run:

$ opam switch create fuzzing-switch 4.07.1+afl

If your program already parses the standard input or a file given to it via the command line, you can simply build the executable from your +afl switch and adapt the above examples. If it doesn't, it's still easy to fuzz any parsing function.

Imagine we have a simple-parser library which exposes the following parse_int function:

val parse_int: string -> (int, [> `Msg of string]) result
(** Parse the given string as an int or return [Error (`Msg _)].
    Does not raise, usually... *)

We want to use AFL to make sure our function is robust and won't crash when receiving unexpected inputs. As you can see the function returns a result and isn't supposed to raise exceptions. We want to make sure that's true.

To find crashes, AFL traps the signals sent by your program. That means that it will consider uncaught OCaml exceptions as crashes. That's good because it makes it really simple to write a fuzz_me.ml executable that fits what afl-fuzz expects:

let () =
  let file = Sys.argv.(1) in
  let ic = open_in file in
  let length = in_channel_length ic in
  let content = really_input_string ic length in
  close_in ic;
  ignore (Simple_parser.parse_int content)

We have to provide example inputs to AFL so we can write a valid file to the inputs/ directory containing 123 and an invalid file containing not an int. Both should parse without crashing and make good starting point for AFL as they should trigger different execution paths.

Because we want to make sure AFL does find crashes we can try to hide a bug in our function:

let parse_int s =
  match List.init (String.length s) (String.get s) with
  | ['a'; 'b'; 'c'] -> failwith "secret crash"
  | _ -> (
      match int_of_string_opt s with
      | None -> Error (`Msg (Printf.sprintf "Not an int: %S" s))
      | Some i -> Ok i)

Now we just have to build our native binary from the right switch and let afl-fuzz do the rest:

$ afl-fuzz -i inputs/ -o findings/ ./fuzz_me.exe @@

It should find that the abc input leads to a crash rather quickly. Once it does, you'll see it in the top right corner of its output as shown in the picture from the previous section.

At this point you can interrupt afl-fuzz and have a look at the content of the findings/crashes:

$ ls findings/crashes/
id:000000,sig:06,src:000111,op:havoc,rep:16  README.txt

As you can see it contains a README.txt which will give you some details about the afl-fuzz invocation used to find the crashes and how to reproduce them in the folder and a file of the form id:...,sig:...,src:...,op:...,rep:... per crash it found. Here there's just one:

$ cat findings/crashes/id:000000,sig:06,src:000111,op:havoc,rep:16
abc

As expected it contains our special input that triggers our secret crash. We can rerun the program with that input ourselves to make sure it does trigger it:

$ ./fuzz_me.exe findings/crashes/id:000000,sig:06,src:000111,op:havoc,rep:16
Fatal error: exception Failure("secret crash")

No surprise here, it does trigger our uncaught exception and crashes shamefully.

Using Crowbar and AFL for property-based testing

This works well but only being able to fuzz parsers is quite a limitation. That's where Crowbar comes into play.

Crowbar is a property-based testing framework. It's much like Haskell's QuickCheck. To test a given function, you define how its arguments are shaped, a set of properties the result should satisfy and it will make sure they hold with any combinations of randomly generated arguments. Let's clarify that with an example.

I wrote a library called Awesome_list and I want to test its sort function:

val sort: int list -> int list
(** Sorts the given list of integers. Result list is sorted in increasing
    order, most of the time... *)

I want to make sure it really works so I'm going to use Crowbar to generate a whole lot of lists of integers and verify that when I sort them with Awesome_list.sort the result is, well... sorted.

We'll write our tests in a fuzz_me.ml file. First we need to tell Crowbar how to generate arguments for our function. It exposes some combinators to help you do that:

let int_list = Crowbar.(list (range 10))

Here we're telling Crowbar to generate lists of any size, containing integers ranging from 0 to 10. Crowbar also exposes more complex and custom generator combinators so don't worry, you can use it to build more complex arguments.

Now we need to define our property. Once again it's pretty simple, we just want the output to be sorted:

let is_sorted l =
  let rec is_sorted = function
    | [] | [_] -> true
    | hd::(hd'::_ as tl) -> hd <= hd' && is_sorted tl
  in
  Crowbar.check (is_sorted l)

All that's left to do now is to register our test:

let () =
  Crowbar.add_test ~name:"Awesome_list.sort" [int_list]
      (fun l -> is_sorted (Awesome_list.sort l))

and to compile that fuzz_me.ml file to a binary. Crowbar will take care of the magic.

We can run that binary in "Quickcheck" mode where it will either try a certain amount of random inputs or keep trying until one of the properties breaks depending on the command-line options we pass it. What we're interested in here is its less common "AFL" mode. Crowbar made it so our executable can be used with afl-fuzz just like that:

$ afl-fuzz -i inputs -o findings -- ./fuzz_me.exe @@

What will happen then is that our fuzz_me.exe binary will read the inputs provided by afl-fuzz and use it to determine which test to run and how to generate the arguments to pass to our function. If the properties are satisfied, the binary will exit normally; if they aren't, it will make sure that afl-fuzz interprets that as a crash by raising an exception.

A nice side-effect of Crowbar's approach is that afl-fuzz will still be able to pick up crashes. For instance, if we implement Awesome_list.sort as:

let sort = function
  | [1; 2; 3] -> failwith "secret crash"
  | [4; 5; 6] -> [6; 5; 4]
  | l -> List.sort Pervasives.compare l

and use AFL and Crowbar to fuzz-test our function, it will find two crashes: one for the input [1; 2; 3] which triggers a crash and one for [4; 5; 6] for which the is_sorted property won't hold.

The content of the input files found by afl-fuzz itself won't be of much help as it needs to be interpreted by Crowbar to build the arguments that were passed to the function to trigger the bug. We can invoke the fuzz_me.exe binary ourselves on one of the files in findings/crashes and the Crowbar binary will replay the test and give us some more helpful information about what exactly is going on:

$ ./fuzz_me.exe findings/crashes/id\:000000\,sig\:06\,src\:000011\,op\:flip1\,pos\:5 
Awesome_list.sort: ....
Awesome_list.sort: FAIL

When given the input:

    [1; 2; 3]
    
the test threw an exception:

    Failure("secret crash")
    Raised at file "stdlib.ml", line 33, characters 17-33
    Called from file "awesome-list/fuzz/fuzz_me.ml", line 11, characters 78-99
    Called from file "src/crowbar.ml", line 264, characters 16-19
    
Fatal error: exception Crowbar.TestFailure
$ ./fuzz_me.exe findings/crashes/id\:000001\,sig\:06\,src\:000027\,op\:arith16\,pos\:5\,val\:+7 
Awesome_list.sort: ....
Awesome_list.sort: FAIL

When given the input:

    [4; 5; 6]
    
the test failed:

    check false
    
Fatal error: exception Crowbar.TestFailure

We can see the actual inputs as well as distinguish the one that broke the invariant from the one that triggered a crash.

Using `bun` to run fuzz testing in CI

While AFL and Crowbar provide no guarantees they can give you confidence that your implementation is not broken. Now that you know how to use them, a natural follow-up is to want to run fuzz tests in your CI to enforce that level of confidence.

Problem is, AFL isn't very CI friendly. First it has this refreshing output that isn't going to look great on your travis builds output and it doesn't tell you much besides that it could or couldn't find crashes or invariant infrigements

Hopefully, like most problems, this one has a solution: `bun`. bun is a CLI wrapper around afl-fuzz, written in OCaml, that helps you get the best out of AFL effortlessly. It mostly does two things:

The first is that it will run several afl-fuzz processes in parallel (one per core by default). afl-fuzz starts with a bunch of deterministic steps. In my experience, using parallel processes during this phase rarely proved very useful as they tend to find the same bugs or slight variations of those bugs. It only achieves its full potential in the second phase of fuzzing.

The second thing, which is the one we're the most interested in, is that bun provides a useful and CI-friendly summary of what's going on with all the fuzzing processes so far. When one of them finds a crash, it will stop all processes and pretty-print all of the bug-triggering inputs to help you reproduce and debug them locally. See an example bun output after a crash was found:

Crashes found! Take a look; copy/paste to save for reproduction:
1432    echo JXJpaWl0IA== | base64 -d > crash_0.$(date -u +%s)
1433    echo NXJhkV8QAA== | base64 -d > crash_1.$(date -u +%s)
1434    echo J3Jh//9qdGFiYmkg | base64 -d > crash_2.$(date -u +%s)
1435    09:35.32:[ERROR]All fuzzers finished, but some crashes were found!

Using bun is very similar to using afl-fuzz. Going back to our first parser example, we can fuzz it with bun like this:

$ bun --input inputs/ --output findings/ /path/to/parse.exe

You'll note that you don't need to provide the @@ anymore. bun assumes that it should pass the input as the first argument of your to-be-fuzzed binary.

bun also comes with an alternative no-kill mode which lets all the fuzzers run indefinitely instead of terminating them whenever a crash is discovered. It will regularly keep you updated on the number of crashes discovered so far and when terminated will pretty-print each of them just like it does in regular mode.

This mode can be convenient if you suspect your implementation may contain a lot of bugs and you don't want to go through the whole process of fuzz testing it to only find a single bug.

You can use it in CI by running bun --no-kill via timeout. For instance:

timeout --preserve-status 60m bun --no-kill --input inputs --output findings ./fuzz_me.exe

will fuzz fuzz_me.exe for an hour no matter what happens. When timeout terminates bun, it will provide you with a handful of bugs to fix!

Final words

I really want to encourage you to use those tools and fuzzing in general. Crowbar and bun are fairly new so you will probably encounter bugs or find that it lacks a feature you want but combined with AFL they make for very nice tools to effectively test critical components of your OCaml code base or infrastructure and detect newly-introduced bugs. They are already used accross the MirageOS ecosystem where it has been used to fuzz the TCP/IP stack mirage-tcpip and the DHCP implementation charrua thanks to somerandompacket. You can consult Crowbar's hall of fame to find out about bugs uncovered by this approach.

I also encourage anyone interested to join us in using this promising toolchain, report those bugs, contribute those extra features and help the community build more robust software.

Finally if you wish to learn more about how to efficienly use fuzzing for testing I recommend the excellent Write Fuzzable Code article by John Regehr.

Hide

What is algebraic about algebraic effects? — Andrej Bauer, Sep 02, 2019

Published as arXiv:1807.05923.

Abstract: This note recapitulates and expands the contents of a tutorial on the mathematical theory of algebraic effects and handlers which I gave at the Dagstuhl seminar 18172 "Algebraic effect handlers go mainstream". It is targeted roughly at the level of a doctoral student with some amount of mathematical training, or at anyone already familiar with algebraic effects and handlers as programming concepts who would like to know what they have to do with algebra.…

The blog moved from Wordpress to Jekyll — Andrej Bauer, Sep 02, 2019

You may have noticed that lately I have had trouble with the blog. It was dying periodically because the backend database kept crashing. It was high time I moved away from Wordpress anyway, so I bit the bullet and ported the blog.

All in all, it was a typical system administration experience: lots of installing Ruby and Node.js packages, figuring out which of several equivalent tools actually is worth using, dealing with scarce and obsolete documentation (a blog post is not a good substitute …

OCamlPro’s compiler team work update — OCamlPro, Aug 30, 2019

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

A lot of work has been done towards a new framework for optimizations in the compiler, called Flambda2, aiming at solving the shortcomings that became apparent in the Flambda optimization framework (see below for more details). While that work is in progress, the team also worked on some more short-term improvements, notably on the current Flambda optimization framework, a…

The OCaml compiler team at OCamlPro is happy to present some of the work recently done jointly with JaneStreet’s team.

This work is funded by JaneStreet

Short-term improvements

Recursive values compilation

OCaml supports quite a large range of recursive definitions. In addition to recursive (and mutually-recursive) functions, one can also define regular values recursively, as for the infinite list let rec l = 0 :: l.

Not all recursive constructions are allowed, of course. For instance, the definition let rec x = x is rejected because there is no way to actually build a value that would behave correctly.

The basic rule for deciding whether a definition is allowed or not is made under the assumption that recursive values (except for functions, mostly) are compiled by first allocating space in the heap for the recursive values, binding the recursively defined variables to the allocated (but not yet initialized) values. The defining expressions are then evaluated, yielding new values (that can contain references the non-initialized values). Finally, the fields of these new values are copied one-by-one into the corresponding fields of the initial values.

For this approach to work, some restrictions need to apply:

the compiler needs to be able to compute the size of the values beforehand (these values must be allocated values, in order to avoid defining an integer recursively),
and since during the evaluation of the defining expressions their fields are not valid, one cannot write any code that may read these fields, like pattern-matching on the value, or passing the value to some function (or storing it in a mutable field of some record).

All of those restrictions have recently been reworked and formalized based on work from Alban Reynaud during an internship at Inria, reviewed and completed by Gabriel Scherer and Jeremy Yallop.

Unfortunately, this work only covers checking whether the recursive definitions are allowed or not; actual compilation is done later in the compiler, in one place for bytecode and another for native code, and these pieces of code have not been linked with the new check so there have been a few cases where the check allowed code that wasn’t actually compiled correctly.

Since we didn’t want to deal with it directly in our new version of Flambda, we had started working on a patch to move the compilation of recursive values up in the compilation pipeline, before the split between bytecode and native code. After some amount of hacking (we discovered that compilation of classes creates recursive value bindings that would not pass the earlier recursive check…), we have a patch that is mostly ready for review and will soon start engaging with the rest of the compiler team with the aim of integrating it into the compiler.

Separate compilation of recursive modules, compilation units as functors

Some OCaml developers like to encapsulate each type definition in its own module, with an interface that can expose the needed types and functions, while abstracting away as much of the actual implementation as possible. It is then common to have each of these modules in its own file, to simplify management and avoid unseemly big files.

However, this breaks down when one needs to define several types that depend on each other. The usual solutions are either to use recursive modules, which have the drawback of requiring all the modules to be in the same compilation unit, leading to very big files (we have seen a real case of a more than 10,000-lines file), or make each module parametric in the other modules, translating them into functors, and then instantiate all the functors when building the outwards-facing interface.

To address these issues, we have been working on two main patches to improve the life of developers facing these problems.

The first one allows compiling several different files as mutually recursive modules, reusing the approach used to compile regular recursive modules. In practice, this will allow developers using recursive modules extensively to properly separate not only the different modules from each other, but also the implementation and interfaces into a .ml and .mli files. This would of course need some additional support from the different build tools, but we’re confident we can get at least dune to support the feature.

The second one allows compiling a single compilation unit as a functor instead of a regular module. The arguments of the functor would be specified on the command line, their signature taken from their corresponding interface file. This can be useful not only to break recursive dependencies, like the previous patch (though in a different way), but also to help developers relying on multiple implementations of a same .mli interface functorize their code with minimal effort.

These two improvements will also benefit packs, whereas recursive compilation units could be packed in a single module and packs could be functorized themselves.

Small improvements to Flambda

We are still committed to maintain the Flambda part of the compiler. Few bugs have been found, so we concentrate our efforts on small features that either yield overall performance gains or allow naive code patterns to be compiled as efficiently as their equivalent but hand-optimized versions.

As an example, one optimization that we should be able to submit soon looks for cases where an immutable block is allocated but an immutable block with the same exact fields and tag already exists.

This can be demonstrated with the following example:

let result_bind f = function
  | Ok x -> f x
  | Error e -> Error e

The usual way to avoid the extra allocation of Error e is to write the clause as | (Error e) as r -> r. With this new patch, the redundant allocation will be detected and removed automatically! This can be even more interesting with inlining:

let my_f x =
  if (* some condition *)
  then Ok x
  else (* something else *)

let _ =
  (* ... *)
  let r = result_bind my_f (* some argument *) in
  (* ... *)

In this example, inlining result_bind then my_f can match the allocation Ok x in my_f with the pattern matching in result_bind. This removes an allocation that would be very hard to remove otherwise. We expect these patterns to occur quite often with some programming styles relying on a great deal of abstraction and small independent functions.

Flambda 2.0

We are building on the work done for Flambda and the experience of its users to develop Flambda 2.0, the next optimization framework.

Our goal is to build a framework for analyzing the costs and benefits of code transformations. The framework focuses on reducing the runtime cost of abstractions and removing as many short-lived allocations as possible.

The aim of Flambda 2.0 is roughly the same as the original Flambda. So why did we decide to write a new framework instead of patching the existing one? Several points led us to this decision.

An invariant on the representation of closures that ensured that every closure had a unique identifier, which was convenient for a number of reasons, turned out to be quite expensive to maintain and prevented some optimizations.
The internal representation of Flambda terms included too many different cases that were either redundant or not relevant to the optimizations we were interested in, making a lot of code more complicated than necessary.
The ANF-like representation we used was not perfect. We wanted an easier way to do control flow optimizations, which led us to choose a CPS-like representation for Flambda 2.0.
Finally, the original Flambda was thought of as an alternative to the closure conversion and inlining algorithms performed by the Closure module of the compiler, translating from the Lambda representation to Clambda. However, a number of optimizations (most importantly unboxing) are done during the next phase of compilation, Cmmgen, which translates to the Cmm representation. The original Flambda had trouble to estimate correctly which optimizations would trigger and what would their benefit be. It may be noted that correctly estimating benefit is a key in Flambda’s algorithms, and we know of a number of cases where Flambda is not as good as it could be because it couldn’t predict the unboxing opportunities that inlining would have allowed. Flambda 2.0 will go from Lambda to Cmm, and will handle all transformations done in both Closure and Cmmgen in a single framework.

These improvements are still very much a work in progress. We have not reached the point where other developers can try out the new framework on their codebases yet.

This does not mean there are no news to enjoy before our efforts show on the mainstream compiler! While working on Flambda 2.0, we did deploy a number of patches on the compiler both before and after the Flambda stage. We proposed all the changes independant enough to be proposed on their own. Some of these fixes have been merged already. Others are still under discussion and some, like the recursive values patch mentioned above, are still waiting for cleanup or documentation before submission.

Hide

What the interns have wrought, 2019 edition — Jane Street, Aug 30, 2019

Jane Street’s intern program yet again is coming to an end, which is a nice opportunity to look back over the summer and see what they’ve accomplished.

Decompress: The New Decompress API — Tarides (Romain Calascibetta), Aug 26, 2019

RFC 1951 is one of the most used standards. Indeed, when you launch your Linux kernel, it inflates itself according zlib standard, a superset of RFC 1951. Being a widely-used standard, we decided to produce an OCaml implementation. In the process, we learned many lessons about developing OCaml where we would normally use C. So, we are glad to present `decompress`.

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress …

One of the many users of RFC 1951 is Git, which uses it to pack data objects into a PACK file. At the request of @samoht, decompress appeared some years ago as a Mirage-compatible replacement for zlib to be used for compiling a MirageOS unikernel with ocaml-git. Today, this little project passes a major release with substantial improvements in several domains.

decompress provides an API for inflating and deflating flows[1]. The main goal is to provide a platform-agnostic library: one which may be compiled on any platform, including JavaScript. We surely cannot be faster than C implementations like zstd or lz4, but we can play some optimisation tricks to help bridge the gap. Additionally, OCaml can protect the user against lot of bugs via the type-system and the runtime too (e.g. using array bounds checking). `ocaml-tls` was implemented partly in response to the famous failure of openssl; a vulnerability which could not exist in OCaml.

[1]: A flow, in MirageOS land, is an abstraction which wants to receive and/or transmit something under a standard. So it's usual to say a TLS-flow for example.

API design

The API should be the most difficult part of designing a library - it reveals what we can do and how we should do it. In this way, an API should:

constrain the user to avoid security issues; too much freedom can be a bad thing. As an example, consider the Hashtbl.create function, which allows the user to pass ~random:false to select a fixed hash function. The resulting hashtable suffers deterministic key collisions, which can be exploited by an attacker.

An example of good security-awareness in API design can be seen in digestif, which provided an unsafe_compare instead of the common compare function (before eqaf.0.5). In this way, it enforced the user to create an alias of it if they want to use a hash in a Map – however, by this action, they should know that they are not protected against a timing-attack.
allow some degrees of freedom to fit within many environments; a constrained API cannot support a hostile context. For example, when compiling to an ESP32 target, even small details such as the length of a stream input buffer must be user-definable. When deploying to a server, memory consumption should be deterministic.

Of course, this is made difficult when too much freedom will enable misuse of the API – an example is dune which wants consciously to limit the user about what they can do with it.
imply an optimal design of how to use it. Possibilities should serve the user, but these can make the API harder to understand; this is why documentation is important. Your API should tell your users how it wants to be treated.

A dbuenzli API

From our experiences with protocol/format, one design stands out: the dbuenzli API. If you look into some famous libraries in the OCaml eco-system, you probably know uutf, jsonm or xmlm. All of these libraries provide the same API for computing a Unicode/JSON/XML flow – of course, the details are not the same.

From a MirageOS perspective, even if they use the in_channel/out_channel abstraction rather than a Mirage flow, these libraries are system-agnostic since they let the user to choose input and output buffers. Most importantly, they don't use the standard OCaml Unix module, which cannot be used in a unikernel.

The APIs are pretty consistent and try to do their best-effort[2] of decoding. The design has a type state which represents the current system status; the user passes this to decode/encode to carry out the processing. Of course, these functions have a side-effect on the state internally, but this is hidden from the user. One advantage of including states in a design is that the underlying implementation is very amenable to compiler optimisations (e.g. tail-call optimisation). Internally, of course, we have a porcelain[3] implementation where any details can have an rational explanation.

In the beginning, decompress wanted to follow the same interface without the mutability (a choice about performances) and it did. Then, the hard test was to use it in a bigger project; in this case, ocaml-git. An iterative process was used to determine what was really needed, what we should not provide (like special cases) and what we should provide to reach an uniform API that is not too difficult to understand.

From this experience, we finalised the initial decompress API and it did not change significantly for 4 versions (2 years).

[2]: best-effort means an user control on the error branch where we don't leak exception (or more generally, any interrupts)

[3]: porcelain means implicit invariants held in the mind of the programmer (or the assertions/comments).

The new `decompress` API

The new decompress keeps the same inflation logic, but drastically changes the deflator to make the flush operation clearer. For many purposes, people don't want to hand-craft their compressed flows – they just want of_string/to_string functions. However, in some contexts (like a PNG encoder/decoder), the user should be able to play with decompress in detail (OpenPGP needs this too in RFC 4880).

The Zlib format

Both decompress and zlib use Huffman coding, an algorithm for building a dictionary of variable-length codewords for a given set of symbols (in this case, bytes). The most common byte is assigned the shortest bit sequence; less common bytes are assigned longer codewords. Using this dictionary, we just translate each byte into its codeword and we should achieve a good compression ratio. Of course, there are other details, such as the fact that all Huffman codes are prefix-free. The compression can be taken further with the LZ77 algorithm.

The zlib format, a superset of the RFC 1951 format, is easy to understand. We will only consider the RFC 1951 format, since zlib adds only minor details (such as checksums). It consists of several blocks: DEFLATE blocks, each with a little header, and the contents. There are 3 kinds of DEFLATE blocks:

a FLAT block; no compression, just a blit from inputs to the current block.
a FIXED block; compressed using a pre-computed Huffman code.
a DYNAMIC block; compressed using a user-specified Huffman code.

The FIXED block uses a Huffman dictionary that is computed when the OCaml runtime is initialised. DYNAMIC blocks use dictionaries specified by the user, and so these must be transmitted alongside the data (after being compressed with another Huffman code!). The inflator decompresses this DYNAMIC dictionary and uses it to do the reverse translation from bit sequences to bytes.

Inflator

The design of the inflator did not change a lot from the last version of decompress. Indeed, it's about to take an input, compute it and return an output like a flow. Of course, the error case can be reached.

So the API is pretty-easy:

val decode : decoder -> [ `Await | `Flush | `End | `Malformed of string ]

As you can see, we have 4 cases: one which expects more inputs (Await), the second which asks to the user to flush internal buffer (Flush), the End case when we reach the end of the flow and the Malformed case when we encounter an error.

For each case, the user can do several operations. Of course, about the Await case, they can refill the contents with an other inputs buffer with:

val src : decoder -> bigstring -> off:int -> len:int -> unit

This function provides the decoder a new input with len bytes to read starting at off in the given bigstring.

In the Flush case, the user wants some information like how many bytes are available in the current output buffer. Then, we should provide an action to flush this output buffer. In the end, this output buffer should be given by the user (how many bytes they want to allocate to store outputs flow).

type src = [ `Channel of in_channel | `Manual | `String of string ]

val dst_rem : decoder -> int
val flush : decoder -> unit
val decoder : src -> o:bigstring -> w:bigstring -> decoder

The last function, decoder, is the most interesting. It lets the user, at the beginning, choose the context in which they want to inflate inputs. So they choose:

src, where come from inputs flow
o, output buffer
w, window buffer

o will be used to store inflated outputs, dst_rem will give to us how many bytes inflator stored in o and flush will just set decoder to be able to recompute the flow.

w is needed for lz77 compression. However, as we said, we let the user give us this intermediate buffer. The idea behind that is to let the user prepare an inflation. For example, in ocaml-git, instead of allocating w systematically when we want to decompress a Git object, we allocate w one time per threads and all are able to use it and re-use it. In this way, we avoid systematic allocations (and allocate only once time) which can have a serious impact about performances.

The design is pretty close to one idea, a description step by the decoder function and a real computation loop with the decode function. The idea is to prepare the inflation with some information (like w and o) before the main (and the most expensive) computation. Internally we do that too (but it's mostly about a macro-optimization).

It's the purpose of OCaml in general, be able to have a powerful way to describe something (with constraints). In our case, we are very limited to what we need to describe. But, in others libraries like angstrom, the description step is huge (describe the parser according to the BNF) and then, we use it to the main computation, in the case of angstrom, the parsing (another example is [cmdliner][cmdliner]).

This is why decoder can be considered as the main function where decode can be wrapped under a stream.

Deflator

The deflator is a new (complex) deal. Indeed, behind it we have two concepts:

the encoder (according to RFC 1951)
the compressor

For this new version of decompress, we decide to separate these concepts where one question leads all: how to put my compression algorithm? (instead to use LZ77).

In fact, if you are interested in compression, several algorithms exist and, in some context, it's preferable to use lzwa for example or rabin's fingerprint (with duff), etc.

Functor

The first idea was to provide a functor which expects an implementation of the compression algorithm. However, the indirection of a functor comes with (big) performance cost. Consider the following functor example:

module type S = sig
  type t
  val add : t -> t -> t
  val one : t
end

module Make (S : S) = struct let succ x = S.add x S.one end

include Make (struct
  type t = int
  let add a b = a + b
  let one = 1
end)

let f x = succ x

Currently, with OCaml 4.07.1, the f function will be a caml_apply2. We might wish for a simple _inlining_ optimisation, allowing f to become an addq instruction (indeed, `flambda` does this), but optimizing functors is hard. As we learned from Pierre Chambart, it is possible for the OCaml compiler to optimize functors directly, but this requires respecting several constraints that are difficult to respect in practice.

Split encoder and compressor

So, the choice was done to made the encoder which respects RFC 1951 and the compressor under some constraints. However, this is not what zlib did and, by this way, we decided to provide a new design/API which did not follow, in first instance, zlib (or some others implementations like miniz).

To be fair, the choice from zlib and miniz comes from the first point about API and the context where they are used. The main problem is the shared queue between the encoder and the compressor. In C code, it can be hard for the user to deal with it (where they are liable for buffer overflows).

In OCaml and for decompress, the shared queue can be well-abstracted and API can ensure assumptions (like bounds checking).

Even if this design is much more complex than before, coverage tests are better where we can separately test the encoder and the compressor. It breaks down the initial black-box where compression was intrinsec with encoding – which was error-prone. Indeed, decompress had a bug about generation of Huffman codes but we never reached it because the (bad) compressor was not able to produce something (a specific lengh with a specific distance) to get it.

NOTE: you have just read the main reason for the new version of decompress!

The compressor

The compressor is the most easy part. The goal is to produce from an inputs flow, an outputs flow which is an other (more compacted) representation. This representation consists to:

A literal, the byte as is
A copy code with an offset and a length

The last one say to copy length byte(s) from offset. For example, aaaa can be compressed as [ Literal 'a'; Copy (offset:1, len:3) ]. By this way, instead to have 4 bytes, we have only 2 elements which will be compressed then by an Huffman coding. This is the main idea of the lz77 compression.

However, the compressor should need to deal with the encoder. An easy interface, à la uutf should be:

val compress : state -> [ `Literal of char | `Copy of (int * int) | `End | `Await ]

But as I said, we need to feed a queue instead.

At this point, the purpose of the queue is not clear and not really explained. The signature above still is a valid and understandable design. Then, we can imagine passing Literal and Copy directly to the encoder. However, we should (for performance purpose) use a delaying tactic between the compressor and the deflator[^4].

Behind this idea, it's to be able to implement an hot-loop on the encoder which will iter inside the shared queue and transmit/encode contents directly to the outputs buffer.

So, when we make a new state, we let the user supply their queue:

val state : src -> w:bistring -> q:queue -> state
val compress : state -> [ `Flush | `Await | `End ]

The Flush case appears when the queue is full. Then, we refind the w window buffer which is needed to produce the Copy code. A copy code is limited according RFC 1951 where offset can not be upper than the length of the window (commonly 32ko). length is limited too to 258 (an arbitrary choice).

Of course, about the Await case, the compressor comes with a src function as the inflator. Then, we added some accessors, literals and distances. The compressor does not build the Huffman coding which needs frequencies, so we need firstly to keep counters about that inside the state and a way to get them (and pass them to the encoder).

[4]: About that, you should be interesting by the reason of why GNU yes is so fast where the secret is just about buffering.

The encoder

Finally, we can talk about the encoder which will take the shared queue filled by the compressor and provide an RFC 1951 compliant output flow.

However, we need to consider a special detail. When we want to make a DYNAMIC block from frequencies and then encode the inputs flow, we can reach a case where the shared queue contains an opcode (a literal or a copy) which does not appear in our dictionary.

In fact, if we want to encode [ Literal 'a'; Literal 'b' ], we will not try to make a dictionary which will contains the 256 possibilities of a byte but we will only make a dictionary from frequencies which contains only 'a' and 'b'. By this way, we can reach a case where the queue contains an opcode (like Literal 'c') which can not be encoded by the pre-determined Huffman coding – remember, the DYNAMIC block starts with the dictionary.

Another point is about inputs. The encoder expects, of course, contents from the shared queue but it wants from the user the way to encode contents: which block we want to emit. So it has two entries:

the shared queue
an user-entry

So for many real tests, we decided to provide this kind of API:

type dst = [ `Channel of out_channel | `Buffer of Buffer.t | `Manual ]

val encoder : dst -> q:queue -> encoder
val encode : encoder -> [ `Block of block | `Flush | `Await ] -> [ `Ok | `Partial | `Block ]
val dst : encoder -> bigstring -> off:int -> len:int -> unit

As expected, we take the shared queue to make a new encoder. Then, we let the user to specify which kind of block they want to encode by the Block operation.

The Flush operation tries to encode all elements present inside the shared queue according to the current block and feed the outputs buffer. From it, the encoder can returns some values:

Ok and the encoder encoded all opcode from the shared queue
Partial, the outputs buffer is not enough to encode all opcode, the user should flush it and give to us a new empty buffer with dst. Then, they must continue with the Await operation.
Block, the encoder reachs an opcode which can not be encoded with the current block (the current dictionary). Then, the user must continue with a new Block operation.

The hard part is about the ping-pong game between the user and the encoder where a Block expects a Block response from the user and a Partial expects an Await response. But this design reveals something higher about zlib this time: the flush mode.

The flush mode

Firstly, we talk about mode because zlib does not allow the user to decide what they want to do when we reach a Block or a Ok case. So, it defines some under-specified _modes_ to apply a policy of what to do in this case.

In decompress, we followed the same design and see that it may be not a good idea where the logic is not very clear and the user wants may be an another behavior. It was like a black-box with a black-magic.

Because we decided to split encoder and compressor, the idea of the flush mode does not exists anymore where the user explicitly needs to give to the encoder what they want (make a new block? which block? keep frequencies?). So we broke the black-box. But, as we said, it was possible mostly because we can abstract safely the shared queue between the compressor and the encoder.

OCaml is an expressive language and we can really talk about a queue where, in C, it will be just an other array. As we said, the deal is about performance, but now, we allow the user the possibility to write their code in this corner-case which is when they reachs Block. Behaviors depends only on them.

APIs in general

The biggest challenge of building a library is defining the API - you must strike a compromise between allowing the user the flexibility to express their use-case and constraining the user to avoid API misuse. If at all possible, provide an intuitive API: force the user not to need to think about security issues, memory consumption or performance.

Avoid making your API so expressive that it becomes unusable, but beware that this sets hard limits on your users: the current decompress API can be used to build of_string / to_string functions, but the opposite is not true - you definitely cannot build a stream API from of_string / to_string.

The best advice when designing a library is to keep in mind what you really want and let the other details fall into place gradually. It is very important to work in an iterative loop of repeatedly trying to use your library; only this can highlight bad design, corner-cases and details.

Finally, use and re-use it on your tests (important!) and inside higher-level projects to give you interesting questions about your design. The last version of decompress was not used in ocaml-git mostly because the flush mode was unclear.

Hide

Derivations as computations (ICFP 2019 slides) — Andrej Bauer, Aug 21, 2019

I gave a keynote talk "Derivations as Computations" at ICFP 2019.

Slides with speaker notes: derivations-as-computations-icfp-2019.pdf
Demo file: demo-icfp2019.m31

Slides with speaker notes: derivations-as-computations-icfp-2019.pdf
Demo file: demo-icfp2019.m31

Abstract: According to the propositions-as-types reading, programs correspond to proofs, i.e., a term t of type A encodes a derivation D whose conclusion is t : A. But to be quite precise, D may have parts which are not represented in t, such as subderivations of judgmental equalities. In general, a term does not record an entire derivation, but only its proof relevant part. This is not a problem, as long as the missing subderivations can be reconstructed algorithmically. For instance, an equation may be re-checked, as long as we work in a type theory with decidable equality checking.

But what happens when a type theory misbehaves? For instance, the extensional type theory elides arbitrarily complex term through applications of the equality reflection principle. One may take the stance that good computational properties are paramount, and dismiss any type theory that lacks them – or one may look into the matter with an open mind.

If there is more to a derivation than its conclusion, then we should not equate the two. Instead, we can adopt a fresh perspective in which the conclusion is the result of a derivation. That is, we think of a derivation as a computation tree showing how to compute its conclusion. Moreover, the computation encoded by the derivation is effectful: proof irrelevance is the computational effect of discarding data, while checking a side condition is the effect of consulting an oracle. Where there are two computational effects, surely many others can be found.

Indeed, we may set up type theory so that any terminating computation represents a derivation, as long as the computational steps that construct type-theoretic judgments are guaranteed to be validated by corresponding inference rules. Common techniques found in proof assistants (implicit arguments, coercions, equality checking, etc.) become computational effects. If we allow the user to control the effects, say through the mechanism of Plotkin and Pretnar’s handlers for algebraic effects, we obtain a very flexible proof assistant capable of dealing with a variety type theories.

Hide

View older blog posts.

OCaml Planet

Coq 8.11+beta1 is out — Coq, Dec 06, 2019

Deep-Learning the Hardest Go Problem in the World — Jane Street, Dec 06, 2019

Updates and a New Run

Frama-C 20.0 (Calcium) is out. Download it here. — Frama-C, Dec 04, 2019

Testing OCaml releases with opamcheck — GaGallium (Florian Angeletti), Dec 03, 2019

OCaml and the opam repository

OCaml and the opam repository

Catching knifes before the fall

Opam and the PRs

Using opamcheck

Coq 8.10.2 is out — Coq, Nov 29, 2019

Announcing Irmin 2.0.0 — MirageOS (Anil Madhavapeddy), Nov 26, 2019

BAP 2.0 is released — The BAP Blog, Nov 19, 2019

The Knowledge Base

New Program Representation

Links

CI/CD pipelines: Monad, Arrow or Dart? — Thomas Leonard, Nov 14, 2019

Introduction

Attempt one: a monad

Attempt two: an arrow

Attempt three: a dart

Comparison with arrows

Larger examples

OCaml Docker base image builder

OCaml CI

Conclusions

On fixed-point theorems in synthetic computability — Andrej Bauer, Nov 06, 2019

Runners in action — Andrej Bauer, Oct 27, 2019

Coq 8.10.1 is out — Coq, Oct 25, 2019

Announcing MirageOS 3.6.0 — MirageOS (Martin Lucina), Oct 18, 2019

MirageOS 3.6.0 release

MirageOS 3.6.0 release

Commas in big numbers everywhere: An OpenType adventure — Jane Street, Oct 14, 2019

Coq 8.10.0 is out — Coq, Oct 07, 2019

OCaml expert and beginner training by OCamlPro (in French): Nov. 5-6 & 7-8 — OCamlPro, Sep 25, 2019

Mr. MIME - Parse and generate emails — Tarides (Romain Calascibetta), Sep 25, 2019

An email parser

An email parser

An extended email parser

A realistic email parser

A parser usable by others

An email generator

78-character rule

A multipart email generator

Behind the forest

Rosetta

Pecu and Base64

Conclusion

A look back on OCaml since 2011 — OCamlPro, Sep 20, 2019

2011

2012

2013

2014

2015

2016

2017

2018

2019

Frama-C 19.1 (Potassium) is out. Download ithere. — Frama-C, Sep 17, 2019

Coq 8.10+beta3 is out — Coq, Sep 16, 2019

Updated Cheat Sheets: OCaml Language and OCaml Standard Library — OCamlPro, Sep 13, 2019

Frama-Clang 0.0.7 is out. Download ithere. — Frama-C, Sep 13, 2019

Decompress: Experiences with OCaml optimization — Tarides (Romain Calascibetta), Sep 13, 2019

Cautionary advice

Specialization

Results

Inlining

In decompress

Untagged integers

Readability versus performance

Exceptions

Unrolling

Results

hot-loop

caml_modify

About decompress

Smaller representation

Conclusion

On complete ordered fields — Andrej Bauer, Sep 08, 2019

In `decompress`

About `decompress`

Using `bun` to run fuzz testing in CI

The new `decompress` API