If [X+/- -> C] A << [X+/- -> D] B
then
(1) C << S << T << D => [X+/- -> S] A << [X+/- -> T] B
(2) D << T << S << C => [X+/- -> S] A << [X+/- -> T] B
Question 1: Can we further generalize this lemma?
- generalize the form of S and T
- might need the constraint C <: D?
- more direction of subtyping? or the direction is already subsumed by C and D
- think so…, since we don’t have constraint for C and D
- no? the reason why this lemma works is due to polarized substitution Question 2: Does this lemma follows from substitution + transitivity?
A dual lemma? NO
If [X+/- -> D] A << [X+/- -> C] B
then
(1) S << C << D << T => [X+/- -> S] A << [X+/- -> T] B
(2) T << D << C << S => [X+/- -> S] A << [X+/- -> T] B
The Case in Distributivity
[X- -> {a : A}] A << [X- -> {a : B}] T
where B <: T
(A is not necessary <: B)
A can be freely rewritten to any A' << A
The lemma is looking for
A << ? << ? << B
B << ? << ? << A
to get
[X- -> {a: ?}] A << [X- -> {a: ?}]T
but the condition gives not such types