-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathopenrecursion.fdoc
314 lines (272 loc) · 10.8 KB
/
openrecursion.fdoc
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
@tangler openrec.flx = examples/openrecursion/openrec.flx
@title Open Recursion
@H1 Designing with Open Recursion
Open recursion is s technique where recursion in both a data type
and the functions that access it are provided in two stages.
For the data:
<ol>
<li>The recursion is replaced by a type variable to produce a flat non-recursive type</li>
<li>Ihe type variable is bound to the type, introducing recursion.</li>
</ol>
For the functions:
<ol>
<li>The recursive application is replaced by a call to a paramater</li>
<li>The function is closed by calling it with itself as the parameter</li>
</ol>
For these techniques to work, an extensible polymorphic data type
is required, higher order functions must be supported, and the fixpoint
operator for both types and functions must be representable. C++ for example
cannot support this technique because the fixpoint operations cannot
be encoded.
The principle reason for using this technique is that that it supports
the open/closed priniple. That is, it allow a closed system to be defined
and operational, which can be extended covariantly to a more featured system
without modifying the original code or disrupting old working programs.
@h1 A simple example.
Here is a simple example. We are going to start with a simple expression
representation that supports addition of integers and extend it to
also support subtraction. Then we will provide a separate extension
to support multiplication. Finally we will extend both of these
extensions together to throw in division.
@pre
add
/ \
sub mul
\ /
div
@
This is a typical OO mixing subtyping diagram, but we will be using
functional techniques. There is no way to do this with object orientation
because of the covariance problem.
@h2 The base case: addition.
Our target data type is this:
@felix
typedef adde = (
`Int of int
`Add of adde * adde
);
@
Notice, it is a recursive data type. The function we want is
@felix
fun evala (term: adde) =>
match term with
| `Int j => j
| `Add (a,b) => evala a + evala b
endmatch
;
@
Again notice it is a recursive function. We are going to recode
our system using open recursion now. Here's the open version of the
data type:
@tangle openrec.flx
typedef o_adde[T] = (
| `Int of int
| `Add of T * T
);
@
Notice this data type is now polymorphic, but no longer recursive.
The type variable has eliminated the recursion.
And here's the open version of the function:
@tangle openrec.flx
fun o_evala[T] (eval: T -> int) (term: o_adde[T]) =>
match term with
| `Int j => j
| `Add (a,b) => eval a + eval b
endmatch
;
@
Again, the function has become polymorphic, and has also acquired
an extra parameter which is used to eliminate the recursive calls.
Now we are going to recover the original data type and function:
@tangle openrec.flx
typedef adde = o_adde[adde];
fun evala (term:adde):int => o_evala[adde] evala term;
@
What we have done is close the open data type by
replacing the type variable with a self-reference.
Similarly, we have closed the function, by replacing
the parameter with a self reference, so that the closed
function now calls itself. Notice that in Felix, the return type
of the recursion must be specified.
Here is a test case:
@tangle openrec.flx
var xa : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
var yaa = evala xa;
println$ "ya="+yaa.str;
@
@h2 Extension to subtraction
Now we're going to add a new feature: subtraction.
Here is the open version of the type and evaluator:
@tangle openrec.flx
typedef o_sube[T] = (
| o_adde[T]
| `Sub of T * T
);
fun o_evals[T] (eval: T -> int) (term: o_sube[T]):int =>
match term with
| `Sub (a,b) => eval a - eval b
| o_adde[T] :>> k => o_evala eval k
endmatch
;
@
Notice both the type and function delegate to the existing code for addition
and only add support for our new operation, subtraction.
@h2 Fixpoint operator.
The closure of the the open type and function is called <em>fixating</em> them.
What we have done is to manually introduce the self-reference.
For the data type, we used a self-refering type alias; for the function
we used eta-expansion.
It is possible to automate both these operations so they work on any suitably
structured open types and functions using combinators called <em>fixpoint operators</em>.
Here's how we do it:
@tangle openrec.flx
typefun o_sube_f (T:TYPE) : TYPE => o_sube[T];
typedef sube = tfix<TYPE> o_sube_f;
fun evals (term:sube):int => (fix[sube,int] o_evals[sube]) term;
@
Here are the definitions from the standard library:
@felix
fun fix[D,C] (f:(D->C)->D->C) (x:D) : C => f (fix f) x;
typefun tfix<K> (f: K ->K):K => f x as x:K;
@
the type fixpoint cheats: it uses thefixpoint operator @{as}
which is builtin to the type system in the compiler.
The function fixpoint operator is interesting because its
rather nasty type is what is required for an eager language.
Lasy languages like Haskell have a simpler type for their
function fixpoint operator.
Finally a test case:
@tangle openrec.flx
var xs : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
var yss = evals xs;
var ysa = evals xa; // ORGINAL DATA
println$ "ys="+yss.str;
println$ "ya="+ysa.str;
@
It's very important to notice that the original data also works with
the new function! Of course it's obvious why: the function @{sube}
delegates to @{adde} in that case.
Well .. actually it's <em>not at all obvious</em> when you think about it.
What happens if you're adding two terms, one of which is a subtraction?
How can the @{adde} routine which appears to know nothing about subtraction
do this?
The answer of course is we passed @{sube} to it as a parameter!
What's critical is this: the extenion is <em>covariant</em> and in particular
the type @{adde} is a <em>subtype</em> of @{sube}.
@h2 Extension to multiplication
Now we're going to make a second extension to the addition system to support
multiplication. It follows a similar pattern to subtraction of course:
@tangle openrec.flx
typedef o_mule[T] = (
| o_adde[T]
| `Mul of T * T
);
fun o_evalm[T] (eval: T -> int) (term: o_mule[T]):int =>
match term with
| `Mul(a,b) => eval a * eval b
| o_adde[T] :>> k => o_evala eval k
endmatch
;
typefun o_mule_f (T:TYPE) : TYPE => o_mule[T];
typedef mule = tfix<TYPE> o_mule_f;
fun evalm (term:mule):int => (fix[mule,int] o_evalm[mule]) term;
var xm : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
var ymm = evalm xm;
var yma = evalm xa; // ORGINAL DATA
println$ "ym="+ymm.str;
println$ "ya="+yma.str;
@
@h2 Mixing it all together
We're no going to mix it all together and also add division.
@tangle openrec.flx
typedef o_dive[T] = (
| o_sube[T]
| o_mule[T]
| `Div of T * T
);
fun o_evald[T] (eval: T -> int) (term: o_dive[T]):int =>
match term with
| `Div(a,b) => eval a / eval b
| o_sube[T] :>> k => o_evals eval k
| o_mule[T] :>> k => o_evalm eval k
endmatch
;
typefun o_dive_f (T:TYPE) : TYPE => o_dive[T];
typedef dive = tfix<TYPE> o_dive_f;
fun evald (term:dive):int => (fix[dive,int] o_evald[dive]) term;
var xd : dive =
`Add (
`Mul (
`Int 39,
`Sub (
`Int 3,
`Div (`Int 2, `Int 2)
)
)
,
`Int 66
)
;
var ydd = evald xd;
var yda = evald xa; // ORGINAL DATA
var yds = evald xs; // ORGINAL DATA
var ydm = evald xm; // ORGINAL DATA
println$ "yd="+ydd.str;
println$ "ya="+yda.str;
println$ "ys="+yds.str;
println$ "ym="+ydm.str;
@
@h1 Open/Closed Principle
In "Object Oriented Software Construction" Bertran Meyer named a crucial
system design principe the "Open/Closed Principle". It states that a system
should have a unit of modularity which is simultaneously closed so it can
be used and also open so it can be extended. This gave rise to the idea
of classes which are closed object factories, but can be extended by
inheritance.
The object oriented version of classes is a catastrophic failure bccause
of severe restrictions imposed by type systems on the type of arguments of methods,
which must be contravariant (or invariant), whereas usually we require covariance.
Open recursion solves this problem by providing types and function which are
open to extension, and do not suffer fron the covariance problem because
type variables are invariant.
The system then provides a closure operator, namely the fixpoint operator,
which locks in covariant behaviour of a particular extension of the base type.
The types as coproducts, which are covariant, and so base types are subtypes
of extensions. This impplies the methods of an extension will continue to work
with data of the base type.
@h2 Issues with polymorphic variants
Polymorphic variants (as in Felix or Ocaml) are essential for open recursion
to work. However as is the case with all structural types with user supplied
componenmts, including records, compiler error diagnostics are very hard to
understand due at least in part the fact that all the components must be listed
to identify the type. By contrast, nominal types are easy to refer to, since
they have a single unique and simple name.
Ocaml has made significant progress in this area by the diagnostics ability
to search the symbol to table to see if a compnent set happens to have a named
alias.
@h2 Multivariant Open Recursion
In our simple example, the open version of a type has a single type variable,
and the open version of a function has a functional parameter: the type variable
and the paramater are eliminated by self-reference by using the fixpoint operators.
However in complex systems such as a compiler, we usually have main types,
and auxilliay types they depend on; sometimes, we have two of more major
types which are convoluted and inseparable: in these cases two or more
type variables and function parameters may be required
This leads to a very difficult combinatorial explosion because now we
can fixate one type variable whilst leaving the other open. Multiple extensions
of one type can be used with multiple extensions of another.
In Felix, the type system terms in the compiler have at least 6 auxilliary types
for which multiple flat extensions cold be provided leading to an unmanagably
large potential set of closed terms. of course this is <em>not</em> a problem
with open recursion at all: it is a simple fact, and a blessing that open recursion
provides the machine to represent these choices. The existence of fixpoint combinators
are then crucial because fixation closures are anonymous and can be provided as required
"on the fly".
Nevertheless, using this technology in complex applications whilst the very environment
where the modularity provided is of most benefit, is also the environment where
it is hardest to get right. In the Felix compiler I found it so difficult,
dynamic typing was prefered; that is, handling terms that should have been
erased by throwing an exception was a lot easier than constructing a type
for every use case so as to obtain a compile time error.
I think it remains to develop language constructions that can leverage
this technology in a more manageable way.