Resource aware DSELs

Just wrote a short note about implementing resource aware domain specific languages by embedding in Idris. Still much to do, but the notation is getting better (less need to write strange looking types, for example).

Correct-by-construction Concurrency

I’ve been hacking merrily away in Idris over the last couple of weeks, seeing what I can make it do. One of the first things I wanted to try was an idea I had for a domain specific embedded language (DSEL) for concurrent programming. The result is written up in this draft paper.

I think one of the areas where dependently typed languages will become important, given appropriate and mature tools, will be the design and implementation of verified DSEL.
Here we use a DSEL to manage the lock state (i.e. number of times locked, type of the value stored in it) of each shared resource – it’s essentially a state monad parametrised over the type and lock status of the resources – which means that the lock state is statically known. As a result, the typechecker can verify that resources are locked before they are accessed, released before exit even in exceptional conditions, and even that they are requested in an order which guarantees deadlock freedom. Programs in the DSEL look (more or less) like monadic Haskell programs.