Tony's Wiki

Inductively find the middle type (cont.)

16 min read

as we did in Example neg leads to neg, we actually find although keeping the middle type isomorphic to the right in the positive case leads to a valid subtype of the right, but sometimes it might not be the super type of the left. Example:

	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

Therefore, we should still go for the rule:

A << T |> C
a weakpos A << C <---   note here it is not 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}] ]

This rule poses a challenge in proving the existential property of A << T |> C, in particular, when we case analysis on [A [a- |-> {a : A}]] << [T [a- |-> {a : B}]] premise, we only get

  1. {a : B} << {a : A}, where neg rule applies
  2. a weakpos in A << T, but we need a weakpos in A << C in order to apply pos rule.
    • and it can be the case that a weakpos in A << C does not hold
      • i.e. A << T implies A << C is not true!

How to prove existential in case of a weakpos A << C

What can we derive from

  • A [a- |-> {a : A}] << T [a- |-> {a : B}]
  • A << T |> C
    • A << C << T
  • T is part of B (so is C ?, maybe no because part of C will come from A)
    • B << T
  • a weakpos in A << T
  • a not weakpos in A << C

We hope to derive B << A

Still, we hope to invert from A [a- |-> {a : A}] << C [a- |-> {a : B}], so the inversion of this judgement precisely fall into the pos and neg case Question: can we obtain this subtyping relation??

Based on the conditions above, we can derive

  • A [a- |-> {a: _ }] << T [a- |-> {a: _}]
  • A [a- |-> {a : B}] << C [a- |-> {a:B }] << T [a- |-> {a:B }]
  • We are done??!!

Check the previous example:

The derivation: 

Inside b binder:
	
 ----------------------------------------- neg
    [(b,l1). ({l1:c.(c -> Int) & (a -> Int)} -> Int) & (**a** -> Int)])
 << [(b,l1). ({l1:c.(((c -> Int)) & ((a -> Int)))} -> Int)])
 |> [(b,l1). ({l1:c.(c -> Int) & (a -> Int)} -> Int) & (**a** -> Int)])

Inside a binder:
	(Int -> [(b,l1). ({l1:c.(c -> Int) & (a -> Int)} -> Int) & (**a** -> Int)])
  << (Int -> [(b,l1). ({l1:c.(((c -> Int)) & ((a -> Int)))} -> Int)])
  |> (Int -> [(b,l1). ({l1:c.(c -> Int) & (a -> Int)} -> Int) & (**a** -> Int)])

May 10 update: the rule does not work precisely

The example

We revisit an example in A Mixed Example, and get into the following counterexample:

	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Top -> b)
<: subtype
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Int -> b)
-- even if a <: Top is weakly positive, we cannot replace using
--  mu a. a -> (mu b. Int -> b)
-- also, we can not delay the subtyping 
-- since after the second merge b will be negatively compared
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Int -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b & Int -> b))
<:
	mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b)


though we may
	mu a. Top -> (mu b. b -> Int & Bool -> b)
&   mu a. Top -> (mu b. Top -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Top -> b)
<: subtype	
	mu a. Top -> ((mu b. b -> Int & Bool -> b) & (mu b. Int -> b)
<: merge
	mu a. Top -> ((mu b. b -> Int & Bool -> b & Int -> b))
<:
	mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b)

xx1 = inputTyp "(mu a. Top -> (mu b. (b -> Int) & ((Int -> Int) -> b))) & ( mu a. Top -> (mu b. Top -> b))"
xx2 = inputTyp "mu a. a -> (mu b. (b -> Int) & ((Int -> Int) -> b) & (Int -> b))"
ghci > scheck xx1 xx2
(True,True)

Running the rule on the example

So, the middle type should be:

1) mu a. a -> (mu b. b -> Int & Bool -> b & Int -> b) --- a is pos, b is neg
   !!! Problem: this middle type is no longer supertype of mu a. A1 !!!
     it has to be the supertype of mu a. A1 & mu a. A2 <: mu a. A1 & A2
2) mu a. a -> (mu b. Bool -> b)  -- a and b are pos, OK
3) mu a. a -> (mu b. Int -> b)  -- a and b are pos, OK

Solution:

  1. Either, add an spl rule to the inductive relation, so it deals with the merges like the first case
  2. Or, do not split on the nested recursive type, make use of nominal unfolding?

The implication of the example

The middle type we expect does not always exist!

Solution

We have to live with distributivity, so we should only work on a single level of mu-types

Although alternative subtyping rules may be complex to design (c.f. Alternative translate subtyping , which turns out that we also need to extend the arrow rule to Siek’s style for the sake of transitivity) , we can still prove Siek’s style lemmas based on the full splitting translate rule.

