Totality versus Turing Completeness

Speaker: Conor McBride, University of Strathclyde

Abstract: It's a well known fact that a total programming language can't encode its own interpreter. Some advocates and most detractors of total programming  note that it comes at the cost of Turing Completeness, another well known fact. These well known facts are about as true as the fact that "Haskell can't handle I/O." I shall talk about ways in which total languages can model the risk of nontermination, and show you a method I have found useful, inspired by notions of algebraic effect. If time permits, I shall sketch an appropriate effect-checking type discipline and/or show how to automate the construction of Bove-Capretta domain predicates by recursive computation over the relevant free monad.