Tony's Wiki

Some careful thoughts on splitting RHS

6 min read

It turns out that the fix in A fix to Jsub-mu rule is not enough. Let’s consider some examples in this post:

Expected Properties:

  1. For a valid split of the right type, it should be a subtype (not necessarily equivalent) of the original type
  2. Among all the splits of the right type, we should be able to find a split such that its merge is equivalent to the original type (otherwise reflexivity is not satisfied)

Design Space

  • negative types should still be split, as the component may be compared with Top -> ... on the LHS (the subtype then merge pattern)
  • When negative variables are concerned, we should retain the original type, otherwise we may lose the original type
    • todo question, what negative variables? the top variable or the variable of each layer? or we need to iterate both as they are both valid?
    • when should the negative variable check be done?

Example 1

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

Here are some valid splits of the type:

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

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

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

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

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

Each are non-equivalent to each other, but are all subtypes of the original type

Example2

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

If we split eagerly, we don’t get original type. The split result can be quite non-trivial in this case.

  
 
ttc = inputTyp "(mu a. (mu b. ( Int & (b -> Int) & (a -> Int))))"
 
ghci> filter (\xs ->  not $ tsubdp2 (foldl1 SAnd xs) ttc) (psplit (-3) (-1) ttc)
[[(mu a. (mu b. Int)),(mu a. (((mu b. (b -> Int))) & ((mu b. (a -> Int)))))],[(mu a. (((((mu b. Int)) & ((mu b. (b -> Int))))) & ((mu b. (a -> Int)))))],[(mu a. (mu b. Int)),(mu a. (mu b. (((b -> Int)) & ((a -> Int)))))],[(mu a. (((mu b. Int)) & ((mu b. (((b -> Int)) & ((a -> Int)))))))],[(mu a. (((mu b. ((Int) & ((b -> Int))))) & ((mu b. (a -> Int)))))],[(mu a. (((mu b. ((Int) & ((a -> Int))))) & ((mu b. (b -> Int)))))]]
 
ghci> filter (\xs ->  tsubdp2 (foldl1 SAnd xs) ttc) (psplit (-3) (-1) ttc)
[[(mu a. (mu b. Int)),(mu a. (mu b. (b -> Int))),(mu a. (mu b. (a -> Int)))],[(mu a. (((mu b. Int)) & ((mu b. (b -> Int))))),(mu a. (mu b. (a -> Int)))],[(mu a. (((mu b. Int)) & ((mu b. (a -> Int))))),(mu a. (mu b. (b -> Int)))],[(mu a. (mu b. ((Int) & ((b -> Int))))),(mu a. (mu b. (a -> Int)))],[(mu a. (mu b. ((Int) & ((a -> Int))))),(mu a. (mu b. (b -> Int)))],[(mu a. (mu b. ((((Int) & ((b -> Int)))) & ((a -> Int)))))]]

The proposed strategy

  • For a recursive type mu a. A
  • We do a splitting on A (treating a as universal variable, regardless of the pos/neg of a):
  • The splitting process is described in psplit function,
    • the key in this function is that in the recursive type case (where the recursive type is positive w.r.t. itself!), we allow splitting that are
      • nested, (i.e. mu b. (a -> Int ) & (a -> Bool) can be split into two)
      • mergeable (i.e. enumerating all combinations, not only the component but also mu b. (a -> Int ) & (a -> Bool) are valid combinations )
    • For other type constructors, we simply propagate the constructor and no need to enumerate as they create equivalent types
  • Now for each splitting of A, we close them with a recursive binder a, and require that this spitting to be checked against LHS

Proving

To prove the soundness of the translate rule, we should still start from the right type

For A << [Bi [a- |-> {a : B}]], where Bi is split from B and ordinary
...

But maybe with the insight from Siek, Bi does not have to be fully split (w.r.t. translated type notion), but we consider atomic components from the perspective of pcont

For each A << [Bi [a- |-> {a : B}]]
where Bi' ~~> Bi, B' ~~> B, and Bi' is in pcont(B')

1) If a is not in negative free variables of Bi,
 then:
 
	    A << [Bi [a- |-> {a : B}]]
implies A << [Bi [a- |-> {a : Bi}]]
implies exists C part of A, <---------- does this hold?
        mcod(C) [a- |-> {a : mcod(C)}] << [Bi [a- |-> {a : Bi}]]

and mcod(C) and Bi are invertible (thanks to pcont)



2) If a is in negative free variables of Bi

??? TODO

As I note, as part of the reasoning, in order to show implies exists C part of A, Bi is still in a certain notion of “ordinary”

can we exploit it in the proof?

Examples of “A < psplit”

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

the body psplits to:
  Int -> mu b. (Int -> b)
  Int -> mu b. (Bool -> b)

let A := (mu a. Int -> mu b. (Int -> b)) & (mu a. Int -> mu b. (Bool -> b))

we can find atomic:
  Int -> mu b. (Int -> b) <: Int -> mu b. (Int -> b)
  Int -> mu b. (Bool -> b) <: Int -> mu b. (Bool -> b)

--------------

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

the body psplits to
  Int -> mu b. ((b -> Int) & (b -> Bool))

let A := (mu a. Int -> mu b. (b -> Int)) & (mu a. Int -> mu b. (b -> Bool))
====> the found subtype (which is A) is not ordinary, but it still holds that
       mcod(A) [a- |-> {a : mcod(A)}] << [Bi [a- |-> {a : Bi}]]]

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

the body psplits to
  a -> mu b. ((b -> Int) & (b -> Bool))


let A := (mu a. a -> mu b. (b -> Int)) & (mu a. a -> mu b. (b -> Bool))
====> the subtyping does not hold, 
      due to negative subtyping + strict distributivity



let A := (mu a. Top -> mu b. (b -> Int)) & (mu a. Top -> mu b. (b -> Bool))
====> the found subtype (which is A) is not ordinary, but it still holds that
       mcod(A) [a- |-> {a : mcod(A)}] << [Bi [a- |-> {a : Bi}]]]

For each Bi, we can find an invertible Ai For each (activated) Ai, we can find a group of Bs

Graph View

Backlinks