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