When dealing with A ~~> A' << B, where B1 <| B |> B2 is splittable, and the split result is not invertible, we need a way to find the middle type.
We would like to define an inductive relation to find the middle type. A << B |> C, indicating that C is the middle type for A << B, where A is invertible, and B should be an (ordinary) split result from an invertible type.
Expected Properties:
1. the middle type exists:
for any
A' ~~> A, wfm B, ord B,
exists A << B |> C
wfm A
A split from B
----------------
wfm [a. A [a- |-> {a : B}]]
2. the middle type forms a subtyping relation:
if A << B |> C, then
A << C << B
3. the middle type is invertible
if A << B |> C, then
exists C' ~~> C
4. fragments should lead to a equivalence body:
If B splits into B1, ... , Bn,
and A << [B1 [a- |-> {a : B}] ] |> [ C1 [a- |-> {a : C1 }] ]
mu a. C1' ~~> [ C1 [a- |-> {a : C1 }] ]
A << [B2 [a- |-> {a : B}] ] |> [ C2 [a- |-> {a : C2 }] ]
...
A << [Bn [a- |-> {a : B}] ] |> [ Cn [a- |-> {a : Cn }] ]
then
C1 & C2 & ... & Cn is equivalent to B
B << C1 << B1
(so, in the soundness proof, we can argue that the
(mu a. C1') & (mu a. C2') ... & (mu a. Cn')
are valid middle types for A << mu a. C' << mu a. B
)
Alternatively, for this property we can prove that:
B << C1 << B1
...
B << Cn << Bn
as a lemma (or inherient constructor) for each individual case
5. The size should be decreasing in order to prove the soundness theorem:
If Xs |- A << B |> C, then
either A <: C and size C <= size A
or C <: B and size C <= size B
Failed attempt:
nat << nat |> nat
A1 << B |> C
-------------
A1 & A2 << B |> C
A2 << B2 |> C2
--------------
A1 -> A2 << B1 -> B2 |> B1 -> C2
Lemma: if [A [a- |-> {a : A}]] << [T [a- |-> {a : B}]]
then either a is weakly postive A << T
or. {a : B} << {a : A} (B << A << T)
A << T |> C
a weakpos A << T
-------------- pos
[A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] |> [ C [a- |-> {a : C}] ]
A << T |> C
B << A
------------- neg
[A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] |> [ A [a- |-> {a : A}] ]
We have missing cases when trying to prove exists T, such that A << B |> T
when
a weakpos in A << T (----> we don't get the condition of B << A)
but
a not weakpos in A << C
A << C << T
How to show B << A ?? <-- is it always true?
Example: neg leads to neg
e.g.
A << T |> C implies A << C /\ C << T
Lemma: if [A [a- |-> {a : A}]] << [T [a- |-> {a : B}]]
then either a is weakly postive A << T
or. {a : B} << {a : A} (B << A << T)
A << T |> C ==> A << C << T
wfm [T [a- |-> {a : B}]] ===> B << T, T is a fragment of B
a weakpos A << T
-- a weakpos A << C and a weakpos C << T
-------------- pos
[A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] |> [ C [a- |-> {a : C}] ]
B << C << T
B << A
------------- neg
[A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] |> [ A [a- |-> {a : A}] ]
If a is negatively compared in A << T, and T is part of B
then a is negatively compared in A << B
A1 = mu a. Int -> mu b. ((b -> Int) & (a -> Int))
A2 = mu a. a -> Int
<: mu a. (
(Int -> mu b. ((b -> Int) & (a -> Int)))
& (a -> Int)
)
mu a. ((Int -> mu b. ((b -> Int) & (a -> Int))) & (a -> Int))
For the first fragment, we have a is weakly positive in A << T
and that "mu a. ((Int -> mu b. (b -> Int))" is a valid subtype of the first fragment T
but it is not a valid supertype of
A1 = "mu a. Int -> mu b. ((b -> Int) & (a -> Int))"
so we still need to find
"mu a. Int -> mu b. ((b -> Int) & (a -> Int))"
as the middle type for the first fragment in T
where a is weakly positive in the translation of A << T,
but the introduction of a -> Int component in A << T |> C
brings out the negative case
i.e. we should still have the rule
For the first fragment in:
(Int -> [b.
({b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
])
& (a -> Int)
[a- |-> {a : (Int -> [b.
({b : (b -> Int) & (a -> Int) & (Int -> a)} -> Int)
& (a -> Int)
])
& (a -> Int)
& (Int -> a)
} ]
i.e.
The first fragment:
A1 = mu a. Int -> mu b. ((b -> Int) & (a -> Int))
| A1 |
<< [a. (Int -> [b. ({b : (b -> Int) & (a -> Int) } -> Int)])]
|> mu a. Int -> (mu b. (b -> Int)) <-- This is fine ?!!
namely:
[a. (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
])
]
[a. (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& ({ a : (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& ( a -> Int)
])
& (a -> Int)
} -> Int)
])
& ({ a : (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& ( a -> Int)
])
& (a -> Int)
} -> Int)
]
We assert
| mu a. Int -> mu b. ((b -> Int) & (a -> Int)) |
= [a. (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& ({ a : (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
])
} -> Int)
])
<< [a. (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
])
]
|> [a. (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& ({ a : (Int -> [b.
({ b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
])
} -> Int)
])
The above assertion comes from the following subderivation:
| mu b. ((b -> Int) & (a -> Int)) |
= [b.
({b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
]
<< [b. ({ b : (b -> Int) & (a -> Int) } -> Int) ]
|> [b.
({b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
]
which comes from
(b -> Int) & (a -> Int)
= ({b : (b -> Int) & (a -> Int) } -> Int)
& (a -> Int)
<< ({ b : (b -> Int) & (a -> Int) } -> Int)
|> ({b : (b -> Int) & (a -> Int) } -> Int)
Example: neg + pos
mu a. Int -> mu b. ((b -> Int) & (Int -> a))
mu a. a -> Int
<: mu a. (
(Int -> mu b. ((b -> Int) & (Int -> a)))
& (a -> Int)
)
(b -> Int) & (Int -> a) << (b -> Int) |> b -> Int (NEG!)
mu b. ((b -> Int) & (Int -> a))
<< [b.
({b : (b -> Int) & (Int -> a) } -> Int)
]
|> mu b. ((b -> Int) & (Int -> a))
a is not weakly positive,
Idea: don’t lose information of the substitution
G ::= . | G, { a : A }
+-------------------+
| G |- A << T |> C |
+-------------------+
a weakpos G |- A << T
G, {a : A} |- A << T |> C
-------------- pos
G |- [A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] |> [ C [a- |-> {a : C}] ]