Tony's Wiki

Direct Splitting on Source Types

3 min read

splitting on A, 

A |> As
As = Asp ++ Asn
--------------------------
mu a. A |>  [mu a. &Asn] ++ [ mu a. Aip for Aip in Asp ]


show: when a is positive in A, 
mu a. A1 & mu a. A2 == mu a. (A1 & A2)
because
     mu a. (A1 & A2) <: mu a. A1
and  mu a. (A1 & A2) <: mu a. A2



   mu a. (Int  -> (mu b. b -> a))
 & mu a. (Bool -> (mu b. b -> a))
== mu a. ((Bool -> (mu b. b -> a)) & (String -> (mu b. b -> a)))

This idea is not working, as on the LHS there can be types that are , the splitting is not precise (information keeping)

but are the source splitting results the atomic building blocks for the actual intermediate type?

Property: forall A'~~> A B' ~~> B , if A << Bi \in spl(B), then there exists {B_s} in fspl(B'), s.t. A <: merge({B_s})

we can later define a special inductive datatype for describing merge(.) | when we replace A << Bi with A << B, the existential type is trivial, just B itself

Problem: defining merge, fspl in a structured way seems hard and ad hoc

Counterexample from QuickCheck



  test/Translate/Spec.hs:49:69: 
  1) split lemma 
       Falsified (after 7319 tests):
         STypPair mu . ((T -> mu . (((mu . (((mu . (I)) & (mu . (((T) & (I))))))) & (mu . (mu . ((((1 -> mu . (I))) & (0))))))))) mu . ((0 -> mu . (mu . (((((mu . (I)) & (mu . (((T) & (I)))))) & (mu . ((((1 -> mu . (I))) & (0)))))))))



  

a = inputTyp "mu a. (Top -> ( ((mu c. Int) & (mu d. mu e. ( (d -> Int) & e) ) )))"

b = inputTyp "mu a. (a -> ((mu c. ( Int & ( mu d. (c -> Int) & d ) ))))"

c = inputTyp "mu a. (Top -> ((mu c. ( Int & ( mu d. (c -> Int) & d ) ))))"

After debugging

 STypPair mu . ((T -> mu . (((mu . ((I -> mu . ((2 -> mu . (I)))))) & (mu . (((1) & (T)))))))) mu . ((0 -> mu . (mu . ((((I -> mu . ((2 -> mu . (I))))) & (((1) & (T))))))))


  1) split lemma split lemma
       Falsified (after 3658 tests):
         STypPair mu . ((T -> mu . (((mu . (1)) & (mu . ((1 -> mu . (I)))))))) mu . ((0 -> mu . (mu . (((1) & ((1 -> mu . (I))))))))

Graph View