Apr 3 - Meeting

Weakly Positive without reflexivity

-- posvar2 k i m (SMu a) (SMu b) | a == b && not (elem i (fvtt a)) = Equiv
-- we hope to eliminate the above rule by tracking Equiv on the fly
Strict | Equiv | EquivCons | Fail
 
posvar2 k i m (SMu a) (SMu b) = 
    -- first check the weakly positivity of the two mu types w.r.t. their binders
    let bres = posvar2 (k-1) k True (opentt a (SVar k)) (opentt b (SVar k))
        ares = posvar2 (k-1) i m (opentt a (SVar k)) (opentt b (SVar k))  in
    case bres of
        Equiv -> ares
        EquivCons -> case ares of
            Equiv -> 
                if i `notElem` fvtt a then Equiv else EquivCons
                -- EquivCons 
                -- to allow for a in mu b. b -> a and mu b. b -> a
                -- and not forbids mu b. b -> Int and mu b. b -> Int
            EquivCons -> EquivCons
            _ -> Fail
        Strict -> ares
        _ -> Fail

The weakly positive rule in the source type:

a ∈m  A <:  B
b ∈+  A <:  B
----------------------
a ∈m μ b. A <: μ b. B


a notin fv(A)
A = B
----------------------
a ∈m μ b. A <: μ b. B

Distributivity

The double environment check is random-tested, though not useful

A counterexample

Despite
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. String -> b)
<:
    mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. String -> b)) 
<: merge
    mu a. Top -> (mu b. b -> Int & Bool -> b & String -> b)
<: subtyping
	mu a. a -> (mu b. b -> Int & Bool -> b & String -> b)

It is not true that:
   ...
<:
	mu a. a -> (mu b. b -> Int & Bool -> b)
&   mu a. a -> (mu b. String -> b)         

<:  mu a. a -> ((mu b. b -> Int & Bool -> b) & (mu b. String -> b))

<: 
	mu a. a -> (mu b. b -> Int &  Bool -> b & String -> b)
	
-- because the merge within "mu b." is strict 
-- not equivalent, it affects "mu a."

-- we must merge then subtyping

Observation I: We were imprecise about being “weakly positive”

Weakly Positive in the translated type != Weakly Positive in the source type

on the source level, a is not weakly positive in
a ∈+ Top -> (mu b. String -> b) <: a -> (mu b. b -> Int & Bool -> b & String -> b)
on the target level, in the translated type there are no negative reflexive comparison of a, so we called it weakly positive

The weakly positive rule in the source type:

a ∈m  A <:  B
b ∈+  A <:  B
----------------------
a ∈m μ b. A <: μ b. B


a notin fv(A)
A = B
----------------------
a ∈m μ b. A <: μ b. B

The top-down reasoning with translation gives us no information about b ∈+ A <: B

It is not direct that a ∈m |A| << |B| implies a ∈m A <: B (assuming a proper definition of equivalence, intersection, distributivity, etc.)

Observation II: The strategy we expected is not actually working

The old idea: By inversion on A [a- |-> {a : A}] << T [a- |-> {a : B} ], where T ∈ spls(B), we either know that:

a ∈+ A << T, so that we can let the source type mu a. T' be the intermediate invertible type

this fails now! since weakly positive is not preserved under backward translation

a is negatively compared reflexively, so we get B << A << T, in this case we can let the intermediate type be just mu a. A, since A contains fields that are already in T, by applying the lemma on all the splitted T’s, we can ensure the intermediate invertible type for all splits all components in B.

i.e. we expect A << Bm1 & Bm2 & Bm3 ... & Bmi << T1 & T2 ... & Tn == B

where the first subtype relation is obtained from the inversion lemma

and the second subtype relation Bm1 ... Bmi << B is only by distributivity

However, the counterexample shows that:

	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. String -> b)
<: merge
    mu a. Top -> (mu b. b -> Int & Bool -> b & String -> b)
<: subtyping
	mu a. a -> (mu b. b -> Int & Bool -> b & String -> b)

The strategy we find is wrong! e.g. for the component:

[a. Top -> [b. String -> b] ]               -- second intersection
<<
[a. {a: ...} -> [b. String -> b]]           -- third split

The intermediate type we proposed was:
mu a. a -> (mu b. String -> b)

but the counterexmaple shows that it cannot be merged with the other Bm

The Ultimate Question: what is the strategy of finding the invertible intermediate type?

Some ideas

The generalized unfolding lemma
introduce Well-bound context (See QuickSub Proof) to generalize the weakly positive restriction
Case analysis on single-sided negative variables: mu a. A & mu a. B == mu a. A & B if a does not appear negatively in A and B. See Intermediate Type from Left
- However, for other cases, we cannot do much with only knowing that a appears negatively in A1, it is not necessarily compared with negative a in B, we may get no condition in this case
One algorithm on the source type to try

mu a. A & mu a. B == mu a. A & B if a does not appear negatively in A and B.

mu a. Int -> a
mu a. Bool -> a
==
mu a. (Int -> a) & Bool -> a
==
mu a. Int & Bool -> a




mu a. A & mu a. B < mu a. A & B 
if `a` appears negatively in `A` or `B`, unless A and B are equivalent


mu a. A1 & mu a. A2 & mu a. A3 <:  mu a. T1 & A3 <: mu a. (T1 & T2)


 mu a. (T1 & T2) ~~> [ T1 [a- -> {a : T1 & T2}] ] & [ T2 [a- -> {a : T1 & T2}] ]



| mu a. A1 | << [ T1 [a- -> {a : T1 & T2}] ] = [ T1 ]

| mu a. A3 | << [ T2 [a- -> {a : T1 & T2}] ]

If a does not appear neg on RHS, pick from RHS
otherwise, pick from LHS

Tony's Wiki

Explorer