Jason (jcreed) wrote,

Mildly frustrating day with work and stuff. Instead of complaining further about it I will tell the story of a cute small puzzle that I think I might have come across years ago, (I think in the form of Frank being skeptical of the use of HOL and impredicativity in authorization logics, because you get unexpected results, if your expectations are not carefully enough tuned to reality) but it popped up during PLClub last Friday, so I will share it with you.

Suppose you're working in some System-F like language, and you try to think of Leibniz equality in a propositions-as-types way, like you want to define X = Y at type τ as

eq(X,Y) = ∀ P : τ → * . P X → P Y

where * is the kind "type". In plain english, for every property that X has, Y also has it. You might ask (as someone did during PLClub) hey, isn't this definition asymmetric? Shouldn't we say also that for every property that Y has, X also has it? The speaker said, ah, well, the property of not P is also a property, so we just substitute that in and we're good.

I thought to myself, gosh, that's an awfully classical way of thinking about it. Since we are bein' all propositions-as-types here, isn't there a more constructive way of doing it?

Yup. It still feels like simulating a sort of negation, but it's fully constructive for sure.

Okay, so we want to show that this definition actually is symmetric, despite appearances. So we have to build a term of type eq(X,Y) → eq(Y,X), or in other words of type
(∀ P : τ → * . P X → P Y) → (∀ Q : τ → * . Q Y → Q X)
where we are just alpha-varying P to Q in the second copy of eq to keep things separate.

The term is

λ q : (∀ P : τ → * . P X → P Y) . Λ Q : τ → * . &lambda y : Q Y. q [λz. Q z → Q X] id y

What's going on is that we instantiate the known equality "from" X to Y — that is, the implication from P X to P Y — by substituting λz. Q z → Q X for the predicate P. This plays the role of negating Q, but we're not really flat-out negating it, we're just putting it in an implication towards Q X.

Now our next obligation is to show that P X holds, which after substitution means showing Q X → Q X. But that's trivial, so we prove it with the identity function id. What we get out is P Y, or after substitution Q Y → Q X. But Q X is exactly what we want, and Q Y is what (in the form of y) we have. So we're done.

Impredicative polymorphism sure is wacky, isn't it?
Tags: math, system f
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded