Gagallium

In this post you can find out what was cut from the previous post on singleton types. These are more technical considerations that may require some familiarity with type theory. In particular, I’ll discuss linear and dependent types in the context of describing more and more singletons.

Could the compiler guess a part of the program I am currently writing? It’s impossible in general, but it may be possible, and hopefully interesting, in special cases. For a start, I am interested in a situation where there is only one possibility: at the expected type, there is only one possible program – modulo (an approximation of) program equivalence.

In a fixed environment, a type is a singleton type if it has only one inhabitant. How widespread are those? Would a language feature to infer their inhabitants be useful? Can we have more interesting singleton types by enriching the type system?

Don’t expect a structured story with a happy ending: this is only a writing-ideas-down session for something I have been thinking about lately.

This is a call to arms: to improve the OCaml compiler, we sorely need a suite of representative benchmarks. If you have ever written performance-sensitive programs in OCaml, you can contribute.

In my last post, I explained my work on verifying a parser for Compcert. I was mainly explaining the solutions I found to my performances problems. Here, I will discuss an other interesting problem I have, concerning the context sensitivity of the C99 grammar.

I recently started a post-doc in the Gallium team, and it is past due-time for my first blog post. I will not start with a research oriented blog right now (but stay tuned!); and I will rather talk about one of my hobbies: writing Coq plugins in OCaml to build new tactics. I reckon that this deviates a bit from standard practice, so I will try to make things clear.

One of my parsing-related Coq files takes more than two hours to compile, which is pretty annoying when the file is less than one thousand lines long and does no complex computations. After some profiling, it appeared that Coq was spending most of its time in the Univ module. This module is part of the Coq kernel, its role is to check that the user is using universes in a consistent way.

Just a few weeks ago, Andrej Bauer wrote two articles ( 1 2 ) about implementing a dependent type theory in Ocaml. In particular, he demonstrates a cool idea to normalize expressions, called « normalization by evaluation ».

However, when trying to evaluate 2²⁰, the program overflows the stack. It turns out that there is an easy and methodic way to locate and fix such problems, which we will discuss in that post.