This week has been shared between a lot of easy fun putting together all the
pieces that I worked on during the last weeks, and a lot of frustration trying
to prove the soundness of the system.

Implementation

After several weeks spent trying to understand the API of CDuce − the language our type-system takes it inspiration from and whose code we planned to reuse as much as possible to ease the Implementation −, I eventually understood it enough to start using it for writing the inference engine.

This has been really enjoyable, as all I had to do was plugging together a few functions that where already dealing with all the boring low-level stuff, and everything has been almost instantly working. I could quickly write a prototype of typer for the core lambda-calculus of the language. It is still a little bit too rough on the edges to be presented, but I should (hopefully) be able to present some nice examples for next week.

On the theoretical side

I talked last week about some difficulties with the proof of the soundness of the type-system.

Those difficulties still hold, although some progress has been done. There are a couple of paths that we are currently exploring for a this:

We may change a bit the semantic of the language we work on (which is currently an approximation of the lazyness of nix) with something closer actual lazyness. This should probably solve our problems, but at the cost of redefining the language with a heavier and less practical formalism.

We may use a non-syntactic proof using something like what is described in this paper which a colleague from tweag suggested to me. While mathematically-heavy, this kind of proof has the advantage of being able to operate on our simplified semantic, which means we can keep our simple formalism everywhere else. It also is more modular than syntactic proofs, which means that we may prove some extensions of the core system without needing to rewrite the full proof.

Next week

Next week will be more or less like this one: I'll continue the implementation using all the nice features offered by CDuce. In the same time, I'll keep on working on the proof − I hope that this will be solved before next Friday.

Provided I find the time − which is rather unlikely, but who knows? − I'll also try to make an online demonstration of the engine to show the progress of the implementation.