Changes between Initial Version and Version 1 of TypeFunctionsSynTC/Naive


Ignore:
Timestamp:
Dec 14, 2006 12:23:36 AM (9 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/Naive

    v1 v1  
     1== A first (naive) attempt == 
     2 
     3 
     4To solve  {{{(C implies t1=t2)}}} with respect to Ax 
     5 
     6 1. We interpret Ax /\ C as a rewrite system (from left to right). 
     7 2. We exhaustively apply rewrite rules on t1 and t2, written t1 -->* t1' and t2 -->* t2' and check that t1' and t2' are syntactically equivalent. 
     8 
     9 
     10Immediately, we find a problem with this solving strategy. 
     11Consider our running example. 
     12 
     13Rewrite rules 
     14{{{ 
     15(forall a. S [a] = [S a]) /\      (R1) -- axioms 
     16(T Int = Int)                     (R2) 
     17 
     18 /\ 
     19 
     20(T [Int] = S [Int]) /\            (R3) -- local assumptions 
     21(T Int = S Int)                   (R4) 
     22 }}} 
     23 
     24applied to {{{(T [Int] = [Int])}}} 
     25 
     26yields 
     27{{{ 
     28T [Int] -->* [S Int]       (R3,R1) 
     29 
     30[Int] -->* [Int] 
     31}}} 
     32 
     33Hence, our (naive) solver fails, but 
     34clearly the (local) property  (T [Int] = [Int]) 
     35holds. 
     36 
     37The trouble here is that 
     38 
     39 * the axiom system Ax is confluent, but 
     40 * if we include the local assumptions C, the combined system Ax /\ C is non-confluent (interpreted as a rewrite system) 
     41 
     42 
     43Possible solutions: 
     44 
     45Enforce syntactic conditions such that Ax /\ C is confluent. 
     46It's pretty straightforward to enforce that Ax and 
     47constraints appearing in type annotations and data types 
     48are confluent. The tricky point is that if we combine 
     49these constraints they may become non-confluent. 
     50For example, imagine 
     51 
     52{{{ 
     53Ax : T Int = Int 
     54 
     55   a= T Int      -- from f :: a=T Int => ... 
     56 
     57      implies  
     58 
     59        (a = S Int -- from a GADT pattern 
     60 
     61            implies ...) 
     62}}} 
     63 
     64The point is that only during type checking we may 
     65encounter that Ax /\ C is non-confluent! 
     66So, we clearly need a better type checking method. 
     67 
     68