Erlang/OTP meets Dependent Types
Archibald Samuel Elliott
August 2015 • Extended Abstract • ICFP 2015 Student Research Competition
Abstract
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 dependently-typed supervisors.