Papers of the Day: Moar Types

This is the second day of my binging on type theory. For today's reading I read the first couple of chapters of Dan Licata's thesis, Hoffman & Streicher's paper on groupoid models of type theory, and Altenkirch's original paper on OTT. 

As far as the thesis went, I only read the introduction and the background chapters so I haven't gotten into the heart of it yet. Funnily enough, the background chapter did have some food for thought in the distinction between derivability and admissibility. I don't know if this is a common way of looking at things that I would have seen if I had ever really taken courses in logic, but in any case I think it makes a lot of sense. I'll probably try to read a chapter three tomorrow.

Alright, so now we come to the things I'm still chewing on. First, there's the Hoffman & Streicher paper. The basic point of the paper was really about proving that uniqueness of identity proofs doesn't follow from intensional type theory by constructing a model where it didn't hold, but I can see that there was some deeper insight in terms of using groupoids to model types - setting the stage for the later omega-groupoid models which I intend to read about tomorrow - as well as it being a good illustration of the general technique of constructing models to help determine if a property of the logical system is necessarily true. I'll probably review some of the constructions again tomorrow, though, before I read some of the papers on omega-groupoid models.

Speaking of models, that's the main thing I've gotten so far out of the other Altenkirch paper: the idea that one can construct a model of your proposed theory within another type theory to determine if it is even possible to make. I think there's more I should be getting out of it, but honestly it was the last thing I read today and I was a bit burned out. I think I'll put it back on the pile for tomorrow for another attack.

Paper(s) of the day: Type Theory Frenzy

Today was my first real day back in graduate school, starting my "second"* year and I had a meeting with my advisor where we discussed what my focus for the next few years will be so that I can start publishing and graduate. 

The idea I had over the weekend was to really dig into the cutting edge of type theory. It's got math, it's foundational, and it's relevant to mechanizing all the mathematics I love so much. It makes a lot of sense as a direction to go in. Of course, the next task was to figure out where the edge is so that I can start pushing. 

I started with two papers on observational type theory and a survey on homotopy type theory. 

I'm still very much processing what I read today, but I'll try to summarize things to the extent that I understand them.

First, let's discuss observational type theory. As background, consider the difference between intensional and extensional type theory. In both, you have a propositional equality defined by a constructor representing reflexivity and a definitional equality used by the typechecker that compares the normal forms of the objects in question. The difference between intensional and extensional type theory is if you are allowed to use the propositional equality as a witness for the definitional equality, making it relevant to typechecking! This has the well-known effect of making typechecking undecidable as well as making execution hairier business by allowing ill-formed terms to typecheck in a context that contains falsity, thus also allowing them to be evaluated. I know that some people have found ways around the scary bits of extensional type theory in order to exploit the good properties it has, but I think it's not controversial to say that neither intensional nor extensional seems terribly satisfying as a stopping point. Now we come to observational type theory, which attempts to hit a sweeter spot that has more of the power of the extensional theory (e.g. functional extensionality) but doesn't lose the computational properties of the intensional theory. How? Well, I don't think I have a good way to explain it than thus; observational type theory is based off of a heterogeneous equality, based on coercions, that takes into account the actual type structure what is being compared - allowing for a term to be safely "cast" between two types exactly when the two types are "equal" computationally. Basically, it respects a notion of iso between types instead of a more evil (in the technical sense, mind you) equality. They don't quite put it that way in the two papers I read, but it seems like the way to take things. Having this less evil notion of equality allows us to have our cake and typecheck it too. The actual details of some of the coercions seem both a bit over my head yet not terribly exciting. I hope to scrutinize the actual Agda implementation a bit in order to get a feel for the way the isos are constructed.

Alright, well speaking of isos now we come to homotopy type theory. From what I can tell homotopy type theory is, at the moment, an exploration of the connections between intensional type theory and higher-order category theory. For example, the structure of identity proofs over a type - including identity proofs on the type of identity proofs and the type of proof on the type of proof on the type of proofs on ... - has the structure of a weak omega-groupoid, a kind of "group-like" structure whose each level obeys certain laws only up to transformations by the next level up, in a way very similar to the actual omega-groupoid generated by the tower of homotopies on a space. I'm still really shaky on what's going on here, other than the fact that work done over the past 2-3 years has started to solidify the idea that generalized "homotopy-like" spaces are (probably?) sound and complete models for intensional type theory, meaning that type theory is the internal language of homotopy theory. The main thing that excites me about this is that it puts words to a gut feeling I had when I first started to learn type theory as I was getting into CS. My background at that point was a mish-mash of diff geo and category theory, and the relationship between operational and denotational semantics (for example) reminded me very much of two categories - leading me to an old paper by R.A.G. Seely that maybe I'll ramble on another time - and I wondered what higher order transformations might mean. In my head it looked a lot like, well, homotopies! I know that's a little different than the situation we're talking about here with homotopy type theory, but I'm excited to think that my first loves in mathematics have deep connections to CS & logic.

