Tony's Wiki

Aug 14 - Meeting

11 min read

  • Although rule csub-mu is not “modular”, we can still have a “modular” version of subtyping, where only the csub-mu rules require ordinary restrictions

    • so we get an easier set of rules to work with! (e.g. substitution lemma)

  • Issue with revisiting msub2_subst lemma:

Due to the andl-andr non-det choice, we can no longer induction on

[msub A B] and then inversion on [msub (subst_styp_m m X C A) (subst_styp_m m X D B)].

Also, due to the new trick, [C] and [D] have to be a labeled type


The condition that [C] and [D] are labeled is also necessary for
dealing with the substitutions under [spl]

and therefore, we might not be able to prove the structural lemma
that easy??

  • We get substitution lemmas in their normal form!!!

    • with some proof tricks on reasoning with positive/negative substitutions
    1. see if the polarizied substituion can go through as the same as the full substitution version

  • TODO: prove the dist-mu rule and see if it helps

  • also recheck the nominal unfolding rule

  • the structural lemma will be

  • logical relation for a semantics

Problem:

  • not complete: the ordinary constraint cause reflexivity problem:
   mu a. (a -> Int) & (a -> Bool)
<: mu a. (a -> Int) & (a -> Bool)

is not in the subtyping relation, because the RHS has to be split first
and 
mu a. (a -> Int) & (a -> Bool) <: mu a. a -> Int 
does not hold

Solution:

  • make the nested negative types non-regular

    • making the subtyping relation less expressive than the one without BCD

  • add built-in reflexivity rule

    • For the completeness proof: solve the refl problem in completeness proof directly
      • However, another (perhaps the only left) issue:
        • to add a proper restriction on the declarative rule
          • mu a. A & mu a. B <: mu a. A & B
          • as well as the nominal unfolding rule (maybe not? if we can case analysis on pos/negativeness and apply the built-in refl rule)
            • and if we manage to avoid introducing extra constraints on the nominal unfolding rule, then we are able to preserve the conservativity to the original nominal unfolding rule
        • to ensure that the RHS is ordinary
    • For the previous proofs, we face the transitivity issue again:
   mu a. (a -> Int) & (a -> Bool) & (Bool -> a)
<: mu a. ((a -> Int) & (a -> Bool)) & (Bool -> a)

However, we cannot show?
   mu a. (a -> Int) & (a -> Bool) & (Bool -> a)
<: mu a. ((a -> Int) & (a -> Bool))

TODO: check here what's the counterexample
  • modify the algorithmic csub-mu to allow non-ordinary rules?
    • see bcd-controled branch
    • Observation: requiring B to be c-ordinary in [a. B] is actually stronger than requring [a. B] to be ordinary: B c-odrinary => [a. B] c-odrinary but not the reverse
    • Proofs of lemmas like csub_inv_spl_l_simple will fail, no such condition is provided
now we allow 
   mu b. b -> mu a. (a -> Int) & (a -> Bool)
<: mu b. b -> mu a. (a -> Int) & (a -> Bool)
because we no longer consider c-splittable RHS as invalid

but LHS is c-splittable, and we expect lemmas like:   
Lemma csub_inv_spl_l_simple : forall n A A1 A2 B,
size_ctyp A + size_ctyp B < n ->
csub A B -> cspl A1 A A2 -> cord B -> csub A1 B \/ csub A2 B.

which is not the case for: mu a. (a -> Int) <: mu a. (a -> Int) & (a -> Bool)


See a further example in the code `bcd-controled` branch

Consider case where mu b. A0 <: mu b. B0
where B0 is sord but not cord?

Now we admit: 
A0 = mu a. (Top -> Int) & (Top -> Bool)
B0 = mu a. (a -> Int) & (b -> Bool)

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

Here,
LHS splits into: mu b. mu a. Top -> Int
               & mu b. mu a. Top -> Bool

RHS is c/s-ordinary, body of RHS is s-ordinary, c-splittable

We cannot show:
mu b. mu a. Top -> Int <: mu b. mu a. (a -> Int) & (b -> Bool)
or
mu b. mu a. Top -> Bool <: mu b. mu a. (a -> Int) & (b -> Bool)


so transitivity will fail, assume
A0' = mu b. mu a. Top -> Int
& mu b. mu a. Top -> Bool


Then:

A0' <: A0, because A0 is c-splittable
A0 <: B0 by the relaxed csub-mu rule
but A0' <:[x] B0, because B0 is not c-splittable

Result of the current system: mu Types that are not c-splittable, and has a s-ordinary, but c-splittable body, will never be considered as a supertype:

e.g.
mu a. a -> (mu b. (b -> Int) & (b -> Bool))

mu Types that are c-splittable, but are s-ordinary (implying negative in the body), will never satisfy the reflexive property:

e.g.
mu b. (b -> Int) & (b -> Bool)
mu b. (Int) & (b -> Bool)

Other

  • leave of absence

Pre-discussion on Discord

Hi @everyone, I am posting some of my latest progress here as I run into some problems with the Controlled Subtyping idea and some design choices need to be made. Please share your thoughts in case you have some ideas so I can try before the meeting this week.


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

Current status of controlled subtyping

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

mu a. a -> (mu b. (b -> Int) & (b -> Bool)) is not splittable

a -> (mu b. (b -> Int) & (b -> Bool)) is splittable, not ordinary


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


