Changes between Version 1 and Version 2 of TypeFunctionsSynTC


Ignore:
Timestamp:
Dec 5, 2006 4:15:07 AM (9 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC

    v1 v2  
    11= Type Checking with Indexed Type Synonyms = 
     2 
     3 
     4== Outline == 
     5 
     6 * Background  
     7 * The challenge 
     8 * A first (naive) attempt 
     9 * A second attempt 
     10    * type checking with type functions using local completion 
     11    * method can be proven correct by establishing a connection 
     12      between type function and CHR derivations 
     13 
     14== Background == 
     15 
     16GHC has now FC as its typed intermediate language. 
     17In a next step, we wish to add type functions to 
     18GHC's source language.  Type functions in combination 
     19with type annotations and GADTs allow us to type check 
     20some interesting programs. 
     21 
     22{{{ 
     23data Zero 
     24data Succ n 
     25data List a n where 
     26  Nil :: List a Zero 
     27  Cons :: a -> List a m -> List a (Succ m) 
     28 
     29type add :: * -> * -> * 
     30     add Zero x = x 
     31     add (Succ x) y = Succ (add x y) 
     32 
     33append :: List a l -> List a m -> List a (add l m) 
     34append Nil xs = xs 
     35append (Cons x xs) ys = Cons x (append xs ys) 
     36}}} 
     37 
     38However, type checking with type functions is challenging. 
     39 
     40== The challenge == 
     41 
     42Consider the axioms 
     43 
     44{{{ 
     45forall a. S [a] = [S a]   (R1) 
     46T Int = Int               (R2) 
     47}}} 
     48S and T are type functions of kind *->* 
     49For convenience, I drop the `redundant' forall a. on R1's lhs. 
     50 
     51Suppose some type annotations/pattern matchings give rise 
     52to the local assumptions 
     53 
     54{{{ 
     55T [Int] = S [Int]        (R3) 
     56T Int = S Int            (R4) 
     57}}} 
     58and under these assumptions we need to verify 
     59 
     60{{{ 
     61T Int] = [Int] 
     62}}} 
     63 
     64 
     65Logically, we can express the above as follows: 
     66 
     67{{{ 
     68(forall a. S [a] = [S a]) /\       -- axioms 
     69(T Int = Int) 
     70 
     71 |= 
     72 
     73(T [Int] = S [Int]) /\             -- local assumptions 
     74(T Int = S Int) 
     75 
     76 implies 
     77 
     78(T [Int] = [Int])                  -- (local) property 
     79}}} 
     80That is, any model (in the first-order sense) which is 
     81a model of the axioms and local assumptions is also 
     82a model of the property. 
     83 
     84NOTE: There are further axioms such as reflexitivity of = etc. 
     85We'll leave them our for simplicitiy. 
     86 
     87The all important question: 
     88How can we algorithmically check the above statement? 
     89Roughly, we perform the following two steps. 
     90 
     91 
     921. Generate the appropriate implication constraint out of the program text.  That's easy cause GHC supports now implication constraints. 
     93(there are some potential subtleties, see GENERATEIMP below). 
     94 
     952. Solve the implication constraint by applying axioms and local assumptions until the (local) property is verified. That's the hard part. 
     96 
     97NOTE:  
     98 
     99We assume that (implication) constraints consist of  equality constraints only. In general, we'll also find type class constraints. We ignore such constraints  for the moment. 
     100 
     101In the following, we assume that symbols t refer to types and symbols C refer to conjunctions of equality constraints and Ax refers to an axiom set. 
     102 
     103We'll restrict ourselves to simple implication constraints of the form {{{   C implies t1=t2 }}} 
     104In general, implication constraints may be nested, e.g 
     105{{{ C1 implies (C2 implies C3) }}} and may contain conjunctions 
     106of implications, e.g. {{{C1 implies (F1 /\ F2)}}} where F1 and F2 are arbitrary implication constraints. Implication constraints may be universally quantified, e.g.  
     107{{{ forall a (S a = T a implies ...) }}} 
     108These universal quantifiers arise from universal type annotations, e.g.  {{{ f :: S a = T a => ....}}}, and 
     109pattern matchings over data types with abstract components, e.g. data Foo where 
     110{{{ K :: S a = T a => a -> Foo}}} 
     111We can operationally deal with universally quantified variables by skolemizing them (and we must ensure that skolemized/universal variables do not escape). 
     112 
     113End of NOTE 
     114 
     115 
     116== A first (naive) attempt == 
     117 
     118 
     119To solve  {{{(C implies t1=t2)}}} with respect to Ax 
     120 
     1211. We interpret Ax /\ C as a rewrite system (from left to right). 
     122 
     1232. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. 
     124 
     125 
     126Immediately, we find a problem with this solving strategy. 
     127Consider our running example. 
     128 
     129Rewrite rules 
     130{{{ 
     131(forall a. S [a] = [S a]) /\      (R1) -- axioms 
     132(T Int = Int)                     (R2) 
     133 
     134 /\ 
     135 
     136(T [Int] = S [Int]) /\            (R3) -- local assumptions 
     137(T Int = S Int)                   (R4) 
     138 }}} 
     139 
     140applied to {{{(T [Int] = [Int])}}} 
     141 
     142yields 
     143{{{ 
     144T [Int] -->* [S Int]       (R3,R1) 
     145 
     146[Int] -->* [Int] 
     147}}} 
     148 
     149Hence, our (naive) solver fails, but 
     150clearly the (local) property  (T [Int] = [Int]) 
     151holds. 
     152 
     153The trouble here is that 
     154 
     155* the axiom system Ax is confluent but if we included the local assumptions C 
     156 
     157* the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) 
     158 
     159 
     160Possible solutions: 
     161 
     162Enforce syntactic conditions such that Ax /\ C is confluent. 
     163It's pretty straightforward to enforce that Ax and 
     164constraints appearing in type annotations and data types 
     165are confluent. The tricky point is that if we combine 
     166these constraints they may become non-confluent. 
     167For example, imagine 
     168 
     169{{{ 
     170Ax : T Int = Int 
     171 
     172   a= T Int      -- from f :: a=T Int => ... 
     173 
     174      implies  
     175 
     176        (a = S Int -- from a GADT pattern 
     177 
     178            implies ...) 
     179}}} 
     180 
     181The point is that only during type checking we may 
     182encounter that Ax /\ C is non-confluent! 
     183So, we clearly need a better type checking method. 
     184 
     185 
     186 
     187== A second attempt == 
     188 
     189To solve  {{{(C implies t1=t2)}}} with respect to Ax 
     190 
     1911. a. We interpret Ax /\ C as a rewrite system (from left to right)       and  
     192 
     193   b. perform completion until the rewrite system is confluent. 
     194 
     1952. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. 
     196 
     197 
     198Step 1b) is new and crucial. For confluent rewrite systems the 
     199checking step 2) will work fine (we also need termination of course). 
     200But how do we now that completion will succeed? 
     201The important condition is to guarantee that Ax is confluent (and 
     202terminating) then completion will be successful (i.e. terminated 
     203and produce a confluent rewrite system). 
     204 
     205Let's take a look at our running example. 
     206{{{ 
     207(forall a. S [a] = [S a]) /\      (R1) -- axioms 
     208(T Int = Int)                     (R2) 
     209 
     210 /\ 
     211 
     212(T [Int] = S [Int]) /\            (R3) -- local assumptions 
     213(T Int = S Int)                   (R4) 
     214}}} 
     215The axioms are clearly confluent 
     216but there's a critical pair between (R2,R4). 
     217 
     218Completion yields 
     219 
     220{{{ 
     221(S Int = Int)                     (R5) 
     222}}} 
     223Now, we can verify that (T [Int] = [Int]) 
     224 
     225by executing 
     226 
     227{{{ 
     228T [Int] -->* [Int]       (R3,R1,R5) 
     229 
     230[Int] -->* [Int] 
     231}}} 
     232 
     233The completion method in more detail. 
     234 
     235=== There are two kinds of critical pairs === 
     236 
     237* Axiom vs local assumption, see (R2,R4) above 
     238* Local assumption vs local assumption. For example, 
     239{{{ 
     240  T Int = S Int  /\  
     241  T Int = R Int 
     242}}} 
     243  Completion yields 
     244{{{ 
     245  S Int = R Int 
     246  R Int = S Int 
     247}}} 
     248 
     249NOTE: Axiom vs axiom impossible cause axiom set is confluent 
     250 
     251 
     252Towards establishing a connection between completion and CHR derivation steps  
     253 
     254 
     255NOTE:  
     256 
     257There's a straightforward translation from type functions to constraints. For each n-ary function symbol T, we introduce a n+1-ary constraint symbol T. Thus, we can represent  
     258{{{T Int = Int}}}  as 
     259{{{ T Int a /\ a=Int}}} 
     260For example, {{{T Int = S Int}}} is represented by  
     261{{{T Int a /\ S Int b /\ a=b}}} 
     262 
     263 
     264We can verify that the completion method success by showing that each critical pair arises in the `corresponding' CHR derivation (this derivation terminates if the axiom system is confluent and terminating, hence, we'll only encounter a finite number of critical pairs, hence, completion terminates). 
     265 
     266Recall the critical pair (axioms vs local assumption) from above 
     267{{{ 
     268T Int = Int     -- axiom 
     269T Int = S Int  -- local assumption 
     270}}} 
     271In the CHR world, we'll represent both as 
     272{{{ 
     273T Int a <==> a=Int         -- axiom turned into CHR 
     274 
     275T Int b /\ S Int c /\ b=c  -- local assumption turned into CHR 
     276                           -- constraints 
     277}}} 
     278In the CHR world, we find that 
     279{{{ 
     280    T Int b /\ S Int c /\ b=c 
     281--> b=Int /\ S Int c /\ b=c      -- apply CHR 
     282<--> b=Int /\ c=Int /\ S Int Int -- equivalence transformation 
     283                                 -- apply mgu 
     284}}} 
     285directly corresponds to  
     286{{{ 
     287S Int = Int 
     288}}} 
     289generated by our completion method 
     290 
     291Recall the critical pair (local assumption vs local assumption) 
     292{{{ 
     293  T Int = S Int  /\  
     294  T Int = R Int 
     295}}} 
     296represented in the CHR world as 
     297{{{ 
     298 T Int a /\ S Int b /\ a=b /\ 
     299 T Int c /\ R Int d /\ c=d 
     300}}} 
     301In the CHR world, we find that 
     302{{{ 
     303    T Int a /\ S Int b /\ a=b /\ 
     304    T Int c /\ R Int d /\ c=d 
     305-->T Int a /\ S Int b /\ a=b /\   
     306   c=a /\ R Int d /\ c=d 
     307 
     308      -- apply FD rule 
     309      -- T a b /\ T a c ==> b=c 
     310 
     311<--> T Int a /\ S Int a /\ R Int a /\ 
     312     a=b, c=a, d=a 
     313}}} 
     314  directly corresponds to 
     315{{{ 
     316    S Int = R Int 
     317    R Int = S Int 
     318}}} 
     319 
     320The general cases are as follows. 
     321 
     322==== axiom vs local assumption case ==== 
     323 
     324{{{ 
     325forall as. (T t1 ... tn = s)  -- axiom 
     326 
     327T t1' ... tn' = s'            -- local assumption 
     328}}} 
     329where exist phi, dom(phi)=as such that phi(ti) = ti' for i=1,...,n 
     330 
     331 
     332completion yields 
     333{{{ 
     334    s' = phi(s) 
     335    phi(s) = s'        
     336}}} 
     337 
     338NOTE: We may need both orientation see above example. 
     339We assume that symbol t refers to types NOT containing type functions and s refers to types which may contain type functions (can be lifted, more below) 
     340 
     341 
     342Explaining completion in terms of CHRs. 
     343Above translates to 
     344{{{ 
     345T t1 ... tn b <==> C 
     346 
     347T t1' ... tn' b' /\ C' 
     348}}} 
     349where  s is translated to (C | b) and s' is translated to (C | b') 
     350 
     351(see above where each type function type is represented by 
     352a variable under some CHR constraints) 
     353 
     354The type functions 
     355{{{ 
     356    s' = phi(s) 
     357    phi(s) = s'        
     358}}} 
     359resulting from completion 'appear' in the CHR derivation 
     360(i.e. the operational effect is the same) 
     361{{{ 
     362     T t1' ... tn' b' /\ C'    -- apply CHR 
     363--> b=b', phi(C) /\ C' 
     364}}} 
     365 
     366==== local assumption vs local assumption ==== 
     367 
     368{{{ 
     369T t1 ... tn = s1 
     370T t1 ....tn = sn 
     371}}} 
     372 
     373completion yields 
     374{{{ 
     375  s1 = s2 
     376  s2 = s1 
     377}}} 
     378In the CHR world, above represented by 
     379 
     380{{{ 
     381T t1 ... tn a /\ C1 
     382T t1 ....tn b /\ C2 
     383}}} 
     384where s1 translated to (C1 | a) 
     385      s2 translated to (C1 | n) 
     386 
     387Then,  
     388{{{ 
     389    T t1 ... tn a /\ C1 /\ 
     390    T t1 ....tn b /\ C2 
     391 
     392--> FD rule step 
     393 
     394    T t1 ... tn a /\ C1 /\ 
     395    a=b /\ [a/b] C2 
     396}}} 
     397 
     398Again, the operational effect of the type function generated 
     399is also present in the CHR derivation 
     400 
     401 
     402Lifting the restriction that t refers to types NOT containing 
     403type functions (we only lift this restriction for 
     404local assumptions). 
     405 
     406Consider 
     407{{{ 
     408forall a. T [a] = [T a]      -- axiom 
     409 
     410T [S Int] = s                -- local assumption 
     411}}} 
     412 
     413We can normalize 
     414{{{ 
     415T [S Int] = s 
     416}}} 
     417to 
     418{{{ 
     419T [b] = s 
     420S Int = b 
     421}}} 
     422Method from above applies then. 
     423 
     424NOTE: Regarding generation of implication constraints. 
     425GENERATEIMP 
     426 
     427The literate implication constraints generated out of the 
     428program text may look as follows 
     429{{{ a=T Int implies ( a= S Int implies ...) 
     430}}} 
     431 
     432The above can be simplified to 
     433{{{ (a=T Int /\ a = S Int) implies ...}}} 
     434Before we proceed with the completion method, we first 
     435need to apply some closure rules (eg. transitivity, left, right etc) 
     436Hence, from the above we generatet 
     437{{{a=T Int /\ a = S Int /\  
     438   T Int = a /\ S Int = a /\       -- symmetry 
     439   T Int = S Int /\ S Int = T Int  -- transitivity 
     440}}} 
     441We omit the trival (reflexive) equations 
     442{{{ T Int = T Int /\ S Int = S Int }}}