What about models of observational type theory? Do they also have rich higher-order category theoretic structure? I don't know! I'd like to know, whether that means I investigate myself or read someone else's work! Someone directed me to a recent dissertation on directed type theory which, I guess, is an approach to type theory based on higher-order categories without the restrictions to groupoids.

* Technically, third, but I lost roughly a year total due to medical stuff & some heinousness and thankfully my department is respecting that these events were pretty much outside of my control.

Paper of The Day: Monads

Okay, so since I was travelling for five hours for Memorial Day weekend then I wanted to do something kind of easy in the car on the way here.

It's a paper that everyone should have (and probably has) read: Moggi's paper on monads and the computational lambda calculus.

The most basic point of this paper is a pretty well known story: strong monads act as generalized let-statements in the internal language of a category. Why do they need to be strong? Well, the strength essentially acts as a way of ensuring that you can "copy" the context from the binding part of the let-statement to be available in the final expression.

Okay, yay, monads!

Well, no, there's more to it than that. One thing that really jumped out at me when I was rereading this paper in the car was the methodical, elegant development that built up the internal language alongside the models by adding richer categorical constructions. It was really cute, but also an approach I see very rarely done in CS literature even though to me it feels very constructive and enlightening. I feel like that's the kind of approach I want to have to my own research once, y'know, I actually start publishing (*cough cough*).  So, anyway, even if you already know the whole story of using monads in semantics I think there's something to be said for sitting down and working through this paper. It's really well structured, which I think is probably a good bit of why it was influential.

Paper of the day: Category Theoretic Solution of Recursive Domain Equations

Okay, this paper was a reread but it was something that I needed to digest better than the first time. Smyth & Plotkin's classic paper. So what's the point of this paper?

Okay, so Dana Scott had this classic result where he built - as a colimit - a domain D\inf (think partially ordered set with some nice properties) that was isomorphic to the set of continuous functions from D\inf to D\inf, thus showing a particular technique in domain theory for building models of the untyped lambda calculus. Another way to put this is that D\inf is the fixed point of the functor F(D) = D -> D.

Well, the problem is that the original construction is fairly rigid, taking place only in a particular category of domains. So the point of this paper is try generalize it to all categories and functors that satisfy certain properties. So what properties do we require?

Well, first we can generalize the notion of omega chain from domain theory to category theory. It's basically the same thing if you think of an arrow from objects A and B to be the same as "A < B", so it's a countable diagram of objects with an arrow leading from the previous to the next object in the sequence.

So then what's a omega-continuous functor? Well, it's a functor that maps colimits of omega chains to colimits of the omega chain induced by the action of the functor. It's basically the interchange of function and limit we're used to from domain theory. Yay!

So the paper establishes one thing right off the bat: if you have a continuous functor and colimits of omega chains exist, then you'll have a fixed point of that functor. So the problem becomes figuring out when you have an omega-complete category.

However, requiring that the category we work in be omega-complete is actually a bit more restrictive than we want. Instead, we work in what are called O-categories which are categories enriched CPO. The bulk of the paper is about showing how most O-categories allow us to find the colimits in the subcategory of embeddings, which has nicer properties and can more readily be omega-complete, and then pull those colimits back to the original category.

It's actually really cool to work through, although I feel like I haven't done the best job of explaining it! The math isn't terribly deep diagram chasing, so if you're at all familiar with category theory you can follow it with a bit of work. I'll confess, though, that the first time I tried to read it I was sitting and scratching my head wondering that the point was, but the point seems to basically be that by generalizing the D\inf construction to its minimal requirements you can get away with using slightly weaker categories than used to be considered prior to this paper.

Paper of the day: Lawvere Theories and Monads

Okay, so stuff on logical relations still isn't sinking in today and I'm feeling pretty foolish. So, let's get back a little more on my home territory: category theory. Specifically, a paper from a few years ago from Hyland & Power about Lawvere theories and their connection to computer science.

Okay, so first off what's a Lawvere theory? Well, basically, it's a category with only one "base" object that generates all other objects via finite products of the base object with itself. Each such category, up to iso obvs, corresponds to a single-sorted algebraic theory. There's a good explanation of them here that I recommend reading. In order to "get it" I had to work through their example of the theory of groups and sketch out the equivalence.

...so, what's the connection to computer science? Well, first let's go back to monads. Err...real monads, not the burritos that appear in the over 9000 Haskell monad tutorials. So, in Moggi's work monads were useful because they were - basically - generalized let statements. These let statements allow us to sequence effects in our computations, such as state, IO, etc. which is really useful for describing the semantics of a language! Okay, but what about the actual morphisms that perform the side-effects? Well, they're left out in the cold so to speak. They're called "non-proper" morphisms and are subject only to some naturality conditions. Now, to be fair, that's nothing to sneeze at but it doesn't capture most equations you would want: just the bare minimum to make sense.

