_tove recommended to me. I really like it.Also recently read:
Klosterman's "Eating the Dinosaur". This is a tough call. At his best (e.g. in the "Best Responses" essaylet, and talking about american football) he's just straight-up clever and funny. At his worst he seems to try a little too hard to mine exactly the same David Foster Wallace vein of footnotey moralizing-but-somehow-balanced introspection. On the plus side, the cultural references are 2000 plus or minus a few years (instead of ca. 1990 in the case of DFW) so I can't help but find it... comfortable in a certain way. But it's something to chuckle at, not the rich theology of tennis and genius and loss that makes you think about Life-and-what-it-Means-comma-man that I found in Consider the Lobster. (7/10)
Daniel L. Everett's "Don't Sleep, There Are Snakes". A collection of anecdotes about the author's work studying the culture and language of the Pirahã, a small tribe of people in Brazil whose isolated language is (allegedly) a counterexample to previously accepted universals about how languages work. Interesting observations and stories to be sure, though it feels a bit slopped-together at times. (6/10)
Pratchett's "Unseen Academicals". Oh this is just totally classic Pratchett. Great characters, silly and entertaining plot, ridiculous asides. And, ultimately, I think some nonzero insight about how professional sports plays a role in people's lives. (9/10)
---
In logic news, I had a good hour or two's meditation this morning over these notions of encoding modal logic into linear logic. I was afraid something would go totally awry with dependent types, because of the following line of thinking:
Linear pi doesn't work in a straightforward way. (I mean, see my thesis for how to dodge the problem without exactly coming up with the linear pi that you expected) Modal pi (as found in contextual modal type theory) does work in a more or less straightforward way. If modal stuff can be encoded as linear stuff, than where the heck does the problem go?But I realized that I wasn't looking hard enough at the problem's particulars. If you step through the encoding, it only ever creates lollipops in types and not in kinds and so avoids the dangerous territory of linear pis entirely. Moreover, if you push the result subsequently through the LLF-to-HLF encoding from my thesis, then what pops out has no occurrence of epsilon or * --- it's a very special case that doesn't make use of the algebra peculiar to linear logic at all.
What does this mean? I think it's that there is something extra-special about a "linear" context zone which by invariant there is always exactly one inhabitant of. If you have more than one of them, you need to have an operation like *, and then you need to decide whether it's associative, commutative, idempotent, etc. If there can be none of them, you have to have an epsilon and decide what sort of unit laws it might or might not satisfy with respect to * (witness the two different units and two different notions of "empty context" in BI). But if there's always exactly one, you can get away with no algebraic choices at all!
I think this reasoning has a chance, if developed further, of settling in my mind why intuitionistic logic's right-hand side, which is sort of "linear" from a Girardian perspective (or "modal" from a Gödelian perspective) is nonetheless more canonical than just a special case of classical linear logic (or classical modal logic).