Changes between Initial Version and Version 1 of TypeFunctionsSynTC/GhcChrExamples


Ignore:
Timestamp:
Jan 18, 2007 11:41:34 AM (7 years ago)
Author:
sulzmann
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSynTC/GhcChrExamples

    v1 v1  
     1{{{ 
     2A rough set of examples (using the refined 'chr-based' algorithm) 
     3 
     4 
     5Assuming a normal form of equations, it is sufficient to apply 
     6the following 'FD'-rule step. 
     7 
     8e1: F t1 = t2 
     9 
     10e2: F t1 = t3 
     11 
     12==>  
     13 
     14e1: F t1 = t2 
     15e2: F t1 = t3 
     16e3: t2 = t3 
     17 
     18where e3 =  (sym e1) trans e2 
     19 
     20 
     21Here are some examples: 
     22 
     23EXAMPLE 1 
     24 
     25Assume (given) 
     26 
     27g : forall a. S [a] = [S a]   -- axiom 
     28 
     29d1 : T Int = Int              -- local equations 
     30d2 : T [Int] = S [Int] 
     31d3 : T Int = S Int 
     32 
     33 
     34wanted 
     35 
     36? : T [Int] = [Int] 
     37 
     38 
     39Step 1: Normalize (local and wanted) equations 
     40        (also applies to axioms but we skip this step here) 
     41 
     42g : forall a. S [a] = [S a]   (0) 
     43 
     44 
     45g1 : T Int = Int       (1) 
     46g2 : T [Int] = a       (2) 
     47g3 : S [Int] = a       (3) 
     48g4 : T Int = b         (4) 
     49g5 : S Int = b         (5) 
     50 
     51 
     52? : T [Int] = [Int]    (6) 
     53 
     54Reduction steps: 
     55 
     56 
     572+6 => ?' : a = [Int] 
     58 
     59   ? = g2 trans ?' 
     60 
     6103 from 0+3 =>   
     62    g03 : a = [S Int] 
     63    g03 = (sym g3) trans (g Int) 
     64 
     65503 from 5+03 => 
     66    g503 : a = [b] 
     67    g503 = g03 trans ([] g5) 
     68 
     6914 from 1+4 => 
     70    g14 : b = Int 
     71    g14 = (sym g4) trans g1 
     72 
     73Apply 14 on 503 => 
     74    g' : a = [Int] 
     75    g' = g503 trans ([] g14) 
     76 
     77We found a match for the (reduced) wanted constraint. 
     78 
     79 ? = g2 trans ?' 
     80   = g2 trans (g503 trans ([] g14)) 
     81   = g2 trans ((g03 trans ([] g5)) trans ([] g14)) 
     82   = g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14)) 
     83 
     84How to map back to the original (given) local equations? 
     85 
     86 
     87The same calculation using the original (given) local equations. 
     88 
     89g : forall a. S [a] = [S a]  (0)   -- axiom 
     90 
     91d1 : T Int = Int        (1)      -- local equations 
     92d2 : T [Int] = S [Int]  (2) 
     93d3 : T Int = S Int      (3) 
     94 
     95wanted: 
     96d4 : T [Int] = [Int]     (4) 
     97 
     98Reduction steps: 
     99 
     10024: 2+4 => 
     101    d24 : S [Int] = [Int] 
     102    d4 = d2 trans d24       -- wanted, we're interested how to construct d4! 
     103 
     104024: 0+24 => 
     105     d024 : [S Int] = [Int] 
     106     d24 = (sym (g Int)) trans d024 
     107 
     108deompose => 
     109     d024' : S Int = Int 
     110     d024 = [] d024' 
     111 
     11213 : 1+3 => 
     113     d13 : S Int = Int 
     114     d13 = (sym d3) trans d1 
     115 
     116 
     117We found a match for the (reduced) wanted constraint. 
     118 
     119    d024' = d13 
     120          = (sym d3) trans d1 
     121 
     122Thus, 
     123 
     124d4 = d2 trans d24 
     125   = d2 trans ((sym (g Int)) trans d024) 
     126   = d2 trans ((sym (g Int)) trans ([] d024')) 
     127   = d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1))) 
     128 
     129 
     130Compare the normalized result  
     131 
     132g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14)) 
     133 
     134against the 'unnormalized' result  
     135 
     136d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1))) 
     137 
     138 
     139EXAMPLE 2 
     140 
     141no axioms involved 
     142 
     143given: 
     144d1 : G Int = Bool 
     145d2 : F (G Int) = Int 
     146 
     147wanted: 
     148 
     149d : F Bool = Int 
     150 
     151clearly d = (sym (F d1)) trans d2 
     152 
     153 
     154The normalized case: 
     155 
     156g1 : G Int = Bool   (1) 
     157g2 : G Int = a      (2) 
     158g3 : F a = Int      (3) 
     159 
     160Reductions: 
     161 
     16212 from 1 + 2 => 
     163   g12 : a = Bool 
     164   g12 = (sym g2) trans g1 
     165 
     166apply 12 on g3: 
     167 
     168   g3' : F Bool = Int 
     169   g3' = (sym (F g12)) trans g3 
     170 
     171Match found, we find 
     172 
     173d = (sym (F g12)) trans g3 
     174  = (sym (F ((sym g2) trans g1))) trans g3 
     175 
     176compare with  
     177 
     178  (sym (F d1)) trans d2 
     179}}}