A Concurrency System for Idris & Erlang
Archibald Samuel Elliott · 2015
Concurrent programming is notoriously difficult, due to needing to reason not only about the sequential progress of any algorithms, but also about how information moves between concurrent agents. What if programmers were able to reason about their concurrent programs and statically verify both sequential and concurrent guarantees about those programs’ behaviour? That would likely reduce the number of bugs and defects in concurrent systems. I propose a system combining dependent types, in the form of the Idris programming language, and the Actor model, in the form of Erlang and its runtime system, to create a system which allows me to do exactly this. By expressing these concurrent programs and properties in Idris, and by being able to compile Idris programs to Erlang, I can produce statically verified concurrent programs. Given that these programs are generated for the Erlang runtime system, I also produce verified, flexible Idris APIs for Erlang/OTP behaviours. What’s more, with this description of the Idris code generation interface, it is now much easier to write code generators for the Idris compiler, which will bring dependently-typed programs to even more platforms and situations. I, for one, welcome our new dependentlytyped supervisors. 1. Idris to Erlang Compiler My compiler uses the existing Idris code generation system. There are three possible Idris intermediate representations that I could generate code from: a high-level IR with lambdas and laziness, a defunctionalised IR with only fully-applied functions, and an applicative-normal form IR. In my case, we used the defunctionalised IR to generate Erlang source code from, according to the following translation, E J〈expression〉K. V J〈variable〉K turns IR variables into valid Erlang variable names; C J〈name〉 # 〈expression〉*K creates constructors; N J〈name〉K turns IR names into valid Erlang Atoms; L J〈constant〉K turns IR constants into Erlang expressions; and O J〈operation〉 # 〈expression〉*K turns primitive operators into their Erlang equivalent. E J〈variable〉K ⇒ V J〈variable〉K E J〈name〉(〈expression〉*)K ⇒ C J〈name〉 # 〈expression〉*K when 〈name〉 is a Constructor ⇒ N J〈name〉K(E q 〈expression〉0 y , · · ·, E q 〈expression〉n−1 y ) otherwise E q let 〈name〉 := 〈expression〉0 in 〈expression〉1 y ⇒ V Jglobal〈name〉K = begin E q 〈expression〉0 y end, E q 〈expression〉1 y E J update 〈name〉 := 〈expression〉K ⇒ E J〈expression〉K E J[〈expression〉]nK ⇒ element(n+2, E J〈expression〉K) E J new 〈name〉(〈expression〉*)K ⇒ C J〈name〉 # 〈expression〉*K E J case 〈expression〉 of 〈alternative〉* end K ⇒ case E J〈expression〉K of A J〈alternative〉0K; · · ·; A q 〈alternative〉n−1 y