Type-driven Development of Communicating Systems in Idris by Edwin Brady

Edwin Brady demonstrates how to use Idris and dependent types to guarantee that concurrent, communicating systems interact correctly.

Idris is a functional programming language with dependent types, which supports ‘total’ functional programming. A function is total if, for all well-typed inputs, it gives either a complete result of a finite prefix of an infinite result, in finite time. Total functions give us strong guarantees about their behavior: for example functions can’t crash due to badly formed inputs, servers will always produce responses to requests. In this talk, I’ll show how Idris supports total programming, with a series of examples. As an extended example, I’ll show how to define a type for describing communicating concurrent systems which, by writing total functions, guarantees that concurrent programs will interact as intended. About Edwin: Edwin Brady is a Lecturer in Computer Science at the University of St Andrews, interested in type theory, dependently typed functional programming, compilers and domain-specific languages (DSLs). He is currently working on the implementation of DSLs for stateful, resource-aware programming, especially for correct network protocol design and implementation, using Idris, a dependently typed functional programming language. When he’s not doing that, you might find him playing Go (He’s about 1 kyu), walking up a hill, watching a game of cricket, or waiting for a delayed train. He also perpetrated the whitespace programming language. Follow @edwinbrady for more on his work and the book he alleges he’ll complete in 2038. About Lambda World: The 2016 Lambda World brought together Functional Programming enthusiasts from around the world for two days of presentations, hacking, networking, and a healthy dose of partying in Cadiz, Spain. Hosted by 47 Degrees, the event also featured a Typelevel Community Conference and a Scala Center Hackathon. Join in on the conversation at twitter.com/lambda_world and twitter.com/47deg using #LambdaWorld. Stay tuned to lambda.world and 47deg.com for more on the conference and announcements for the 2017 event.