# Changes between Initial Version and Version 1 of TypeFunctionsSynTC/GhcChrExamples

Show
Ignore:
Timestamp:
01/18/07 03:41:34 (6 years ago)
Comment:

--

Unmodified
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}}}