Some leads on contra-variant subtyping

[HuStmpHrrr]

In #127 , I removed contra-variant subtyping because I am not able to justify any termination measure for the subtyping algorithm in #124 . The major issue is that when checking the subtyping relation between return types of Pi, the context becomes smaller for the return type on the left hand side, so the normal form of that type is no longer accurate, c.f. #121 (comment) .

Nevertheless, I still think that contra-variant subtyping should be decidable, and this is the only blocker. As a proof of concept, I have shown in #125 that the subtyping relation in the PER model is transitive, so there really isn't any problem on the semantic side.

After some bangs on the wall, I think we can move forward with the decidability with contra-variant subtyping with the following leads. The main idea is that, the decision of subtyping decreases by the syntax size of normal forms, even if the normal forms are not accurate. Every time we go under Pi's, we re-normalize the return type on the left hand side, but if the size of the normal forms is invariant under subtyping between contexts, then we are good.

Now, the goal is to show that contra-variant subtyping doesn't change the size of normal forms. I think this can be proved, after we finish soundness proof. We need to provide another set of semantic definitions to model this invariant of size. I list a few critical lemmas and definitions below:

1. First, we should relate two domain values, if their readbacks have equal size. This is what the new semantic definition should eventually imply.
2. Then, we define an inductive relation between domain values a and b, such that when tagging a a subtype of that of b, then their readbacks have equal size.
3. We generalize the previous relation to evaluation environments, where the contexts are related by semantic subtyping.
4. Now we define semantic judgments. For example, for G |- t : T, we should say G is semantically well-formed, and then for all G' a sub-context of G, the evaluations of t in two different environments related by 3 is related by the relation defined in 2.
5. Instantiate the judgment in 4 will hopefully give us a proof of normal forms having equal size.

It involves some work, probably not gonna be easy, so we should finish what we have now before moving towards this direction. Leave this investigation for the future; if we pull this off, we can write another paper about it.

[Ailrun]

I think we need something really clear, as once we extend the system with contextual types, we have another source of contravariance. Once POPL deadline is over, I will also put an RFC with my idea. (Possibly as a comment in this issue)

[HuStmpHrrr]

I think we need something really clear, as once we extend the system with contextual types, we have another source of contravariance. Once POPL deadline is over, I will also put an RFC with my idea. (Possibly as a comment in this issue)

contextual types might not cause issue. LF is a separate system, it doesn't have to support any subtyping at all.

[Ailrun]

it doesn't have to support any subtyping at all.

Ah yeah, true. But anyway, I think it would be a good idea to have the way as cleanest as possible we can come up with to block as less future extensions as possible.

[Ailrun]

I tried to prove this theorem (of course it didn't change PER itself to use contravariance so it is not super meaningful even if it is proved, but), and from that, I think what we need is basically the "realizability" of per_subtyp.
https://github.com/Beluga-lang/McLTT/blob/889fd8e4b4c952b7d54ae6390972f720fb313cbd/theories/Core/Completeness.v#L83-L86

Here, {{ ⊢ Γ' ⊆ Γ }} so length should be the same, thus once we have forall s, exists W W, {{ Rtyp a2 in s ↘ W }} /\ {{ Rtyp a1 in s ↘ W' }} /\ {{ ⊢anf W ⊆ W' }} (* or similar syntactic simple judgement *) like per_top_typ then we can almost prove the theorem. After that, I think we can adjust PER to use contravariant subtyping and other proofs according to that.