Paper(s) of the day: Building and Translating

Okay, so I'm going to write about two papers today. The first is Build, Augment, Destroy Universally and the second is Verifying Haskell Programs Using Constructive Type Theory, which I didn't even remember downloading. Slightly odd!

So the first paper is actually really cute. So most functional programming peeps know that initial algebras give you the basic semantics of folds for datatypes in a language where types are defined inductively*. This initial algebra semantics also gives you the convenient fusion laws that a compiler can use in order to improve performance. Now, the major contribution of the paper is to show how for (co)inductive types you can consider the initial algebra(terminal coalgebra) to also be a (co)limit of a forgetful functor and that you get the build/destroy operators which help you build an entirely different kind of fusion law! I think it's really cute and the math is pretty simple. I think I'd like to try writing some small interpreter with explicit build/fold/etc keywords built in for the datatypes. 

The second paper is from back in 2005 and uses oldskool Agda, not Agda2, and came out pretty close to the paper I mentioned last night that uses coinduction to embed general recursive functions. Something I'm still turning around in my head it's cool for them to use Maybe as a monad for partiality when, as discussed in Capretta's paper, that's not really sound because it allows you to "decide" whether or not programs terminate which means that you can't really be talking about the computable functions. Maybe I'm just missing something? In any case, I need to look and see if people have tried to extend/update this translation for Agda2 since it actually has coinduction. One thing that bothers me a little is that I can't find them explain their restrictions on Haskell datatypes that are allowed. Clearly they can't shallowly embed all Haskell types, because then you'd have a copy of the untyped lambda calc as a type in Agda which is just a little unsound logically.

There's some other things that I was thinking about and working on today - mostly picking up some pieces about the idea of a Pointed typeclass and thinking about how one would automatically translate a set of definitions for Haskell/Habit typeclasses into inductive universes in type theory. It seems a bit better than System F dictionaries...but that's just a gut feeling. I actually need to read about such translations a bit more. 

Tomorrow will, hopefully, really be about logical relations. :-p

* Yes, in Haskell things are a bit conflated between induction and coinduction because initial algebras and terminal coalgebras are the same thing in most models of Haskell-ish systems in categories of complete partial orders.