What’s all this then?

I’m glad you asked. It’s a new blog series I’m writing, to go along with some code I’ve been hacking on and a talk I presented at YOW! Lambda Jam.

The focus is on writing Domain Specific Languages (DSLs) in Haskell.

Some of it will be about some of the cool tools, techniques and libraries we can use in Haskell. There’s some great stuff out there, with mixed amounts of documentation. I’m not going to fully cover the gaps there, but hopefully I can get you to take a look at something you might otherwise have left on the shelf.

Some of it will be about how to get your feet wet with Programming Language Theory (PLT) in order to help improve your DSLs. For the most part it’s super useful, it’s not anywhere near as scary as it looks going in, and you can get a lot of good use out of the easy bits that you pick up in the beginning.

Some of it will be madness, where I try to work out if I can do something without much regard for whether I should be doing it at all. I’ll try to remember to point out when I’m doing that.

There will also be some themes that run through this project: testability and composition. We’ll be using QuickCheck to do a lot of heavy lifting for us on the testing front. For composition, we’ll periodically refactor the code that we have to make things more reusable and composable.

The talk

Here is the video, here are the slides and here is the code.

The blog posts

Part 1 - The basics

With many more on the way…

For those of you playing along at home

These posts should all be self-contained, so you probably don’t need the following books. I had them in my books-that-I-want queue for a long time but wasn’t sure I eas ready for them, and now I kind of wish that I dived in earlier.

There are two books on PLT that are standard recommendations. The reason they are standard recommendations is because they are great.

“Types and Programming Lanugages” (TAPL) by Benjamin Pierce.

“Practical Foundations For Programming Languages” (PFPL) by Robert Harper.

If it has been a while since you’ve done mathematical proofs, I highly recommend “How To Prove It” (HTPI) by Daniel Velleman.

The second chapter of TAPL mentions all of the math that you’ll need to do all of the exercises. HTPI will get you there, and open some other doors as well.

An alternative recommendation is to work through “Software Foundations” in parallel with TAPL. The first part teaches you how to use Coq to prove things. After that it covers similar material to the first half of TAPL, with the Coq compiler checking your proofs along the way.

I’ll recommend some more materials later on, when the content spirals off into some other directions, but for now the above should be fine.

Why are you doing this?

When I was new to Haskell, someone mentioned a paper that covered something I was interested in, and so I started to skim it.

It was about an extension to Haskell, and I can clearly remember that it was formatted in two columns. Other bits I’m a bit more vague about, since it was pretty alien to me.

The bit that really struck me was that it was all on one page.

The first column mentioned the additions to the type system in some syntax that I couldn’t read. The second column mentioned the addition to the semantics in some other-but-related syntax that I also couldn’t read. After the diagrams with the changes where the proofs that the changes didn’t break anything in the existing system and that the changes delivered on their promises.

The paper then went on to discuss various extensions and alternatives to their change - clearly the authors had done what they’d wanted to do on that page, and were keen to discuss other matters.

I was very struck by how composable the two strange-looking syntaxes were, and how effective the existing proofs and proof strategies were at dealing with incremental changes. That’s when I asked some questions, picked up TAPL, and - after reading Chapter 2 of TAPL - picked up HTPI.

If you read a bit of TAPL or PFPL, you’ll see that it takes a similar approach. It spends a lot of time incrementally building up a series of languages and proving that the increments add what they claim to and that they don’t make a mess while doing it.

I found that exciting, and hopefully I can spread some of that excitement around with this series.

There are also a few tools that make some of this easier, and I’m pretty keen to spread the word about them.

Site proudly generated by Hakyll