Proving and implementing

May 26, 2017

It's been a month (already !) since my last update on this work. In the meantime, we've begun to prove a subset of the type-system, and (slowly) started the implementation.

One nice feature that we added in order to make our system more powerful is a little touch of bidirectional typing, which allows us to type some expressions that the old type-system wasn't powerful enough to type.

Here is an example (and in fact the example that motivated this addition in the first place):

Although the type annotation corresponds to a type that's perfectly reasonable − `f`

applied to a value of type `true`

and a value of type `Int`

returns an `Int`

, and applied to a value of type `false`

and a value of type `Bool`

returns a `Bool`

−, the type-system isn't able to infer it. It doesn't matter how we annotate the expression, it can't, because we would have to annotate `x`

as either `Int`

or `Bool`

depending on the value of `cond`

, and our system can't express this.

Without diving into the details, this is now possible to do. Of course this exact case isn't really exciting as it is easily possible to rewrite is as something with roughly the same semantics and that already was possible to type. But the really nice thing is that most of the times you now only have to annotate the top-level functions, and not every single lambda in the code.

The main work of those last weeks has been on establishing a proof of the soundness of (the core of) the type-system.

Saying that a type-system is "sound" intuitively means that it respects the adage that "well-typed programs cannot go wrong". The exact definition depends on what it is intended for, but in our case we can define it as "A well-typed expression will either loop indefinitely, raise an exception, or reduce to a value" (where a value is a constant, a list, a record, a function…).

We've been working on this the last few weeks, and this is somehow harder than expected. The classical way of proving soundness is to prove two lemmas known as "subject reduction" and "progress". The first one states that if a well-typed expression `e`

reduces ("evaluates") to another expression `e'`

, then `e'`

is also a well-typed expression, which has the same type as `e`

(or a more precise type). The second one states that if `e`

is a well-typed expression, then it reduces to some `e'`

. The combination of those two lemmas give us our soundness theorem.

The fact is that the subject-reduction lemma doesn't hold for our system − for a couple of reasons that I won't detail here to keep things simple, but that I would gladly explain if anyone is interested. We see some possible workarounds for this, but we still have to investigate a little more to ensure that they are viable.

We also started the implementation. For this, we will reuse a lot of code from the implementation of the type system of the CDuce language because ours shares a lot with it. In particular, a really big part − maybe the biggest part − of the implementation is the subtyping relation, which is the same in CDuce and in Nix.

Unfortunately the code of CDuce, although really well-written, lacks of documentation and is hardly commented, so it took me some time to get into it.

Apart from trying to keep this weekly newsletter weekly − and I apologize for the whole month of silence, I'll try next week to come up with a clear idea of how to prove the soundness (not a fully redacted proof, but at least the main arguments), and advance on the implementation − ideally, I'd like to have a working prototype of a simplified type-checker (without bidirectional typing) for the core lambda-calculus − no lists and no records − within three weeks (but I'm not very good at estimates, so this doesn't mean much).