How to be a Productive Programmer

Monday 14th November 2011

On Friday, I gave a talk at the Scottish Programming Languages Seminar (SPLS) at Heriot-Watt. Many thanks to Greg Michaelson for organising everything and giving me time to speak.

I've put the slides I used on-line as a PDF file (with two small fixes, see below).

The talk presents an extension of a Nakano-style typed λ-calculus with a delay modality for guarded recursion. In short, this means:

The type system presented has a type-former ▷ so that for any type A, there is another type ▷ A representing an A delayed by one step in the current time stream.
Unlike Nakano's calculus, where the delay modality is presented using sub-typing rules, I have followed Conor's idea and presented the delay modality using applicative functor rules. I think this makes it a little easier to program with, and certainly easier to experiment with in an existing language like Haskell.
The really exciting new thing is the addition of clock variables, which allows for multiple time streams to be in play at once. This means it is possible to look at “all” of a potentially infinite computation and extract useful information from it. In the slides I presented the take and replaceMin functions as examples of this.

As I mentioned during the talk, this is based on Conor's blog post Time files like an Applicative Functor from over two years ago.

The hoped-for outcome is a nice way of programming with codata in a functional language like Haskell. Still more hopefully, this will extend to systems with dependently types too, though I am still confused about where the clock variables ought to live.

I fixed two typos that were present in copy of the slides that I used in the talk:

On slide 18 (page 42 in the PDF), I had “Time Files like an Applicative Functor” as the title of Conor's blog post. Obviously, time is rubbish at filing, or at least not as good as applicative functors are.
On slide 28 (page 57 in the PDF), I had the semantics of data type descriptions as an endofunction on some undefined curly D thing. It ought to be the powerset of the semantic domain.