Tony's Wiki

Apr 17 - Meeting

4 min read

  • The fix on Siek’s algorithm seems working
    • we get a lot of timeout examples
A \in B
a notin fv_neg(A)
----------------------
mu a. A \in mu a. B


a in fv_neg(A)
----------------------
mu a. A \in mu a. A


[C_pos, C_neg] are part of A, 
			where pos/neg are divided based on 
			whether a appears (weakly) positively in Ci
C_pos & C_neg <: B
C_neg & B [  a -> {a : C_neg & B}] <: B [a -> {a: B} ]
---------------
mu a. A <: mu a. B
  • One source of timeout:
    • the positivity check

Attempt

One may try to simplify the mu-rule to: C_neg & B [ a -> {a : C_neg & B}] <: B [a -> {a: B} ]


[C_pos, C_neg] are part of A, 
			where pos/neg are divided based on 
			whether a appears (weakly) positively in Ci
C_pos & C_neg <: B
B <: C_neg (which implies that C_neg & B <--> B)
---------------
mu a. A <: mu a. B

However, this prevents some trans => Siek subtyping: e.g.


C_neg can be (Top -> ..)
while B can be an irrelevant type, say (Int -> ...)

then we can check with:
(C_neg & B)[{a: C_neg B&} / a] <: B [{a: B} / a]
but not
B <: C_neg



ghci> jsub (-1) (inputTyp "mu a. (((a -> Int) -> Top) -> a)") (inputTyp "mu a. (a -> a)")
False
ghci> tsubdp2 (inputTyp "mu a. (((a -> Int) -> Top) -> a)") (inputTyp "mu a. (a -> a)")
True

A possible fix? (to make the algorithm more precise)

relax the pos var check:

The fix is successful

Another counterexample:


  1) Jeremy Siek's BCD Subtyping translate => Siek (with recursive types)
       Falsified (after 4195 tests):
         STypPair 
mu . ((mu . (((1 -> mu . (I)) -> mu . (((mu . (I)) & (mu . (T)))))) -> ((mu . (((mu . (I)) & (mu . (I))))) & (mu . (mu . (((I) & (I)))))))) mu . ((mu . (((I -> mu . (T)) -> mu . (mu . (((I) & (T)))))) -> mu . (((((mu . (I)) & (mu . (I)))) & (mu . (((I) & (I))))))))

Simplify to:

tt1 = inputTyp "mu a. (((mu b. (((a -> Int) -> ( ((( Int) )))))) -> ((((Int)))))) "

tt2 = inputTyp "mu a. (((mu b. (((Int -> (Top)) -> ( ((Int )))))) -> (((((( Int) )) )))))"


simplity to:

tt1 = inputTyp "mu a. ((mu b. ((a -> Int) -> Int)) -> Int)"

tt2 = inputTyp "mu a. ((mu b. ((Int -> Top) -> Int)) -> Int)"


reason:

after unrolling a,
we get 
mu b. ({a: ....} -> Int) -> Int -> Int
<:
mu b. (TOPLIKE) -> Int -> Int

and can only be checked by nominal unfolding,
not B <: C_neg

Idea: also split on B?


Problem: how to deal with mu a. Top -> a <: mu a. (a -> a) & ...

An exponential blowup?

ghci> a
(mu a. (((a) & (a)) -> (mu b. ((((mu c. (((((((Int) & ((b -> Top))) -> (c -> ((((a) & (b)) -> ((((mu d. (((Int -> Top) -> b) -> ((Int) & ((((mu e. ((Int) & ((mu f. Int))))) & (d)))))) -> c)) & (Int))) -> (((Top -> c)) & (c))))) -> (b -> Int))) & (Top)) -> (mu d. c)))) & (Top)) -> (((((Top -> ((Top) & ((((((mu c. (Int -> ((((((((mu d. Top)) & (b)) -> ((Top) & (Int)))) & (((Int) & (Int))))) & (Top))))) & ((mu c. Int)))) & ((((((Top -> ((Int) & ((mu c. a))))) & (Int))) & (Top)))))))) & (Int))) & (((mu c. b) -> (Top -> ((b) & (a))))))))))
ghci> tsubdp2 a a
^CInterrupted.

Graph View

Backlinks