Proposed lemma (Siek style with controled splitting)

Theorem: If A << [T [a- |-> {a : B}]], where T belongs to the strict split of B , then there exists

  • C as part of A, such that mcod(C) [a- |-> {a : mcod(C)}] << T [a- |-> {a : B}]
  • an invertible D, such that mcod(C) [a- |-> {a : mcod(C)}] << D [a- |-> {a : D}] << T [a- |-> {a : B}] and B << D << T

Proof draft. By induction on A << [T [a- |-> {a : B}]]

  • Case S-rec:
    • A [a- |-> {a : A}] << T [a- |-> {a : B}], we have two cases:
      1. a is weakly positive, exists:
        • C := [ A [a- |-> {a : A}]] , mcod(C) = A
        • D := T is invertible (since T is strict split, this is possible)
        • `mcod(C) [a- |→ {a : mcod(C)}] << T [a- |→ {a : T}] << T [a- |→ {a : B}]“
      2. a is not weakly positive, implying B <: A, exists:
        • C := [ A [a- |-> {a : A}]] , mcod(C) = A
        • D := A
        • mcod(C) [a- |-> {a : mcod(C)}] << A [a- |-> {a : A}] << T [a- |-> {a : B}]
  • Case andl/andr:
    • By IH we have such C and D, then exists the same C and D, we can show:
    • C is still part of A1 & A2, and the rest of the conditions holds
  • Case and:
    • This case tells us T is s-ordinary but not c-ordinary, so we CANNOT apply the IH

    Alternatively, can we consider applying the IH to a different simple split invertible type?

    • rewrite [T1 [a- |-> {a : B}]] to [T1 [a- |-> {a : T1}]… idea

Restricting the splitting rule to s-ordinary types does not help

How about we reason from A?

Proposed lemma 2 (Siek style with controled splitting + on A)

Theorem: If A << [T [a- |-> {a : B}]], where T belongs to the strict split of B , then there exists a C as part of A, such that

  1. for every [Ci [a- |-> {a : Ci}] in C, we can find Ts subset of strict split ofT such that Ci [a- |-> {a : Ci} << Ts [a- |-> {a : B}]
  2. The intersection of all Ci’s is a subtype of T (i.e. C is a subtype of T, containing sufficient fields to cover T)

Proposed lemma 3 (controled splitting + what else?)

The original theorem should still hold for c-splitting:

Theorem: If A << [T [a- |-> {a : B}]], where T belongs to the strict split of B , then there exists an invertible C, such that

  • A << [C [a- |-> {a: C}]] << [T [a- |-> {a : B}]]
  • B << A << T

For the counterexample, we can argue that the weakly positive rewriting of

  • (mu a. a -> (mu b. b -> Int & Bool -> b))
  • & (mu a. a -> (mu b. Int -> b)) are the intended middle type

Question is, how to prove this theorem, because we will get stuck in the S-and case, and the original lemma does not hold in the case of exhaustive splitting

More precise controled splitting

It turns out that, when considering c-ord and s-rod (c.f. Controled Splitting), it seems necessary to split the postive nested types while considering negative nested types as ordinary. i.e. we propose the following rules

       a in fv_neg(T)
---------------------
s-ord  [ T [a- |-> {a : B}]]


       a not in fv_neg(T)
       T1 <| T |> T2
----------------------------
[T1 [a- |-> ... ]] <| [T [a- |-> ... ]] |> [T2 [a- |-> ... ]]



a not in fv_neg(T)
sord T
---------------------
s-ord [ T [a- |-> {a : B}]]

Note, since a in fv_neg(T) indicates the whole T is negative (therefore no positive parts should be split out), I believe that list-style splitting is not necessary

The new notion of controled splitting still preserves the invertible property

Why the rules?

Consider the following example:

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

In this case, under the new consideration:
the body of the right type 
mu b. (Int -> b) & (a -> Int) is splittable 
(despite the negative a, b is positive)

so the middle type for the first fragment is
 mu a. mu b. (Int -> b)
 coming from the right
 (note, not mu a. mu b. Top -> b from the left)

and the second fragment is
mu a. mu b. a -> Int
coming from the left

While the following subtyping fails:

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

because there are negative b in the body:

	mu b. (Int -> b) &  (a -> b -> Int)

However, the refined rule still does not change the situation in The example

In other word, despite the example is weakly positive, but in order to prove soundness, we still have unsolved missing case:

With sord-splitting, we may have:

   [ A1 [a- |-> { a : A1} ] & [ A2 [a- |-> {a : A2}]]
<< [ T [a- |-> { a : B }]]

where T may = [b. T1 & T2 ], and b appears negatively in T,
so T is s-ordinary but splittable, and we might get


[ A1 [a- |-> {a : A1 }]] << [ [ T1 [b- |-> {b : T1 & T2 }] ] [a- |-> { a: B }] ]
[ A2 [a- |-> {a : A2 }]] << [ [ T2 [b- |-> {b : T1 & T2 }] ] [a- |-> { a: B }] ]




For the example, we know 
	a is weakly positive in A1 << [ T1 ... ] and A2 << [ T2 ... ]
so mu a. T1 & T2 satisfy the expected invertible type property


But the missing case we don't know how to prove is when
       a is weakly positive in A1 << [ T1 ... ]
   but not weakly positive in A2 << [ T2 [b- |-> {b : T1 & T2}] ], 
	   which implies B << A2 << [ T2 [b- |-> {b : T1 & T2}] ]

By intuition, it seems that in this case,
  A2 must also be << [T1 [b- |-> {b : T1 & T2}] ]]]
can can 

We also know that b in fv_neg(T1 & T2)

if b in fv_neg(T1)?

if b in fv_neg(T2)?

This seems hard to discuss

Problem to the more precise version

It turns out that just looking at one side (the B side) of negative variable occurrences is not enough, consider:

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

mu a. (mu b. (b -> Top) & (a -> Bool))
is s-ordinary, due to the negative b in the body

a is weakly positive in 
  [b. Top -> Int] << [b. {b : ...} -> Top]

a is negative in
  [b. a -> Bool] << [b. a -> Bool]

There are no invertible B << C << T, that serves as the middle type


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


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

Oh, the example contains toplike types, let's avoid it

We find an example that fails the Siek’s intermediate subtyping

Again, changing mu b. b -> Top to mu b. b -> Int

   mu a. (mu b. Top -> Int)
&  mu a. (mu b. a -> Bool)
<: (hold in translate subtyping, not in Siek!!!)
   mu a. (mu b. (b -> Int) & (a -> Bool))

Maybe the failure of Siek’s subtyping is related to the observation we have made that just looking at one side (the B side) of negative variable occurrences in Problem to the more precise version

Still we can work on the translate subtyping:

mu a. (mu b. (b -> Int) & (a -> Bool))
is s-ordinary, due to the negative b in the body

a is weakly positive in 
  [b. Top -> Int] << [b. {b : ... a -> ...} -> Int]

a is negative in
  [b. a -> Bool] << [b. a -> Bool]

There are no invertible B << C << T, that serves as the middle type


In translate subtyping, we have the following subtyping:
   mu a. (mu b. Top -> Int)
&  mu a. (mu b. a -> Bool)
<: Yes 
   mu a. (mu b. (b -> Int) & (a -> Bool))

Because:
  [a. [b. Top -> Int ] ]
& [a. [b. {a : 
	[b'. a -> Bool ]
	} -> Bool]]
<:
  [a. [b. 
	({ b : (b -> Int) & (a -> Bool) } -> Int)
  & ({ a : [b'. 
		({b' : ... } -> Int  )
	  & (a -> Bool ) 
	  ] 
	} -> Bool)
  ] ]

Now, let's find the middle type in the declarative system:

"merge then subtyping" fails:
   mu a. (mu b. Top -> Int)
&  mu a. (mu b. a -> Bool)
<: YES
   mu a. ((mu b. Top -> Int) & (mu b. a -> Bool))
<: NO
   mu a. (mu b. (b -> Int) & (a -> Bool))


"subtyping then merge" also fails:
   mu a. (mu b. Top -> Int)
&  mu a. (mu b. a -> Bool)
<: YES
   mu a. (mu b. b -> Int)
&  mu a. (mu b. a -> Bool)
<: YES
   mu a. ((mu b. b -> Int) & (mu b. a -> Bool))
<: No
   mu a. (mu b. (b -> Int) & (a -> Bool))



ghci> btypp xx1
(([(a,l0). [(b,l1). (Top -> Int)]]) & 
 ([(a,l0). [(b,l1). (
	    {l0:c. [(d,l3). (c -> (Int -> Int))]} 
	 -> (Int -> Int)
	 )
	 ]])
 )
ghci> btypp xx3
[(a,l0). [(b,l1). (
	(({l1:c.(((c -> Int)) & ((a -> (Int -> Int))))} -> Int)) & 
	((
		{l0:c. [(d,l3). (
			(({l3:e.(((e -> Int)) & ((c -> (Int -> Int))))} -> Int)) & 
			((c -> (Int -> Int)))
		)]} 
	-> (Int -> Int)))
)]]

Graph View

Backlinks