Tony's Wiki

Sept 18 - Meeting

7 min read

New notion of ordinary

The problem last time:

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


BUT:

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

Solution: split cord into tord and tsplty

tord - subtyping ordinary tsplty - subtyping splitable but c-ordinary

The corner case we are facing is

  A1 -> ... -> [a. ... ]
& ...
& An -> ... -> [a. ... ]
<:
  B1 -> ... -> [a. ... ]

tsplty B2
A' is function part of A
B1 <: dom(A')
cod(A') <: B2
-----------------------
A <: B1 -> B2

(** [tsplty] are designed to be the types that are 
    c-ordinary, but not-ordinary,
    i.e. contain non-ordinary parts in their bodies *)
Inductive tsplty : ctyp -> Prop :=
| tsplty_arrow : forall A B,
    lcv_styp A -> lcl_styp A ->
    tsplty B ->
    tsplty (styp_arrow A B)
| tsplty_mu_neg : forall A L,
    (forall X, X `notin` L -> X `in` fv_ctt_m Pos (open_ctt (open_ctl A X) X)) ->
    (forall X, X `notin` L -> sord (open_ctt (open_ctl A X) X)) ->
    tsplty (styp_mu A)
| tsplty_mu_pos : forall A L,
    (forall X, X `notin` L -> X `notin` fv_ctt_m Pos (open_ctt (open_ctl A X) X)) ->
    (forall X, X `notin` L -> tsplty (open_ctt (open_ctl A X) X)) ->
    tsplty (styp_mu A)
.

The formalization for the extended subtyping rules is:

| csub_arr_splty: forall As A B1 B2,
    lcv_styp A -> lcl_styp A ->
    tsplty B2 ->
    tpart_fun As A ->
    csub B1 (fdoms As) ->
    csub (fcods As) B2 ->
    csub A (styp_arrow B1 B2)
 
| csub_mu_pos: forall A A' B L,
    lcv_styp A -> lcl_styp A ->
    cont_pos A (Some A') ->
    (forall X, X `notin` L -> 
      csub (open_ctt (open_ctl A' X) X) (open_ctt (open_ctl B X) X)) ->
    tsplty (styp_mu B) ->
    csub A (styp_mu B)
 
| csub_mu_neg: forall A A' B L, 
    lcv_styp A -> lcl_styp A ->
    cont_neg A A' ->
    (forall X, X `notin` L -> 
      csub (open_ctt (open_ctl A' X) X) (open_ctt (open_ctl B X) X)) ->
    tsplty (styp_mu B) ->
    csub A (styp_mu B)

which we make use of the legacy in Containment.v

As is (sublist) part of A
B1 <: doms As
cods As <: B2
B2 is special-splittable
-------------------------
A <: B1 -> B2



A' is the merge of all positive mu-parts of A
A' <: B
B2 is special-splittable
-------------------
A <: [a. B]


A = mu a. (A1a+ & A1b-)  & mu a. A2+ & ....

mu a. (A1a+ & A1b-) <: mu a. A1a+ 


A' is one of the negative mu-parts of A
A' <: B
B2 is special-splittable
-------------------
A <: [a. B]

Important Lemmas proved

  • tord tsplty are mutual exclusive
  • tord \/ tsplty cord
  • tord types can have left inversion lemmas for csplitting:
    • A <: B, tord B, A1 <| A |> A2
    • then either A1 <: B or A2 <: B
  • Promotion lemmas:
Lemma csub_cont_neg: forall A A' B,
	csub (styp_mu A') B ->
	cont_neg A A' ->
	csub A B.

Lemma csub_cont_neg_r: forall A A' B,
  csub B A ->
  cont_neg A A' ->
  csub B (styp_mu A').

Also works for cont_pos, tpart_fun

The cont_neg and cont_pos design match well with the cspl/sspl

Proof strategy of Transitivity

A <: B <: C by size

  1. C is c-splittable, we have A <: C1 and A <: C2 by IH, and A <: C follows
  2. C is c-ordinary, B is c-ordinary,
    • by analysis on A <: B and B <: C we can always apply IH to a smaller type (e.g. A1 in A1 -> A2, A in [a. A] )
    • To finish the proof in these cases, we need more modular lemmas, in particular the extended ones (should be fine)
  3. C is t-ordinary, B is c-splittable, then either A <: B1 or A <: B2, so A <: C by IH
  4. (the only left case:) C is tsplty, B is c-splittable:
    • The arrow types: OK, we have good inversion lemmas
    • The recursive types: no

Example of the only left case:

A = (mu b. Top -> (mu a. a -> Int))
  & (mu b. Top -> (mu a. a -> Bool))
  
B = mu b. Top -> ((mu a. a -> Int) & (mu a. a -> Bool))
  (c-splittable)
C = mu b. b -> (mu a. (a -> Int) & (a -> Bool))    
  (c-ordinary, body splittable)

A <: C is concluded by the corner case positive rule

The proof idea:

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

where [a. C] is tsplty
      [a. B1] <| [a. B] |> [a. B2]
      
We should argue that A must be mu-like

so we can find a merge As of A's mu-bodies: 
such that:
   As <: B <: C ==IH==> A <: C
so [a. As] <: [a. C]
and A <: [a. As] <: [a. C]


As is the merge of A's mu-bodies
A <: [a. As]
[a. As] <: [a. C]
-----------------
A <: [a. C]









A = Int & [a. A1] & [a. A2]
As = A1 & A2
------------------
[a. As] <==> A












The problembatic case is the last step!

as the As might have both pos/neg parts
so even though A <: [a. As], it is possible that A <:[x] [a. C]

However, it seems that we cannot prove this reasoning without priori knowledge of the shape of translated type:

          mu b. b -> (mu a. a -> Int) & (mu a. a -> Bool)
    <:[x] mu b. b -> (mu a. (a -> Int) & (a -> Bool))
    Does not hold



    mu b. b -> (mu a. (a -> Int) & (a -> Bool))
~~> [b.  {b : ... } -> [a. { a: ... } -> Int
                         & { a: ... } -> Bool ] ]

       [b. (Top -> [a. Top -> Int])] & [b. b -> [a. a -> Bool]]
    <:[might ok] [b. (b -> [a. a -> Int]) & (b -> [a. a -> Bool])]       --- cspl
    <:[might ok] [b. b -> [a. (a -> Int) & (a -> Bool)]]                    --- cord, tsplty
    Might hold with a proper substitution on b


    But, [b. (Top -> [a. Top -> Int])] & [b. b -> [a. a -> Bool]]
      <:[must no] [b. b -> [a. (a -> Int) & (a -> Bool)]] 
      
      
      wf T
      B is part of T
      ------------------
      wf [a . B [a- |-> {a : T }]]

TODO:

  • more modular lemmas, in particular the extended ones
  • inversion lemmas, for A <: B1 -> B2, we say exists As part of A …
    • for A <: [a. B]? there are two disjunctive cases?
    • what about the case where a is neg/pos in B?

After Meeting Notes

  • QuickSub - can thread over the union types, to reduce complexity
  • can visit Tom while in Paris
  • try source subtyping afterwards
  • Fiplus casting - might be better suit to solve other problems
    • see Lionel OOP example

Graph View