I think I've proven it, now. It required tweaking the typechecking algorithm. I was sitting in Sam's alternating between trying to find a counterexample, trying to prove it, and taking bites of the sandwich. I paused for bit to think about soundness, and realized that for it I only needed the types of an irrelevant function and its argument to match up in the promoted context, because I can type-convert to the `good' type in that context, and then fall back down into the irrelevant typing judgment. So I tried proving completeness for the weaker assumption that the types are equal in the stronger context (whee, contravariance) and succeeded! Assuming I didn't fuck anything up, anyway. I should ask Frank to proofread my, uh proof, probably.
...make lemma-nade.
I think I've proven it, now. It required tweaking the typechecking algorithm. I was sitting in Sam's alternating between trying to find a counterexample, trying to prove it, and taking bites of the sandwich. I paused for bit to think about soundness, and realized that for it I only needed the types of an irrelevant function and its argument to match up in the promoted context, because I can type-convert to the `good' type in that context, and then fall back down into the irrelevant typing judgment. So I tried proving completeness for the weaker assumption that the types are equal in the stronger context (whee, contravariance) and succeeded! Assuming I didn't fuck anything up, anyway. I should ask Frank to proofread my, uh proof, probably.
-
(no subject)
Fun talk by Sara Soskolne down at Cooper about the maximally fiddly bits of designing Gotham and Quarto.
-
(no subject)
A nice long essay full of typography found on Broadway: http://www.hopesandfears.com/hopes/culture/design/216855-typography-of-broadway-from-a-to-z
-
(no subject)
More stuff happened: Tried to find a typisch deutsche döner kebap, but we only came across an outdoor stand with no real seating to speak of,…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments