Sept 4 - Meeting

• Implementation

  • Implemented in typ.how Haskell Unbounded.LocallyNameless
  • Test the implementation (e.g. transitivity) using QuickCheck

• The proposal last week

  • !!! pconts need to be refined, to fully split the positive counterparts
  • toplike_csub with the part relation
  • Are more conditions needed for the formalization?
    • csub_inv_spl_r_simple is unchanged because we add the ordinary condition

• A new proposal

  • We achieve a modular subtyping rule for csub-mu
  • reflexivity should be ok
  • csub_inv_spl_r_simple still OK
  • Transitivity
    • The csub_inv_spl_l_simple is not provable
      • Can we fix it with size (maybe no)
      • the size proof trick might only be inlined in the transitivity proof
    • How to prove transitivity without the presence of csub_inv_spl_l

• Idea: can we have a meta-proof for substitutions?

The proposal we have last week

In Aug 27 - Meeting, we propose:

[a. B] is c-ordinary
B is not c-ordinary <==> B1 <| B |> B2
==> B is s-ordinary
==> a in FvNeg(B)
A' is part of the mu-domains of A
if a in FvNeg(A')
   then dropLabel(a, A') <: dropLabel(a, B) 
        and dropLabel(a, B) <: dropLabel(a, A') 
   else A' <: B
-----------------------------
A <: [a. B]

Some intuitions on this rule:

• This rule identifies the problematic corner case we had in the unrestricted target subtyping: mu a. a -> mu b. (b -> Int) & (a -> Bool), which involves nested negative types, but the body is c-splittable
• The negative a poses a reflexive constraint on the left type, so this rule attempt to require isomorphism in presence of negative variables
• Since the LHS can be intersections, this rule attempts to find those precise intersection fields that form the isomorphic counterpart
• The labelled types can mess up with the iso-morphism due to translation on mu a. A & mu a. B vs. mu a. A & B, so dropLabel is required
• Also, for the identified right type, it can be the case that the negative a is compared with Top, so when the left type is positive, we still require A' <: B instead of isomorphism

This rule is challenging to reason with:

Transitivity Proof, tricky case:

Consider A <: B <: C we need to show B <: C when we are considering mu-like types, A <: B and B <: C can have multiple (in particular, 3) cases. Those cases where A <: B and B <: C adopt different csub-mu rules can be tricky:

Csub_mu_pos + Csub_mu

s-ordinary B
a in Fl_Neg(B)
A' part of mu-body of A
A' <: B
a notin Fl_Neg(A')
-----------------
A <: [a. B]


c-ordinary C
B <: C
-----------------
[a. B] <: [a. C]

How to prove A <: [a. C]? the only rules available are csub-mu, csub-andl, csub-andr

Examples for this case:

A = mu a. Int -> mu b. (Top -> Int) & (Top -> Bool) 
  & mu a. Int -> mu b. (Top -> Int) & (Bool -> a)
B = mu a. Int -> mu b. (b -> Int) & (b -> Bool) & (a -> Int) & (Bool -> a)
C = mu a. Int -> mu b. (Bool -> a)

Csub_mu_neg + Csub_mu

s-ordinary B
a in Fl_Neg(B)
A' part of mu-body of A
A' <: B
a notin Fl_Neg(A')
-----------------
A <: [a. B]


c-ordinary C
B <: C
-----------------
[a. B] <: [a. C]

A new proposal

The rule in The proposal we have last week, though being able to rule out the counterexamples to soundness, is too restrictive. In particular, the isomorphism check is not flexible enough in the reasoning. By taking a closer look, we adopt more intuitions and propose the simplified rule: (Coq branch bcd-simple)

The usual case:

A <: B
B is c-ordinary
------------------------ Csub-mu
[a. A] < [a. B]


Again, the corner case we are considering is when the right type is [a. B], where
[a. B] is c-ordinary, but B is c-splittable, implying a is negative in B


A' ∈ negative mu-part of A
A' <: B
B is s-ordinary
a in FlNeg(B)
------------------------- Csub-mu-neg
A <: [a. B]


A' = &(positive mu-parts of A)
A' <: B
B is s-ordinary
a in FlNeg(B)
------------------------- Csub-mu-pos
A <: [a. B]

$\frac{A^{\prime }\in \text{MuPart}(A)a\in \text{FlNeg}(A^{\prime })B^{\bullet }a\in \text{FlNeg}(B)A^{\prime }<:B}{A<:[a.B]}\text{Csub-Mu-Neg}$

$\frac{A^{\prime }=\&(\{A_i\in \text{MuPart}(A)|a\notin \text{FlNeg}(A_i)\})B^{\bullet }a\in \text{FlNeg}(B)A^{\prime }<:B}{A<:[a.B]}\text{Csub-Mu-Pos}$

$\text{MuPart}([a.A])=\{A\}\text{MuPart}(A\&B)=\text{MuPart}(A)\cup \text{MuPart}(B)$

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




A <: B
--------------
[a. A] <: [a. B]




A' in MuPart(A)
[a. A'] <: B
----------------
A <: B








A1 <| A |> A2
A <: B
ordinary B
---------------
either A1 <: B or A2 <: B




A <: B <: C
C ordinary
B splittable


[a. B1] <| [a. B] |> [a. B2]

Int -> [... A ] <: (Int -> [a. B1]) & (Top -> [a. B2]) <: Int -> [a. C]




  
  

  Int -> [a. Top -> [b. (b -> Int)]]
& Top -> [a. Top -> [b. (b -> Bool)]]

<: Int -> [a. Top -> [b. (b -> Int)]
            & Top -> [b. (b -> Bool)]] -- splittable

<: 

  Int -> [a. a -> [b. (b -> Int) & (b -> Bool)]] -- ordinary