Paper of the day: General Recursion Via Coinductive Types

Okay, so I read bits and pieces of a number of papers today - a bit of a draft by Conor McBride, the recent arrows papers by Lindley et al (just cuz...not because they're relevant to my research at all), one of the first containers papers by Abbott et al, reread Build Augment Destroy, but actually read all of this cool sounding paper by Venanzio Capretta General Recursion Via Coinductive Types. So, yeah, I think I'll talk about that instead as my Paper O' Teh Day.

So, basically, this paper describes in great length the trick for actually describing the lifting monad constructively in type theory. Basically, the idea is that you use a coinductive type to represent partial computations. You can then show that you can embed the partial recursive functions into your type theory as functions on the lifted type. I feel like that was a really crappy way to describe that, so let me try again.

So in order to have a logically useful type theory you probably want to restrict yourself to only normalizing terms (...you don't have to, by the way, but implementation gets interesting). General recursive functions, naively encoded, aren't necessarily normalizing. What to do!? Well, you use coinduction to describe a potentially non-terminating function by the explicit process of stepping through the computation...and since this is coinduction, there can be an infinite number of steps!

So, basically, that's how you encode general recursion into it. There's more details related to how the Y-combinator works that I feel like I haven't entirely grokked, but I want to try and implement some of this structure in Agda. What's nice is that once you have your encoding of the computable functions this way, you can start building up some actual domain theory. Which I have just a tiny bit of interest in, coincidentally!

Okay, so for tomorrow I should finish the build augment destroy paper and the initial semantics is enough paper. I kinda want to write a little implementation of a small language that has actual fold/build/etc. keywords as a proof of concept for something I want to propose for the Habit language.