Well, the neat thing is that if you describe side-effects by their operations as some kind of Lawvere theory, you can recover the monad of side-effects as a coend that kinda "rolls up" all the operations into the structure that they operate on. That description wasn't very good, was it? I'll have to think of some better picture at some point. Now, since monads are a more general structure than Lawvere theories you get a bit of a loss of information, i.e. the less stringent equations on operations; however, it does mean that from a more rigid description we can recover the "generalized let" we want from sequencing.

Now here's where I get murky - I haven't done any serious examples so I don't see entirely how one would directly use this to describe the semantics of a programming language with side-effects. I get conceptually that it's more specific, but I'm not entirely clear on how much it buys you and if its worth it. I probably need to read the half-dozen papers written by Plotkin et al. on the topic. :-p

Now, okay, so I've told a little bit of a lie so far - if one does these constructions in "ordinary" category theory, this whole trick of recovering the monad from the Lawvere theory only really works on the category Set, which isn't terribly useful for programming languages that allow general recursion...instead, we have to move over the enriched category theory which I'm still wrapping my head around.

The basic point of enriched category theory is that rather than having sets of morphisms, one has hom-objects from another monoidal closed category. The normal rules about composition still, basically, hold the way you'd expect in the hom-objects. Again, the nitty-gritty of what changes in enriched category theory is lost on me at the moment; however, I know that there has been work to rebuild the work on Lawvere theories in the enriched setting and that this is what's actually used in the Plotkin et al. papers.

So, yeah, this was a bit longer than I intended but I had a lot to talk out with this paper.

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.

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.

Paper(s) of the day: Bananas

Okay, so as I said I would I ended up reading Bananas, Envelopes, and Barbed Wire as well as Bananas In Space.

Wow, so I don't think the original paper has aged well in some ways. The notation and equations are very different than any other way I've seen the material presented, and it's no wonder I feel like I didn't get much out of this paper five years ago when I was just learning category theory and knew essentially no computer science ("Oh, so you know computer science now?" "Stop that, Caylee!"). So, I read Freyd's papers on fixed points of functors a lot more recently and I think they're clearer if much harder to find. I've never found them available on the Interwebz, but I grabbed copies from my university library. There's no category theorists at Portland State, but we have copies of the category theory journals. Go figure!

So, anyway, the original paper is cute from a historic perspective as it shows how natural fusion laws from the category of sets and functions can be extended to the the categoy of cpos with some strictness side conditions. It basically says, but doesn't show with commuting diagrams, that these laws come from universal mapping properties of limits and colimits.

The Bananas in Space paper is really cute though because it shows how to describe these constructions as Haskell (well, Gofer...) code. The punchline is giving a demonstration of Freyd's difunctors as code. Which, honestly, makes sense if you think of Haskell programs as existing in some subcategory of CPO that's clearly going to be enriched in the ways that Freyd's work needs. I mean, clearly, that's not really rigorous math but it's a really cute example of the construction.

So what did I really gleen from these papers? Well, I guess I didn't pick up stuff that I hadn't already known about. I suppose one thing I'm wondering about is why I haven't seen more systems for reasoning about programming languages using equational methods like these. I have seen papers talking about how you can do it, but I haven't seen many mechanized systems for doing the work and proving serious properties of programs. I've wondered before if that's because most of the languages we'd want to reason about don't have a formal semantics.

I think I just made an argument for why I need to get back to working on a semantics for Habit...*scurry scurry*

Tomorrow will be reviewing Plotkin's generalization of the D-infinity construction as well as Pitt's original paper on logical relations.

Paper of the day: Design Patterns as Higher-Order Datatype-Generic Programs

So for tonight's studying I decided to read something almost entirely unrelated to semantics and read the journal version of Jeremy Gibbons's paper, available online here. So, yeah, I guess this was really the clearest explanation of some of the tricks involving bifunctors and explicit fixed points that I've read. 

The whole punchline is really on page 13, but he spends the rest of the paper explaining how these constructions relate to the iteration patterns from OO programming. It's pretty cute and despite having used Haskell off and on for a few years, I'd never really written any examples with the generic fold, unfold, hylo, and map operations.

Reading this also made me want to go back to the old "bananas" papers which I haven't read since I was trying to decide if I actually liked this whole computer science thing a few years back, just after burning out of grad school in a completely different field. (Spoiler alert: yes, it turned out that I liked computer science a lot.)

I think I'll read the original bananas paper tomorrow, and then maybe get back to some things a bit more relevant to my actual research after that. For example, I want to read that paper about safely including partiality via coinduction. That felt like a jargon-y sentence. Ouch.