Tony's Wiki

A note on Jsub-mu rule

3 min read

Instead of splitting

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

to

Positive parts:
	mu a. Int -> a
	mu a. mu b. Int -> a
	mu a. mu b. Int -> b

Negative part:
mu a.(
	(a -> Int)
	& (mu b.
		(Bool -> b)
	  & (b -> a))
)

We might want to leave the nested part mu b. (Int -> a) & (Int -> b) untouched.

The justification is that since the splitting on the LHS is exhaustive (considering nested recursion), we can always include the untouched part, and find (exhaustively splitted) left components to form a valid subtype for the actual negative part used in rule jsub-mu

How to prove soundness for this rule?

Consider some subtyping examples that cross nested recursion:

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

a not in fv_neg(Int -> (mu b. (b -> Int) & (b -> Bool)))
===> we get the ability to freely rewrite the substitution 
==> exists B' such that B' is part of B

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


(mu a. A1) & (mu a. A2) <: (mu a. A3)
  A1' [a- |-> {a : A1'}]
& A2' [a- |-> {a : A2'}]
<<
  A3' [a- |-> {a : A3'}]

a in fv_neg(A3)

show:

   (A1 & A2) [a |-> {a : A1 & A2}]
<: A3 [a |-> {a : A3}]

by IH, need to show
   A1' [a |-> {a : A1' & A2'}]
 & A2' [a |-> {a : A1' & A2'}]
<< A3' [a |-> {a : A3'}]



CounterExample: subtype then merge
  

js1 = inputTyp "(mu a. Int -> (mu b. a -> Int)) & \
              \ (mu a. Int -> (mu b. Top -> (Int -> Int)))"

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

ghci> (jsub (-1) js1 js2, tsubdp2 js1 js2)

(False,True)

The random test also reveals a (I guess) similar counterexample

  test/Translate/Spec.hs:233:13: 
  1) Meta properties of splitting for any subtype A of B, we can always find a merge-form of B such that A is subtype of the merge-form
       Falsified (after 450 tests):
         STypPair (mu a. (((mu b. (((mu c. (((mu d. ((mu e. Int) -> Top))) & ((mu d. (b -> (mu e. Int))))))) & (a)))) & ((mu b. Top)))) (mu a. (mu b. (((((mu c. (((mu d. ((mu e. Int) -> Top))) & ((mu d. (b -> (mu e. Int))))))) & (a))) & (Top))))

Conclusion

Well, it turns out that not only the optimization does not work, but we also need to refine the original rule so that it enumerates even more combinations, for a detailed note, refer to A note on Jsub-mu rule

Graph View

Backlinks