B1 <| B |> B2
ordinary [ (a, l). B ]
a is in fv_neg(B)
A <: B1
A <: B2
B <: A
---------------------------
[ (a, l). A ] <: [ (a, l). B ]

Based on the rules I presented in the last document, we can derive a “modular” subtyping variant, where the ordinary constraints in the function, toplike, andl, andr rules are removed. However, note that in this “modular” rules, the ordinary constraint in the csub-mu rule cannot be removed. Otherwise the controled “algorithmic” subtyping will not be equivalent to the “modular” subtyping.

Despite this and some issues I suspected last time, many of them can actually be solved. In particular I proved:

  • transitivity (which was done last time, and note that it relies on the extra ordinary condition in the csub-mu rule)
  • the restricted splitting/ordinary relation can still have the standard form of the unfolding lemma (without adding any extra conditions)
  • the unfolding lemma should be admissible for the controlled subtyping relation (maybe not the structural unfolding lemma, as labeled types seem to matter)

Issue of controlled subtyping

However, there is one important problem in the controled subtyping: reflexivity is lost. Think of the proof of reflexivity: in case of [a. A] (the recursive label type), the IH gives A <: A, to show [a. A] <: [a. A] by applying csub-mu rule, we need to know [a. A] is ordinary, which is not always true, and as we mentioned, there is no modular version of csub-mu that does not require an ordinary constraint.

If we look at examples we can actually see that (in order to achieve transitivity?) this ordinary constraint in the csub-mu rule forbids quite a lot of subtyping:

  • mu Types that are c-splittable, but are s-ordinary (implying negative occurrence of the recursive variable in the body), will never satisfy the reflexive property:
e.g.
mu b. (b -> Int) & (b -> Bool)
mu b. (Int -> b) & (b -> Bool)
are not reflexive to themselves
  • recursive types that are not c-splittable, and has a s-ordinary, but c-splittable body, will never be considered as a supertype of any type:
e.g.
mu a. a -> (mu b. (b -> Int) & (b -> Bool))
because neither csub-and nor csub-mu can be applied
(Note that the c-ordinary constraint is posed on the body B, instead of the whole type [a. B])

However, reflexivity is an expected property and it is also important to prove completeness (since the source subtyping is reflexive). So I am thinking of some recovery strategies:

Removing the ordinary constraint from csub-mu (Coq branch: bcd-controled)

Since we know that with ordinary constraint, the algorithmic csub-mu does not have a modular version. We consider removing the ordinary constraint from algorithmic csub-mu rule in the first place. Then csub-mu will overlap with csub-and in the case of recursive types, but we recover reflexivity.

However, this will fail the transitivity property:

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


(translated) A is a subtype of (translated) B
because B can be split into
      mu b. mu a. (Top -> Int)
and   mu b. mu a. (Top -> Bool)

(translated) B is a subtype of (translated) C
because C is c-ordinary (due to nested negative occurrence of `a` and `b`)
so csub-mu rule can be applied

However, A is not a subtype of C
as C is splittable, it is not ordinary
so csub-and rule cannot be applied to C

Adding a built-in reflexivity rule (Coq branch: bcd-controled)

I am not sure if this idea can work, but currently it creates some complexities in this lemma (which is essential for the transitivity lemma):

Lemma csub_inv_spl_r_simple : forall n A B1 B2 B,
  size_ctyp A + size_ctyp B < n ->
  csub A B -> cspl B1 B B2 -> csub A B1 /\ csub A B2.

In the new case, A = B, we need to show csub B1 B /\ csub B2 B from cspl B1 B B2 with no induction hypothesis to use. However, this does not always hold, consider:

B = [b. (b -> [a. ((a -> Int) & (a -> Bool))]) & 
        (Top -> [a. (a -> String)])]
         with [a- |-> {a : .... } ], [b- |-> {b : ... }]
B1 = [b. b -> [a. (a -> Int) & (a -> Bool)]]
         with [a- |-> {a : .... } ], [b- |-> {b : ... }]
B2 = [b. Top -> [a. (a -> String)]]
         with [a- |-> {a : .... } ], [b- |-> {b : ... }]

I will omit the polarized substitution as they are not the cause of problem

B is not a subtype of B1, because
B1's body can be further split into:
b -> [a. a -> Int] and b -> [a. a -> Bool] (with substution)
so `csub-mu` rule cannot be applied

B itself is not c-splittable (due to nested negative occurrence of `a` and `b`), so `csub-and` cannot be applied

I am still hoping that there can be some minor adjustments to the current controlled subtyping rules (as they prove to have other nice properties) to recover the reflexivity property, but I am not sure how to do it yet. Or perhaps we need some deeper changes to the controlled subtyping rules to achieve what we want, i.e. avoiding the counterexample we had before, but also preserving reflexivity, transitivity, etc. Please let me know if you have any ideas or suggestions, I will try to implement them before the meeting this week.

Thoughts Afterwards

There might more foundational reason of this issue, our intention was to avoid nested negative types like:

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

they were valid in an unrestricted translated subtyping, but not derivable in the source declarative subtyping

So we come up with the restriction that nested deep negative types are not allowed.

This can indeed become a source of non-transitivity (the subtyping only allows one-splits but not deep splits)

Currently, we achieve transitivity by having an over-restricted subtyping system that is even not reflexive

If we are going to loosen this restriction, we have to reconcile between the restriction with the potential non-transitivity issue. (the hope is that by the property that negative types can at most be reflexive, we can achieve this reconciliation)

Graph View

Backlinks