Rss feed
July 3, 2017

This week has been dedicated to records: parsing, simplification and (a bit of) typing.

read more
June 26, 2017

After some more engineering on the typer, I'll now start dealing with records

read more
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.

read more
June 2, 2017

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.

read more
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.

read more
April 25, 2017

This week's post will be about adding gradual types and type annotatinos to the system.

read more
April 10, 2017

Nix is all about records. They are everywhere in nixpkgs, and even the semantics of nix seems to have been designed with this idea of records everywhere as a first class construct. (In fact, I think that it would be more correct to think of nix as "json with lambda-calculus on top of it" rather than "a functional language with lists and records").

Thus we have to type records.

read more
April 3, 2017
Before we can work on the type system, the first step is to define the language in a way that will allow us to think about it. In particular, we wanted to simplify it as much as possible by removing everything that could be considered as syntactic sugar. read more
March 28, 2017
So this is it, my internship has begun. As promised, I will try to post regular updates on my work on this blog. read more