Tony's Wiki

Aug 27 - Meeting

5 min read

The modified rule:

[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]

mu a. A & mu a. B <: mu a . A & B

A <: B <: C

B1 <| B |> B2
B <: C
---------
either B1 <: C or B2 <: C

Why isomorphic check?

We want to avoid the non-derivable:

  mu b. mu a. a -> Int
& mu b. mu a. b -> Bool
<:
  mu b. mu a. (a -> Int) & (b -> Bool)
  
  translates to:
  [b. [a. {a : a -> Int} -> Int]]
& [b. [a. {b : [a. b -> Bool] } -> Bool]]
<:
  [b. [a. 
     ( {a : (a -> Int) & (b -> Bool) } -> Int )
  &. ( {b : [a. ( .... ) & (b -> Bool) ]} -> Bool )
  ]]
  
  after dropping label `b`
  [b. [a. {a : a -> Int} -> Int]]
& [b. [a. b -> Bool]]
<:
  [b. [a. 
     ( {a : (a -> Int) & (b -> Bool) } -> Int )
  &. ( b -> Bool )
  ]]
  
  the subtyping is still not isomorphic

Why part of relation?

To ensure fields can be dropped, discussed last week

Why dropLabel function

This is to ensure one-layer merge is still allowed, consider the simplest:

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

  [a. {a : a -> [b. ... ]} -> [b. ... ] ]
& [a. {a : a -> Bool} -> Bool]
<:
  [a. {a : (a -> [b. ... ]) & (a -> Bool) } -> [b. ... ]
    & {a : (a -> [b. ... ]) & (a -> Bool) } -> Bool ]

The right type will be split first

SubGoal (1)
  [a. {a : a -> [b. ... ]} -> [b. ... ]]
& [a. {a : a -> Bool} -> Bool]
<:
  [a. {a : (a -> [b. ... ]) & (a -> Bool) } -> [b. ... & ...  ]
  
  
Even after relaxed with the `partof` relation
  [a. {a : a -> [b. ... ]} -> [b. ... ]]
<:[a. {a : (a -> [b. ... ]) & (a -> Bool) } -> [b. ... ]]

Still we have negative variables, so the two types are not iso-morphic unless label a are dropped: [a. a -> Int ] ~ [a. a -> Int]

Note: the part relation must be exhaustive

 
  
 
parts :: STyp -> [STyp]
parts (SAnd a b) = parts a ++ parts b
parts (TMu a) = [TMu a]
parts (SFun a b) = [SFun a b' | b' <- parts b]
parts (SRcd l a) = [SRcd l a' | a' <- parts a]
parts t = [t]
 
  
  
 
-- [mcodPos k t] collect all the (positive) intersection components of t
mcodPos :: Int -> STyp -> [STyp]
mcodPos k (SAnd a b) = mcodPos k a ++ mcodPos k b
mcodPos k (TMu a) =
let a_open = opentl (opentt a (SVar (k))) (k) in parts a_open
mcodPos k _ = []
 
  
  
  
 
-- Helper function to fold a list of types into a single SAnd-chained type.
-- An empty list becomes STop, a single-element list is the type itself.
foldSAnd :: [STyp] -> STyp
foldSAnd [] = STop
foldSAnd [t] = t
foldSAnd (t:ts) = SAnd t (foldSAnd ts)
 
  
 
-- Generates all subsequences of the input list.
-- This is equivalent to generating the powerset.
subsequences :: [a] -> [[a]]
subsequences [] = [[]]
subsequences (x:xs) = let subs = subsequences xs
in subs ++ map (x:) subs
 
  
 
-- The main function to generate all SAnd combinations.
allMcod :: [STyp] -> [STyp]
allMcod types = map foldSAnd (subsequences types)
 
 
-- the missing case for the csub-mu rule:
saux k a (TMu b) | isJust (cspl2 (opentt b (SVar (k-1)))) = let
  fresh_k = k - 1
  b_open = opentl (opentt b (SVar fresh_k)) fresh_k
  a_open_lis = mcodPos fresh_k a
  a_open_combs = allMcod a_open_lis
  testNeg t = fresh_k `elem` flttNeg True t
in
any (\a_open ->
if testNeg a_open then
let r1 = csub (fresh_k-1) (dropLabel fresh_k a_open) (dropLabel fresh_k b_open)
    r2 = csub (fresh_k-1) (dropLabel fresh_k b_open) (dropLabel fresh_k a_open)
in r1 && r2
else csub fresh_k a_open b_open) a_open_combs

This is to ensure precise isomorphic left type can be located For example:

         (mu a. (((Int -> ((a) & (((Int) & (Top)))))) & (Top)))
         (mu a. (a -> (((mu b. (b -> ((Int) & (Top))))) & (Int))))
        <: their merge
since the right type will be split exhaustively
the precise left type also needs some exhaustive splitting to be picked

Graph View

Backlinks