Edwin Brady Lambda World Interview

Edwin Brady will be speaking at Lambda World in September 2016. He is the creator of Idris, a dependently typed language. He'll be talking about total functions.

Follow him on Twitter and GitHub, and visit his homepage.

PurelyFunctional.tv: How did you get into functional programming?

Edwin Brady: I was taught Gofer (essentially a subset of Haskell) at the University of Durham in 1996, and I remember quite enjoying it then. It was only when I started postgraduate study with James McKinna and Conor McBride at Durham in 2000 that I really got into it, though. I was attracted by the promise of sophisticated type systems that meant if your program compiled, you'd know it was going to work. 16 years later, we've made some excellent progress, but there's still some way to go...

PF.tv: Very briefly, what is your talk about?

EB: I'll be talking about why "total functional programming" is important, and what it really means for a function to be pure. A total function is, essentially, one which is guaranteed to produce some output no matter what input you give it, so you know that it's never going to crash or go into an infinite loop.

I'll be using Idris, which is a purely functional programming language with first-class types. As an extended example, I'll show how you can define a type for describing concurrent, communicating systems and be sure, by writing total functions, that your concurrent programs continue running as long as they need to, always respond to messages, and generally perform as they're supposed to.

PF.tv: What do you hope people will take away from the talk?

EB: Two things:

• Purely functional programming is about more than referential transparency (that is, given the same inputs, functions always return the same outputs). We should only consider a function pure if it's guaranteed to produce a result for all possible inputs.

• Expressive type systems allow us to define models for safe, machine checkable, correct, concurrent programs which are guaranteed to be free of deadlock and race conditions.

PF.tv: What concepts do you recommend people be familiar with to maximize their experience with the talk?

EB: Some familiarity with Haskell or Idris syntax will be very useful. It'll also be good to know what is generally understood by a "pure" function, and by the concept of "total function", though I will explain both in the talk.

PF.tv: What resources are available for people who want to study up before the talk?

EB: You can find out more about Idris, and documentation including a tutorial. The example I'll be presenting in the talk is covered in depth in Chapter 11 of the forthcoming book, Type-driven Development in Idris. You can get an early access version (including that chapter!). All the code is freely available from there too.

PF.tv: Where can people follow you online?

EB: I'm [@edwinbrady]Twitter on Twitter, and you can also find me on the #idris irc channel on irc.freenode.net, as edwinb.

PF.tv: Are there any projects you'd like people to be aware of? How can people help out?

EB: Mostly, I'd like people to know about the Idris programming language so that they can contribute programs and libraries. It's primarily a research language but that's only because most of the developers at the moment are academics. There's no reason why it can't become a practical language for everyday software development, given an efficient compiler and good library support.

PF.tv: Where do you see the state of functional programming in 10 years?

EB: Concurrent, parallel and distributed computing are certainly not going to go away. Functional programming is already pretty go od at these, but I expect it'll only get better, and I hope the prospect of robust and secure distributed systems will attract more people.

Also, given that I'm interested in type systems, correctness, and total functional programming, I hope that we'll have learned to use types even more effectively in 10 years time and that we really will be closer to being able to say "It type checks! Ship it!" with a straight face.

PF.tv: If functional programming were a superhero, what superpower would it have?

EB: This is tricky because most superpowers involve unleashing side effects on the outside world. Pure functional programming, at least, is about describing and reasoning about effects rather than doing them. So I suppose that means its superpower is Omniscience: if you look at the type of a purely functional program you should know exactly what's going on!

Or does that even mean that its superpower is to control everyone else's superpower?