A blog at Gallium: informal posts about research, programming practice, OCaml development, and general ramblings.

## Fast vectorizable math functions approximations

- January 26, 2015
- Last updated on 2015/01/27

How and why I designed my own approximated implementations
of `log`

, `exp`

, `sin`

and `cos`

. The approximation error is quite
small, and the functions are fast and vectorizable. For example, my
`logapprox`

function is 7.5x faster in tight loops than
the `icsi_log`

function, while being more precise.

## Left-recursive versus right-recursive lists in LR parsers

- January 21, 2015
- Last updated on 2015/01/22

Contrary to top-down (LL) parsers, which do not support left recursion, bottom-up (LR) parsers support both left recursion and right recursion. When defining a list-like construct, a user of an LR parser generator, such as Menhir, faces a choice between these two flavors. Which one should she prefer?

Two considerations guide this choice: expressiveness (which flavor leads to fewer conflicts?) and performance (which flavor leads to a more efficient parser?).

In this post, I am mainly interested in discussing expressiveness. I also comment on performance in the setting of Menhir.

As we will see, the bottom line is that neither formulation seems deeply preferable to the other.

## Normalization by realizability also computes

- December 2, 2014
- Last updated on 2014/12/02

I share with Pierre Dagand the pleasure of having finished
the redaction of a small article on realizability for JFLA
15 (Journées francophones des langages
applicatifs). It is a rather simple presentation of the *computational
content* of adequacy proofs, which we hoped to understand better by
exhibiting their proof terms as well-typed lambda-terms in a dependently
typed meta-language.

http://gallium.inria.fr/~scherer/research/norm*by*rea/dagand-scherer-jfla15.pdf

## 2-or-more approximation for intuitionistic logic

- November 25, 2014

I just finished the proof of a property of the simply-typed lambda-calculus that hopefully can serve as a termination argument to decide whether a type has a unique inhabitant.

http://gallium.inria.fr/~scherer/drafts/2-or-more-approximation.pdf

The 10-pages note containing the proof is available, and all comments are warmly welcome -- in particular about an already-existing proof of this result, I don't know about any. The rest of this post is (a HeVeA rendering of) the introduction, motivating the problem and presenting the fact to be proved -- or disproved. Feel free to ask yourself whether it is true or false before looking at the full note. The answer is at the last sentence of the introduction (only in the note).

It is interesting that we don't have much intuition about whether the result is true or false -- I changed my mind several times about it, and people asked about it guessed different way. The proof, however, is relatively simple and not particularly technically involved -- but I spent a few days simplifying the concepts and the notations.

## Two final versions and a Verasco release

- November 3, 2014

We have just submitted the final version of two papers, presenting the state of our recent research.

- A Formally-Verified C Static Analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie
- Verified compilation of floating-point computations, by Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond

## Lawvere theories and monads

- July 29, 2014
- Last updated on 2014/07/30

In this Agda file, I give an introduction to Lawvere theories and Monads. It's not exactly a "gentle" introduction because:

- I'm still trying to grok these things myself,
- I've to live up to my reputation of writing unfathomable gagaposts.

We'll start with the State monad and, briefly, a Tick monad. The game is the following: I'll present them syntactically -- through a signature -- and semantically -- through a collection of equations. I'll then show how the usual monad is related to this presentation.

## Paper draft: the Essence of Ornaments

- June 16, 2014

The Essence of Ornaments (pdf) is a draft of a new article, hoping to provide an accessible introduction to the theory of ornaments. Any feedback on the draft, in the comments or by email, is warmly welcome.

## Ornaments in practice

- May 27, 2014

I (Thomas Williams) am currently doing an internship with Pierre Dagand and Didier Rémy on ornaments, a way to relate datatypes sharing a common structure. Ornaments come from the scary world of dependent types, and the goal of my internship is to implement them in the more familiar setting of ML datatypes. We've produced a draft where we present how ornaments can be useful in practice in an ML-like programming language.

## Current (and future?) state of OCamlbuild parallelization

- May 18, 2014

A few days ago, Hugo Heuzard asked about the details of the problem with OCamlbuild's parallelism today on mantis: PR#5754. My mantis comment quickly grew into the blog post below.

I worked last September on better parallelization for OCamlbuild, but didn't finish the thing (I couldn't get something mergeable in time for ICFP) and got distracted with tons on other things to do since. I just uploaded the state of my branch:

https://github.com/gasche/ocaml/tree/ocamlbuild-indirect-style

## The 6 parameters of (’a, ’b, ’c, ’d, ’e, ’f) format6

- April 18, 2014

The infamous `format6`

type is the basis of the hackish but damn
convenient, *type-safe* way in which OCaml handles format strings:

```
Printf.printf "%d) %s -> %f\n"
3 "foo" 5.12
```

The first argument of `printf`

in this example is not a string, but
a format string (they share the same literal syntax, but have
different type, and there is a small hack in the type-inference engine
to make this possible). It's type, which you can get by asking
`("%d) %s -> %f\n" : (_,_,_,_,_,_) format6)`

in a toplevel,
is a mouthful (and I renamed the variables for better readability):

```
(int -> string -> float -> 'f, 'b, 'c, 'd, 'd, 'f) format6
```

What do those six arcane parameters mean? In the process of reviewing
Benoît Vaugon's work
on using GADTs to re-implement format functions, I've finally felt the
need (after years of delighted oblivion) to understand each of those
parameters. And that came after several days of hacking on
*easier-to-understand* ten-parameters GADT functions; hopefully most
of our readers will never need this information, but the probability
that I need to refresh my memory in the future is strong enough for me
to write this blog post.