Compute the Intermediate Type

Based on weakly positive restriction for translated types we can define a relation that captures the way we compute intermediate types in Full Splitting

|-------------|
| A << B |> C |
|-------------|

a ∈+ A << T
A << T |> Bm
------------------------------------- rec-wkpos
   zeta a l. A [ a - |->  { l a : A } ] 
<< zeta a l. T [ a - |->  { l a : B } ] 
|> zeta a l. Bm [a - |->  { l a : Bm }]



B <: A
-------------------------------------
zeta a l. A [ a - |->  { l a : A } ] 
<< zeta a l. T [ a - |->  { l a : B } ] 
|> zeta a l. A [a - |->  { l a : A } ]



A2 << B2 |> Bm2
----------------------------------
A1 -> A2 << B1 -> B2 |> B1 -> Bm2


A1 << B |> C
------------------
A1 & A2 << B |> C


A2 << B |> C
------------------
A1 & A2 << B |> C



+ 1 special rule when B is toplike

Then we are left to prove

Theorem. If A' ~~> A, A << B |> C, then there exists C' s.t. C' ~~> C (Easy)

Theorem. If A' ~~> A, B' ~~> B, Bi in spl(B), A << Bi |> C, then A << C << Bi

• Proof in case rec-wkpos might be hard,
  • we get A << Bm << T from IH
  • but we need to show A [a- |-> {a : A}] << Bm [a- |-> {a: Bm}] << T [a- |-> {a : B}]
  • given only a ∈+ A << T, but we expect a ∈+ A << Bm
• Therefore we need to prove another lemma:

Lemma. If A' ~~> A, B' ~~> B, Bi in spl(B), A << Bi |> C, then for any a, a ∈+ A << Bi implies a ∈+ A << C

since we cannot specify a concrete a, we have to state as an implication

• Proof in case rec-wkpos:
  • a ∈+ A << T
  • IH tells for any a a ∈+ A << T implies a ∈+ A << Bm
  • Goal is to show for any b, if b ∈+ A [a- |-> {a : A}] << T [a- |-> {a: B}] then b ∈+ A [a- |-> {a : A}] << Bm [a- |-> {a : Bm}]

need to rely on substitution lemmas for weak pos

• Proof in case rec-self: ok

Now prove the theorem again

• Proof in case rec-wkpos:
  • we get A << Bm << T from IH
  • a ∈+ A << T, and applying the lemma, we get a ∈+ A << Bm
  • By a ∈+ A << T, we derive
  • A [a- |-> {a : A}] << Bm [a- |-> {a: Bm}] << T [a- |-> {a : B}]
    • LHS by a ∈+ A << Bm
    • RHS by Bm << T and B << Bm (? How)
• Proof in case rec-self?

Counterexamples:

In fact, there are counterexamples to the current rules (See Haskell pwlt7a):

Despite

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

It is not true that:
	mu a. Top -> (mu b. b -> Int & b -> Bool) (----- WKPOS) 
&   mu a. a -> (mu b. b -> String)            (----- REFL)
<: [x]
	mu a. a -> (mu b. b -> Int & b -> Bool & b -> String)

we must merge then subtyping

But we can still have
	mu a. Top -> (mu b. b -> Int & b -> Bool)
&   mu a. Top -> (mu b. Top -> b)
<: 
	mu a. Top -> (mu b. b -> Int & b -> Bool)
&   mu a. Top -> (mu b. Int -> b)
<:
	mu a. a -> (mu b. b -> Int & b -> Bool & Int -> b)

It seems that something even stronger should be derived from negative reflexivie subtyping

Think again:

We have merge then subtyping:

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

It is not true that:
   ...
<:
	mu a. Top -> (mu b. b -> Int & b -> Bool) (----- WKPOS) 
&   mu a. a -> (mu b. b -> String)            (----- REFL)
<: [x]
	mu a. a -> (mu b. b -> Int & b -> Bool & b -> String)

we must merge then subtyping

We have subtyping then merge

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

but not
  mu a. (Top -> a)
& mu a. (a -> Int & a -> Bool)
<: merge
& mu a. (Top -> a & a -> Int & a -> Bool)
<: subtyping -- no
  mu a. (Int -> a & a -> Int & a -> Bool)

merges in the inner mu will pose an equality constraint on the outer recursive variables

Check, how the derivation differ in:
    mu a. Top -> (mu b. b -> Int & b -> Bool)
&   mu a. Top -> (mu b. b -> String & b -> Int)
is subtype of 
    mu a. a -> ((mu b. ...)  &( mu b .  ...))

between 
    mu a. Top -> (mu b. b -> Int & b -> Bool)
&   mu a. Top -> (mu b. b -> String)
is subtype of 
    mu a. a -> ((mu b. ... &  ...))