Tony's Wiki

Aug 21 - Meeting

5 min read

A closer look at the negativeness checking

Fv_Neg(trans(mu a. a -> Int))
= Fv_Neg( [a. {a : a -> Int} -> Int ] )
= Fv_Pos( {a : a -> Int} )
= {}

Only with a positive a can we reveal the negativeness of the translated type

Fv_Neg(trans(mu a. a -> a))
= Fv_Neg( [a. {a : a -> a} -> a ] )
= Fv_Pos( {a : a -> a} )
= { a }

This is fine? as we always open a type before checking a negativeness

Consider checking b in mu a. a -> (mu b. a -> b)
The translation:

mu b. a -> b ~~> [b. a -> b]
   trans(mu a. a -> (mu b. a -> b) )
=  [a. {a : a -> [b. a -> b]} 
    -> [b'. {a : a -> [b. a -> b] } 
        -> b']
   ]
Fv_Neg(body) = { }

We need to count the label in!

Regarding nested recursive types (example in QuickSub)

mu b. nat -> (mu a. a -> b)

mu a. a -> b ~~> [a. {a : a -> b} -> b]
The translation is:
[b. nat 
  -> [a. {a : a -> 
            {b : nat -> [a'. {a' : a' -> b} -> b] }
         } 
       -> b] 
]

Fl_neg(body) = { b }

So, we should actually be computing Fl_neg instead of Fv_neg

The missing case

In Aug 14 - Meeting we proposed To deal with the examples we should have a rule for:


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

Examples

  1. reflexivity, OK
  2. Top Vs negative types? - single recursive type
    • (mu a. Top -> Int) & (mu a. a -> Bool) <: mu a. (a -> Int) & (a -> Bool)
    • by declarative rules: mu a. Top -> Int <: mu a. a -> Int, OK
    • by controled subtyping: the splitting rules apply, the subtyping works as well
  3. Top Vs negative types - ordinary types due to nested negativeness
    • The type in question:
      • mu b. b -> mu a. (a -> Int) & (a -> Bool) cannot be split
      • its body b -> mu a. (a -> Int) & (a -> Bool) is not ordinary
      • neither csub-mu nor csub-and apply
      • we need to apply the proposed rules
    • A subtyping example:
      • mu b. Top -> mu a. (a -> Int) & (a -> Bool) <: mu b. b -> mu a. (a -> Int) & (a -> Bool)
      • by declarative rules: nominal unfolding + reflexivity on function return type
      • by controled subtyping: we need the proposed rule, but **isomorphic check does not suffice
A CLOSER LOOK:
[b. {b : ... } -> 
	[a. { a : ... } -> Int
	  & { a : ... } -> Bool ]]
splits into:
[b. {b : b -> [a. ... ] } -> [a. { a : (a -> Int) & (a -> Bool) } -> Int ]
[b. {b : b -> [a. ... ] } -> [a. { a : (a -> Int) & (a -> Bool) } -> Bool ]

LHS:

[b. Top -> 
	[a. { a : ... } -> Int
	  & { a : ... } -> Bool ]]
splits into
[b. Top -> [a. { a : (a -> Int) & (a -> Bool) } -> Int ]
[b. Top -> [a. { a : (a -> Int) & (a -> Bool) } -> Bool ]







 cannot be split
  • Some examples that contribute to the design choice:
    • For the above right type, (mu b. Top -> (mu a. Top -> Int)) & ( mu b. Top -> (mu a. a -> Bool)) is a valid subtype, which is an intersection type instead of recursive type. Moreover, it cannot be solved by andl/andr rule
      • ⇒ For the proposed rule, the left type must be general enough
        • either a general type
        • or use some aux functions like mcod to deal with intersections
    • For the above right type (mu b. b -> (mu a. a -> Int)) & (mu b. b -> (mu a. a -> Bool)) or its merge mu b. b -> ((mu a. a -> Int) & (mu a. a -> Bool)), where the negative b is preserved instead of subsumed by Top, are forbidden
      • ⇒ For the proposed rule, it should rule out such case
        • It seems that the distinguishing feature is whether the left type contains (useful) negative variables?
B1 <| B |> B2
ordinary [ (a, l). B ]    (implying  a is in fv_neg(B))
mcod_pos(A) <: B
---------------------------
A <: [ (a, l). B ]
  • The computation of mcod_pos, should not consider deep splits, but just syntactic merges of intersections:
mcod_pos([(a, l). A]) = A     if a is not in fv_neg(A)
                      = Top   otherwise
mcod_pos(A1 & A2)     = mcod_pos(A1) & mcod_pos(A2)
  • so that we can recover the invertible translated recursive types from the algorithm in the soundness proof

TODOs

  • Implement a prototype of the algorithm, test the landscape of subtypes of the example type
  • Modify the Coq proof to accommodate the new positive/negative tests

Graph View