Ben Darwin will be presenting "State Machines All The Way Down" by Edwin Brady
In a dependently-typed programming language such as Agda or Idris, types may refer to ordinary terms in the language and so express precise guarantees about run-time behaviour. For instance, one may define size-indexed arrays and operations on them so that type-checking guarantees the absence of out-of-bound indexing. This paper applies this machinery, along with Idris's 'interfaces' (or typeclasses), to a somewhat different situation: creating type-safe state transition systems - that is, protocols whose correct usage is similarly guaranteed by their type-correctness. The resulting library, ST, based around the notion of indexed monad, allows specifying protocols which are compositional in both horizontal (multiple protocols can be used simultaneously) and vertical (protocols can be defined in terms of other protocols) senses. We'll see examples, such as safe Unix socket programming, and how additional Idris features combine to improve the usability of this library. I will begin with a brief introduction to dependent types and indexed monads in Idris in order to make the presentation hopefully self-contained.
Paper link: https://www.idris-lang.org/drafts/sms.pdf
Ben Darwin is a programmer/analyst at Sick Kids Hospital's Mouse Imaging Centre.