Changes between Initial Version and Version 1 of TypeFunctionsSynTC/GhcChrExamples

Timestamp:

01/18/07 03:41:34 (6 years ago)

Author:

sulzmann

Comment:

--

TypeFunctionsSynTC/GhcChrExamples

@@ +1 @@
+{{{
+A rough set of examples (using the refined 'chr-based' algorithm)
+
+
+Assuming a normal form of equations, it is sufficient to apply
+the following 'FD'-rule step.
+
+e1: F t1 = t2
+
+e2: F t1 = t3
+
+==> 
+
+e1: F t1 = t2
+e2: F t1 = t3
+e3: t2 = t3
+
+where e3 =  (sym e1) trans e2
+
+
+Here are some examples:
+
+EXAMPLE 1
+
+Assume (given)
+
+g : forall a. S [a] = [S a]   -- axiom
+
+d1 : T Int = Int              -- local equations
+d2 : T [Int] = S [Int]
+d3 : T Int = S Int
+
+
+wanted
+
+? : T [Int] = [Int]
+
+
+Step 1: Normalize (local and wanted) equations
+        (also applies to axioms but we skip this step here)
+
+g : forall a. S [a] = [S a]   (0)
+
+
+g1 : T Int = Int       (1)
+g2 : T [Int] = a       (2)
+g3 : S [Int] = a       (3)
+g4 : T Int = b         (4)
+g5 : S Int = b         (5)
+
+
+? : T [Int] = [Int]    (6)
+
+Reduction steps:
+
+
+2+6 => ?' : a = [Int]
+
+   ? = g2 trans ?'
+
+03 from 0+3 =>  
+    g03 : a = [S Int]
+    g03 = (sym g3) trans (g Int)
+
+503 from 5+03 =>
+    g503 : a = [b]
+    g503 = g03 trans ([] g5)
+
+14 from 1+4 =>
+    g14 : b = Int
+    g14 = (sym g4) trans g1
+
+Apply 14 on 503 =>
+    g' : a = [Int]
+    g' = g503 trans ([] g14)
+
+We found a match for the (reduced) wanted constraint.
+
+ ? = g2 trans ?'
+   = g2 trans (g503 trans ([] g14))
+   = g2 trans ((g03 trans ([] g5)) trans ([] g14))
+   = g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14))
+
+How to map back to the original (given) local equations?
+
+
+The same calculation using the original (given) local equations.
+
+g : forall a. S [a] = [S a]  (0)   -- axiom
+
+d1 : T Int = Int        (1)      -- local equations
+d2 : T [Int] = S [Int]  (2)
+d3 : T Int = S Int      (3)
+
+wanted:
+d4 : T [Int] = [Int]     (4)
+
+Reduction steps:
+
+24: 2+4 =>
+    d24 : S [Int] = [Int]
+    d4 = d2 trans d24       -- wanted, we're interested how to construct d4!
+
+024: 0+24 =>
+     d024 : [S Int] = [Int]
+     d24 = (sym (g Int)) trans d024
+
+deompose =>
+     d024' : S Int = Int
+     d024 = [] d024'
+
+13 : 1+3 =>
+     d13 : S Int = Int
+     d13 = (sym d3) trans d1
+
+
+We found a match for the (reduced) wanted constraint.
+
+    d024' = d13
+          = (sym d3) trans d1
+
+Thus,
+
+d4 = d2 trans d24
+   = d2 trans ((sym (g Int)) trans d024)
+   = d2 trans ((sym (g Int)) trans ([] d024'))
+   = d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1)))
+
+
+Compare the normalized result 
+
+g2 trans ((((sym g3) trans (g Int)) trans ([] g5)) trans ([] g14))
+
+against the 'unnormalized' result 
+
+d2 trans ((sym (g Int)) trans ([] ((sym d3) trans d1)))
+
+
+EXAMPLE 2
+
+no axioms involved
+
+given:
+d1 : G Int = Bool
+d2 : F (G Int) = Int
+
+wanted:
+
+d : F Bool = Int
+
+clearly d = (sym (F d1)) trans d2
+
+
+The normalized case:
+
+g1 : G Int = Bool   (1)
+g2 : G Int = a      (2)
+g3 : F a = Int      (3)
+
+Reductions:
+
+12 from 1 + 2 =>
+   g12 : a = Bool
+   g12 = (sym g2) trans g1
+
+apply 12 on g3:
+
+   g3' : F Bool = Int
+   g3' = (sym (F g12)) trans g3
+
+Match found, we find
+
+d = (sym (F g12)) trans g3
+  = (sym (F ((sym g2) trans g1))) trans g3
+
+compare with 
+
+  (sym (F d1)) trans d2
+}}}