Singleton types for code inference, continued

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.


Singleton types for code inference

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.


OCaml compiler optimizations: we need a representative benchmark suite

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.


Verifying a parser for a C compiler (continued)

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.


Emancipate yourself from LTac: Your first Coq plugin

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.


Performance improvements in the universe checker of Coq

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.


Fixing stack overflows using continuations

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 220, 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.