I’m currently in grand and lovely Edinburgh, Scotland for the whirling logical excitement of FLoC.  It’s really been worth the trip so far, and hopefully also for the rest of the Iowa contingent (Cesare Tinelli, Duckki Oe, Andy Reynolds, Harley Eades, and visiting Vilhelm Sjöberg have all been here or still are).  I’ll try to post a little bit about some of the great talks I’m seeing here, and maybe a little about some fascinating conversations I’ve had with some very sharp and knowledgeable people.

For now (and yes, I can’t sleep with the jetlag — it’s 5am or so and I’ve been up thinking about ordinals for 2 hours), just a little about the Partiality and Recursion (PAR) workshop this past Thursday.  There were a lot of talks that were very interesting to me, particularly all the talks on co-induction.  Thorsten Altenkirch was talking about mixed inductive and coinductive definitions (and hence, mixed recursive and co-recursive functions).  This seems like an interesting and important generalization, although I’ll have to read more to get a better sense for when we’d find ourselves needing this.  I quite enjoyed a very clever talk by Nils Anders Danielsson, currently postdoc’ing with Thorsten but — he tells me — starting soon as an assistant professor at Gothenburg.  Congratulations to him on that!  Nils was explaining how to implement some really alarmingly co-recursive functions — at least to co-recursion beginners like myself — essentially by defining a little language within the type theory for describing those programs, and then writing a co-recursive interpreter for them.  These functions can do things like pass parts of their output in simultaneously as inputs.  Wow.

I do have to say that the highlight for me was Conor McBride’s invited talk.  I had not met Conor in person before, though we’ve talked on email and recently in comments on this blog.  I had heard he was a very engaging speaker, and that was for sure.  He has a very watchable quality, as the West Wing TV show puts it (in I forget what season). His talk focused on some really elegant ways to structure programs so that their termination is made very apparent.  He uses a single parametrizable terminating recursor, where what you supply as the parameter is something that captures a particular terminating way of traversing your data.  He also pointed out a really nice dependently typed programming trick: if you’re trying to write a program called foo that takes in arguments a:A and b:B, say, and returns some output of type C (let’s suppose C is not indexed, although his method absolutely applies to that case), then the very first thing you do is define a type family (is that the right terminology?  I get a little confused about that) called Foo, as follows:

$\textnormal{Foo}\ a\ b\ \ :=\ \ C$

Why would you do this?  You do this so that when you are down in some case in your code, after doing a case-split on $a$, let’s say, you will see, from the type you are trying to inhabit at that point, what it is that you should be trying to do at that point.  Suppose the types A, B, and C are all nat, just for a simple example.  Then if you’ve case-split on $a$ and are in the $(S\ a')$ branch, the type you need to inhabit is

$\textnormal{Foo}\ (S\ a')\ b$

The point is, the very form of this type tells you: “Hey there! Right now, in case you forgot, what you’re supposed to be doing is giving the definition for foo with inputs $(S\ a')$ and $b$.”  As Conor said, the slogan for this approach to writing your code is “programming problems as types”.  Here, the programming problem is, define foo on inputs $(S\ a')$ and $b$.  I will definitely try this for the next dependently typed program I write.  Guru’s support for type definitions is pretty meager, but you could still try this out with what it has (and Trellys will not suffer from such limitations — once we have a type checker for the core language).

Anyhow, I very much liked this PAR workshop.  QA9 readers (who weren’t there in person) would have liked it, too: it was a termination (or actually more co-termination) paradise.  The organization was very well done, too, with a lunch already set up at a nearby restaurant and prepaid.  So people could all go together, and no one had to fuss around with bills and money and such.  It was quite great.

Tomorrow it’s some verification talks in the morning at IJCAR for me, and then working a bit in the hotel on some other pressing stuff.  Or maybe napping a bit after this sleepless AM…