One of those days

My update for the day is fairly skimpy. I skimmed "A View From The Left", started a paper on the omega-groupoid interpretation of ITT, and subsequently tripped over my lack of intuition about operads and landed flat on my fibration. I think I sprained a syntactic category, or something equivalent to it.

In all seriousness, I clearly need to read some relevant chapters both from Jacobs's Giant Yellow Book and from Leinster's elaboration of operads and higher-order categories. I was skimming along fine with my current level of mathematical knowledge, but need to buff up a bit now. I've read a bit of the machinery for the syntactic category of a dependent theory but it was long enough ago I can barely hum the tune. I probably could have faked it slightly better today had I slept well, but it was one of those days when I woke up <6 for no apparent reason.

I did, though, see a talk about relativistic programming and chatted briefly with one of the grad students working on it. It turns out that their last submission outlines a kind of induction principle for reasoning about concurrent programs that use their primitives for blocking. I was told that they hoped someone could pick up the note and mechanize the reasoning in some fashion, but I was good and didn't offer up my services. :-) Maybe it'd be a cute thing to do at some point during my PhD, but at the moment I'm too excited about digging into OTT/HTT/etc.

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.

Talking Things Out

Okay, so I'm starting what is essentially my second year of my PhD. Err...there's kinda personal reasons why I was only enrolled for one quarter this past academic year, but suffice it to say that things are resolved enough that I'm starting back up again.

I don't think I've explicitly said where I am and what I'm doing, though. So, to get things out of the way I'm a student at Portland State University. You may not have heard of it. That's okay, I hadn't either but I came here because of the HASP group. Formerly the Programatica team that brought you things like House. Since my interests are in logic, formal methods, type theory, and all that my piece in the research team is to work on defining the semantics of Habit, the language our team has designed and is building a certified compiler for. It's a Haskell-ish language that's strict, has a more interesting typeclass system, and is missing a number of type system extensions that - while interesting in terms of language design in Haskell - aren't really needed for Habit and would just make the semantics and compilation more annoying.

My background really isn't in computer science, it's mostly math and physics, and I didn't start programming until I was in my early 20s. So, I'm not the most typical candidate for a PhD in CS but that's how things go! 

I used to be a bit intimidated by technical blogging, but after the past couple of years the idea of someone randomly showing up in my personal writing space and picking a fight with me just isn't scary anymore.