Resource-safe DSELs

I talked yesterday about some recent work with Idris on implementing Domain Specific Embedded Languages using dependent types to guarantee that important resource properties are preserved.

One of the standard examples of any language that uses dependent types to some extent is the “Well-typed interpreter”. Cayenne has one, Epigram has one, here’s the Idris version, it’s a typical example for motivating GADTs in Haskell, etc…

Well-typed interpreters like this become really interesting when you want to express other static properties, such as safe resource usage. The challenge is to keep the notational overhead low while retaining compositionality and correctness. Here, for example, is a program in a domain specific language embedded in Idris which allocates two chunks of memory, does some reading and writing, then frees them. It typechecks, so we know that there will be no memory leaks, and no invalid memory accesses.

testProg : MemSafe TyUnit;
testProg = program 2
	   (BIND (ALLOC 1024)
     (\b1.  BIND (ALLOC 1024)
     (\b2.  BIND (PEEK (handle b1) 100 ?)
     (\val. BIND (POKE (handle b2) 100 val ?)
     (\u.   BIND (ACTION (putStrLn "testProg OK"))
     (\u.   BIND (FREE (handle b1) ?)
     (\u.   FREE (handle b2) ?)))))));

The type MemSafe TyUnit says this is a memory safe program which does not return a value (or rather, returns the unit value). The notational overhead is:

• The program must be preceded by program n where n is the number of memory regions which will be allocated.
• Each access generates a proof obligation, where you must show that the location you want to access is available. Hence the ? (as discussed here)
• handle converts your handle ID to something usable in a resource constraint proof. The programmer doesn’t need to understand the details of this, just to use it!
• Idris does not yet have a generic do notation, hence all the BINDs. Adding such a thing would be a small matter of programming.

Things get more interesting when you want to call other functions defined in this way, or when you have some dynamic data. Here’s a memory safe program which takes a location within a region as an argument, and calls another program:

testProg2 : Int -> (MemSafe TyUnit);
testProg2 loc = program 2
           (BIND (ALLOC 1024)
     (\b1.  BIND (ALLOC 1024)
     (\b2.  maybe (checkBound loc 1024)
	          (BIND (ACTION (putStrLn "Error"))
	      (\t. BIND (call testProg)
	      (\t. BIND (FREE (handle b1) ?)
	      (\t. FREE (handle b2) ?))))
     (\cmp. BIND (PEEK (handle b1) loc ?)
     (\val. BIND (POKE (handle b2) loc val ?)
     (\u.   BIND (FREE (handle b1) ?)
     (\u.   BIND (FREE (handle b2) ?)
     (\u.   ACTION (putStrLn "Success")))))))));

Since this is embedded in a general purpose host language, we can add any helper functions we think will be useful. Here, we’ve used maybe to do a dynamic check, and compute either a proof that a location is in range, or not if the location is out of range. We’ve used call to run another DSEL program.

Running the whole thing is done by:

main : IO ();
main = interp Empty (testProg2 1025);

A similar idea works for file management and shared memory handles in concurrent programs. The next question is — can we make the framework generic so that implementing a resource aware DSEL is a simple matter of describing the resource constraints? Can we compose languages with multiple resource types? We shall see…