- The inductive relation we discussed last week does not work as expected
- May 10 update the rule does not work precisely
- We revisit the notion of Controled Splitting in More precise controled splitting, and find we should further s-split nested positive types
- todo The observation leads to what proof?
Also, another issue is that we might NOT be able to prove an equivalence congruence lemma on recursive type, so whether the proof idea really works remain a question
i.e. : A <: B and B <: A implies mu a. A <: mu a. B Solved- We find an example that fails the Siek’s intermediate subtyping
- Solution: check Laurent Olivier’s BCD rules, see if similar style can be developed for distributivity + Amber style?
- The structural unfolding lemma seems provable, with translated subtyping
- TODO revisit the JFP issue, see if it also solves the restriction on the structural unfolding lemma
⇒ what is the translation in presence of bounded quantification
- If we adapt the APLAS typing (+structural) and semantics, do we get a calculus for free?
- ⇒ No, we still need to deal with disjoint, casting, (which relies on splitting, and cause uninvertible types)
- The structural unfolding lemma also helps with the encoding, already shared in the notes