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.
Edwin Brady is a Lecturer in Computer Science at the University of St Andrews in Scotland, UK. His research interests there include programming language design, in particular type systems and domain specific languages. Since 2008, he has been designing and implementing the Idris programming language, a general purpose functional programming language with dependent types, which he uses to implement verified domain specific languages. When he’s not doing that, he’s likely to be playing a game of Go, wrestling with the crossword, or stuck on a train somewhere in Britain.