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)
Guy from Seattle team we've been working with showed up today at work; no matter how much I'm generally comfortable working with remote teams (and I…
-
(no subject)
Sean's back in town --- good fun working with nonremote teammates.
-
(no subject)
Played some board games at the fb office with newly-arrived-to-nyc dan blandford and some friends-of-friends of his. Codenames and…
- Post a new comment
- 0 comments
- Post a new comment
- 0 comments
