Type-driven Development of Communicating Systems in Idris

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 behaviour: 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 to show how total programming works in practice, 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.