• en

# OCaml Planet

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

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

# 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…

# 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.

# 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:

1. OCaml Beginner course for professional programmers (5-6 Nov)
2. 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…

# 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…

# 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.

# OCaml Developer at Ahrefs Pte Ltd (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 14, 2019

What We Need

Ahrefs is looking for a backend developer with deep understanding of networks, distributed systems, OS fundamentals and taste for simple and efficient architectural designs. Our backend is mostly implemented in OCaml with some C++ and Rust.

In this role, be prepared to deal with 25 petabytes of live data, OCaml and Linux on a daily basis.

Basic Requirements:

• Proficiency in OCaml
• Knowledge of C++ and/or Rust is a plus

The ideal candidate is expected to:

• Independently deal wi…

# Compiler Engineer at Axoni (Full-time) — Functional Jobs (FunctionalJobs.com), Sep 13, 2019

Compiler Engineer

Headquartered in New York City, we are currently working intensely on what we expect to become the most widely used programming language for blockchain smart contracts: AxLang. Based on Scala, AxLang enables secure and full featured smart contract development by supporting both functional programming and formal verification. Its design is driven by the rigorous requirements for solutions serving the world's largest financial institutions.

AxLang is part of Axoni's b…

# 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…

# 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…

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

Theorem: All complete ordered fields are isomorphic.

The standard proof posted by Joel has two parts:

1. A complete ordered field is archimedean.
2. 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 …

# 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…

# 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…

# 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

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

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 e…

# Deriving Slowly — Rudi Grinberg, Aug 20, 2019

There’s been some recent grumbling about the usability of ppx in OCaml, and instead of just letting it slide again, I’ve decided to do something constructive about this and write a little tutorial on how to write a deriving plugin.

# Using OCaml to drive a Raspberry Pi robot car — Jane Street, Aug 19, 2019

Back when the Raspberry Pi was first released in 2012 Michael Bacarella wrote a blog post on using OCaml and Async on this little device. Since then installing OCaml via opam has become a pretty smooth experience and everything works out of the box when using Raspbian – the default Raspberry Pi distribution.

# Do applied programming languages research at Jane Street! — Jane Street, Aug 16, 2019

As our Tools & Compilers team has grown, the kinds of projects we work on has become more ambitious. Here are some of the major things we’re currently working on:

# X509 0.7 — Hannes Mehnert (hannes), Aug 15, 2019

## Cryptographic material

Once a private and public key pair is generated (doesn't matter whether it is plain RSA, DSA, ECC on any curve), this is fine from a scientific point of view, and can already be used for authenticating and encrypting. From a practical point of view, the public parts need to be exchanged and verified (usually a fingerprint or hash thereof). This leads to the struggle how to encode this cryptographic material, and how to embed an identity (or multiple), capabilities, …

# BAP Knowledge Representation - Part 1 — The BAP Blog, Aug 15, 2019

An important part of BAP 2.0 is the new knowledge representation system, which drives all the new code. Given how important it is for understanding and using modern BAP, I decided to introduce it informally in a series of blog posts. This series is by no means a substitution for documentation or a tutorial, which will (I hope) follow. The intention is to describe the system in a friendly manner like I would describe it to my colleague in front of a whiteboard.

All information in BAP 2.0 is stor…

# Down — Daniel Bünzli, Jul 23, 2019

First release of Down, an unintrusive OCaml toplevel experience upgrade.

View older blog posts.