June 14, 2017

I couldn't find the time last week to make something presentable out of the typechecker as I promised, but almost all the features are already here − except records which I'll probably start implementing in a few weeks.

Implementation

State of the typechecker

I finished most of the engine for the language without records, so I'll now work on adding everything that is needed around, and handling some constructs that could be ignored from a theoretical point of view − mostly because it could be considered as just some syntactic sugar.

Here are the constructs that need to be considered:

Assert
The assert construct should be typed in a rather simple way, as assert e1; e2 is equivalent to if e1 then e2 else raise "Assertion failed" 1 .

Import
The simplest way to handle the import statement is to simply replace it by a dump of the imported file. This is probably what I will do in a first time. In a second time, it may be useful for performance reasons to type the imported file separately and memoïze the result (this is what nix does with the evaluation iirc).

Different modes of check

During the design of the type-system, there has been a constant tension between having a safe type-system and being able to typecheck as much existing code as possible.

Eventually, it became clear that both weren't compatible, and that in order to keep the best of both worlds, we needed to have (at least) two different versions (a "permissive" one and a "strict" one) of the type-system. So that's what we decided to do, with an annotation to switch from one to the other. Nothing has been implemented in this direction, and the boundary between strict and permissive hasn't been decided yet − especially, it will mostly concern records. But an important point is that the gradual type will be considered differently.

On the theoretical side

There hasn't been much improvement here, as I am still stuck with the proof of correctness, which is definitely harder than expected (but I must admit, I didn't work a lot on it). A PhD student of my advisor is also working on a really similar proof, and hopefully he will find a solution − as I don't really have much more time for this because I need to work on the implementation.

Next week

I'll start drafting headlines for my dissertation; this will allow me to see which points need some more work.

In parallel, I plan to make the type annotations for lists − this will probably deserve its own post as there is some really elegant stuff that I borrow from CDuce and that are worth presenting, as well as to treat the assert and import keywords.

I'm also rewriting the parser − this is already almost over, but there is still a few polishing work ongoing, as the old one was a quick and dirty crafted one, that I wrote in order to be quickly able to work on the typechecker itself, but which behaves quite badly − in particular regarding error messages.


1 Well, it is not strictly equivalent because the exceptions raised by assert and the one raised by raise aren't exactly the same − see this comment −, but four our purposes, it is the same.

Commentaires