Changes between Initial Version and Version 1 of TypeFunctionsSynTC/GhcChrExamples


Ignore:
Timestamp:
Jan 18, 2007 11:41:34 AM (9 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}}}