New draft on Normalization by Evaluation using GADTs

Syntax!

There is a new draft on my web page! It is called Tagless and Typeful Normalization by Evaluation using Generalized Algebraic Data Types, which is a mouthful, but only describes accurately the cool new OCaml development we elaborated together with Olivier and Chantal. The world of Normalization by Evaluation (NbE) is still relatively new to me, but its wonders keep amazing me. It’s a program specialization algorithm… no, it’s a completeness proof for first-order logic… wait, it’s a technique to turn an interpreter into a compiler! Definitely, Aarhus University, my new home, is not the worst place to learn about it.

Since the introduction of GADTs in OCaml, a whole new realm of applications emerged, the most well-known being to faithfully represent typed languages: it allows to define compact and correct interpreters, and type-preserving program transformations. Ok, if you never saw this, here is a small snippet that…

View original post 321 more words

Building a C# compiler in F#

Neil Danson's Blog

A little over a year ago I wrote a post about Roslyn.

Recently (after seeing Mads Torgersen‘s excellent NDC-london talk) I was inspired to attempt to write my own mini-C# compiler to address some of the missing features in C#.

Mads Torgersen repeating what I said a year ago Mads Torgersen repeating what I said a year ago

Roslyn

Roslyn is a Microsoft project to rewrite the VB and C# compilers in their respective languages. After Mads talk, and listening to the (proposed) new features for C# 6 I couldn’t help but feel a little underwhelmed with the direction of C#.

Mads’ justification seems reasonable on the face of it – C# 2, 3,4 & 5 have all had major new language additions (namely generics, linq, dynamic & async) and that C# 6 is more of a ‘tidy the pain points’ release. But I had a number of ideas for improvements, and unfortunately only two are…

View original post 1,644 more words