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'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.
As an update, someone just let me know that the idea of n-categoric semantics for OTT is a reasonable idea and that, in fact, Thorsten Altenkirch is currently working on it.
ReplyDeleteTo be more precise, you'd have to change the syntax of OTT if you wanted it to describe higher-dimensional types. The reason is that OTT has a rule of proof irrelevance, which says that any two proofs of equality are themselves equal. For higher-dimensional types, this isn't true: there can be different "proofs" of equivalence between the same two terms, which have different computational behavior. For example, if you take equivalence at a universe (type of types) to be isomorphism, then Bool is isomorphic to Bool in two different ways (identity and 'not'). The definition of OTT exploits this proof irrelevance, so you'd have to work harder if you wanted to make it work for higher dimensions.
ReplyDeleteFor the semantics of OTT, see http://www.cs.nott.ac.uk/~txa/publ/lics99.pdf
(which actually predates the syntax, but it's the same kind of type theory). The basic idea is that a type in OTT describes a setoid (a type equipped with an equivalence relation), which is of course a special case of a groupoid.