Skip to content

Commit bf98b44

Browse files
skallerskaller
committedMar 9, 2024
name change to make it easier to follow
1 parent 0fd3c7e commit bf98b44

File tree

3 files changed

+238
-111
lines changed

3 files changed

+238
-111
lines changed
 

‎examples/openrecursion/openrec.flx

+34-34
Original file line numberDiff line numberDiff line change
@@ -4,76 +4,76 @@ typedef o_adde[T] = (
44
| `Add of T * T
55
);
66
#line 79 "openrecursion.fdoc"
7-
fun o_eval[T] (eval: T -> int) (term: o_adde[T]) =>
7+
fun o_evala[T] (eval: T -> int) (term: o_adde[T]) =>
88
match term with
99
| `Int j => j
1010
| `Add (a,b) => eval a + eval b
1111
endmatch
1212
;
1313
#line 91 "openrecursion.fdoc"
1414
typedef adde = o_adde[adde];
15-
fun eval (term:adde):int => o_eval[adde] eval term;
15+
fun evala (term:adde):int => o_evala[adde] evala term;
1616
#line 103 "openrecursion.fdoc"
17-
var x : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
18-
var y = eval x;
19-
println$ y;
17+
var xa : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
18+
var yaa = evala xa;
19+
println$ "ya="+yaa.str;
2020
#line 113 "openrecursion.fdoc"
2121
typedef o_sube[T] = (
2222
| o_adde[T]
2323
| `Sub of T * T
2424
);
25-
fun o_eval2[T] (eval: T -> int) (term: o_sube[T]):int =>
25+
fun o_evals[T] (eval: T -> int) (term: o_sube[T]):int =>
2626
match term with
2727
| `Sub (a,b) => eval a - eval b
28-
| o_adde[T] :>> k => o_eval eval k
28+
| o_adde[T] :>> k => o_evala eval k
2929
endmatch
3030
;
3131
#line 139 "openrecursion.fdoc"
3232
typefun o_sube_f (T:TYPE) : TYPE => o_sube[T];
3333
typedef sube = tfix<TYPE> o_sube_f;
34-
fun eval2 (term:sube):int => (fix[sube,int] o_eval2[sube]) term;
34+
fun evals (term:sube):int => (fix[sube,int] o_evals[sube]) term;
3535
#line 160 "openrecursion.fdoc"
36-
var x2 : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
37-
var y2 = eval2 x2;
38-
var y3 = eval2 x; // ORGINAL DATA
39-
println$ y2;
40-
println$ y3;
36+
var xs : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
37+
var yss = evals xs;
38+
var ysa = evals xa; // ORGINAL DATA
39+
println$ "ys="+yss.str;
40+
println$ "ya="+ysa.str;
4141
#line 187 "openrecursion.fdoc"
4242
typedef o_mule[T] = (
4343
| o_adde[T]
4444
| `Mul of T * T
4545
);
46-
fun o_eval3[T] (eval: T -> int) (term: o_mule[T]):int =>
46+
fun o_evalm[T] (eval: T -> int) (term: o_mule[T]):int =>
4747
match term with
4848
| `Mul(a,b) => eval a * eval b
49-
| o_adde[T] :>> k => o_eval eval k
49+
| o_adde[T] :>> k => o_evala eval k
5050
endmatch
5151
;
5252
typefun o_mule_f (T:TYPE) : TYPE => o_mule[T];
5353
typedef mule = tfix<TYPE> o_mule_f;
54-
fun eval3 (term:mule):int => (fix[mule,int] o_eval3[mule]) term;
55-
var x3 : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
56-
var y4 = eval3 x3;
57-
var y5 = eval3 x; // ORGINAL DATA
58-
println$ y4;
59-
println$ y5;
54+
fun evalm (term:mule):int => (fix[mule,int] o_evalm[mule]) term;
55+
var xm : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
56+
var ymm = evalm xm;
57+
var yma = evalm xa; // ORGINAL DATA
58+
println$ "ym="+ymm.str;
59+
println$ "ya="+yma.str;
6060
#line 211 "openrecursion.fdoc"
6161
typedef o_dive[T] = (
6262
| o_sube[T]
6363
| o_mule[T]
6464
| `Div of T * T
6565
);
66-
fun o_eval4[T] (eval: T -> int) (term: o_dive[T]):int =>
66+
fun o_evald[T] (eval: T -> int) (term: o_dive[T]):int =>
6767
match term with
6868
| `Div(a,b) => eval a / eval b
69-
| o_sube[T] :>> k => o_eval2 eval k
70-
| o_mule[T] :>> k => o_eval3 eval k
69+
| o_sube[T] :>> k => o_evals eval k
70+
| o_mule[T] :>> k => o_evalm eval k
7171
endmatch
7272
;
7373
typefun o_dive_f (T:TYPE) : TYPE => o_dive[T];
7474
typedef dive = tfix<TYPE> o_dive_f;
75-
fun eval4 (term:dive):int => (fix[dive,int] o_eval4[dive]) term;
76-
var x4 : dive =
75+
fun evald (term:dive):int => (fix[dive,int] o_evald[dive]) term;
76+
var xd : dive =
7777
`Add (
7878
`Mul (
7979
`Int 39,
@@ -86,11 +86,11 @@ var x4 : dive =
8686
`Int 66
8787
)
8888
;
89-
var y6 = eval4 x4;
90-
var y7 = eval4 x; // ORGINAL DATA
91-
var y8 = eval4 x2; // ORGINAL DATA
92-
var y9 = eval4 x3; // ORGINAL DATA
93-
println$ y6;
94-
println$ y7;
95-
println$ y8;
96-
println$ y9;
89+
var ydd = evald xd;
90+
var yda = evald xa; // ORGINAL DATA
91+
var yds = evald xs; // ORGINAL DATA
92+
var ydm = evald xm; // ORGINAL DATA
93+
println$ "yd="+ydd.str;
94+
println$ "ya="+yda.str;
95+
println$ "ys="+yds.str;
96+
println$ "yn="+ydm.str;

‎openrecursion.fdoc

+102-37
Original file line numberDiff line numberDiff line change
@@ -55,10 +55,10 @@ typedef adde = (
5555
@
5656
Notice, it is a recursive data type. The function we want is
5757
@felix
58-
fun eval (term: adde) =>
58+
fun evala (term: adde) =>
5959
match term with
6060
| `Int j => j
61-
| `Add (a,b) => eval a + eval b
61+
| `Add (a,b) => evala a + evala b
6262
endmatch
6363
;
6464
@
@@ -76,7 +76,7 @@ The type variable has eliminated the recursion.
7676

7777
And here's the open version of the function:
7878
@tangle openrec.flx
79-
fun o_eval[T] (eval: T -> int) (term: o_adde[T]) =>
79+
fun o_evala[T] (eval: T -> int) (term: o_adde[T]) =>
8080
match term with
8181
| `Int j => j
8282
| `Add (a,b) => eval a + eval b
@@ -89,7 +89,7 @@ an extra parameter which is used to eliminate the recursive calls.
8989
Now we are going to recover the original data type and function:
9090
@tangle openrec.flx
9191
typedef adde = o_adde[adde];
92-
fun eval (term:adde):int => o_eval[adde] eval term;
92+
fun evala (term:adde):int => o_evala[adde] evala term;
9393
@
9494
What we have done is close the open data type by
9595
replacing the type variable with a self-reference.
@@ -100,9 +100,9 @@ of the recursion must be specified.
100100

101101
Here is a test case:
102102
@tangle openrec.flx
103-
var x : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
104-
var y = eval x;
105-
println$ y;
103+
var xa : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
104+
var yaa = evala xa;
105+
println$ "ya="+yaa.str;
106106
@
107107

108108
@h2 Extension to subtraction
@@ -114,18 +114,18 @@ typedef o_sube[T] = (
114114
| o_adde[T]
115115
| `Sub of T * T
116116
);
117-
fun o_eval2[T] (eval: T -> int) (term: o_sube[T]):int =>
117+
fun o_evals[T] (eval: T -> int) (term: o_sube[T]):int =>
118118
match term with
119119
| `Sub (a,b) => eval a - eval b
120-
| o_adde[T] :>> k => o_eval eval k
120+
| o_adde[T] :>> k => o_evala eval k
121121
endmatch
122122
;
123123
@
124124
Notice both the type and function delegate to the existing code for addition
125125
and only add support for our new operation, subtraction.
126126

127127
@h2 Fixpoint operator.
128-
The closure of the the open type and function ic called <em>fixating</em> them.
128+
The closure of the the open type and function is called <em>fixating</em> them.
129129
What we have done is to manually introduce the self-reference.
130130
For the data type, we used a self-refering type alias; for the function
131131
we used eta-expansion.
@@ -138,7 +138,7 @@ Here's how we do it:
138138
@tangle openrec.flx
139139
typefun o_sube_f (T:TYPE) : TYPE => o_sube[T];
140140
typedef sube = tfix<TYPE> o_sube_f;
141-
fun eval2 (term:sube):int => (fix[sube,int] o_eval2[sube]) term;
141+
fun evals (term:sube):int => (fix[sube,int] o_evals[sube]) term;
142142
@
143143

144144
Here are the definitions from the standard library:
@@ -157,11 +157,11 @@ function fixpoint operator.
157157
Finally a test case:
158158

159159
@tangle openrec.flx
160-
var x2 : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
161-
var y2 = eval2 x2;
162-
var y3 = eval2 x; // ORGINAL DATA
163-
println$ y2;
164-
println$ y3;
160+
var xs : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
161+
var yss = evals xs;
162+
var ysa = evals xa; // ORGINAL DATA
163+
println$ "ys="+yss.str;
164+
println$ "ya="+ysa.str;
165165
@
166166

167167
It's very important to notice that the original data also works with
@@ -188,20 +188,20 @@ typedef o_mule[T] = (
188188
| o_adde[T]
189189
| `Mul of T * T
190190
);
191-
fun o_eval3[T] (eval: T -> int) (term: o_mule[T]):int =>
191+
fun o_evalm[T] (eval: T -> int) (term: o_mule[T]):int =>
192192
match term with
193193
| `Mul(a,b) => eval a * eval b
194-
| o_adde[T] :>> k => o_eval eval k
194+
| o_adde[T] :>> k => o_evala eval k
195195
endmatch
196196
;
197197
typefun o_mule_f (T:TYPE) : TYPE => o_mule[T];
198198
typedef mule = tfix<TYPE> o_mule_f;
199-
fun eval3 (term:mule):int => (fix[mule,int] o_eval3[mule]) term;
200-
var x3 : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
201-
var y4 = eval3 x3;
202-
var y5 = eval3 x; // ORGINAL DATA
203-
println$ y4;
204-
println$ y5;
199+
fun evalm (term:mule):int => (fix[mule,int] o_evalm[mule]) term;
200+
var xm : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
201+
var ymm = evalm xm;
202+
var yma = evalm xa; // ORGINAL DATA
203+
println$ "ym="+ymm.str;
204+
println$ "ya="+yma.str;
205205
@
206206

207207
@h2 Mixing it all together
@@ -213,17 +213,17 @@ typedef o_dive[T] = (
213213
| o_mule[T]
214214
| `Div of T * T
215215
);
216-
fun o_eval4[T] (eval: T -> int) (term: o_dive[T]):int =>
216+
fun o_evald[T] (eval: T -> int) (term: o_dive[T]):int =>
217217
match term with
218218
| `Div(a,b) => eval a / eval b
219-
| o_sube[T] :>> k => o_eval2 eval k
220-
| o_mule[T] :>> k => o_eval3 eval k
219+
| o_sube[T] :>> k => o_evals eval k
220+
| o_mule[T] :>> k => o_evalm eval k
221221
endmatch
222222
;
223223
typefun o_dive_f (T:TYPE) : TYPE => o_dive[T];
224224
typedef dive = tfix<TYPE> o_dive_f;
225-
fun eval4 (term:dive):int => (fix[dive,int] o_eval4[dive]) term;
226-
var x4 : dive =
225+
fun evald (term:dive):int => (fix[dive,int] o_evald[dive]) term;
226+
var xd : dive =
227227
`Add (
228228
`Mul (
229229
`Int 39,
@@ -236,14 +236,79 @@ var x4 : dive =
236236
`Int 66
237237
)
238238
;
239-
var y6 = eval4 x4;
240-
var y7 = eval4 x; // ORGINAL DATA
241-
var y8 = eval4 x2; // ORGINAL DATA
242-
var y9 = eval4 x3; // ORGINAL DATA
243-
println$ y6;
244-
println$ y7;
245-
println$ y8;
246-
println$ y9;
239+
var ydd = evald xd;
240+
var yda = evald xa; // ORGINAL DATA
241+
var yds = evald xs; // ORGINAL DATA
242+
var ydm = evald xm; // ORGINAL DATA
243+
println$ "yd="+ydd.str;
244+
println$ "ya="+yda.str;
245+
println$ "ys="+yds.str;
246+
println$ "ym="+ydm.str;
247247
@
248248

249+
@h1 Open/Closed Principle
250+
In "Object Oriented Software Construction" Bertran Meyer named a crucial
251+
system design principe the "Open/Closed Principle". It states that a system
252+
should have a unit of modularity which is simultaneously closed so it can
253+
be used and also open so it can be extended. This gave rise to the idea
254+
of classes which are closed object factories, but can be extended by
255+
inheritance.
256+
257+
The object oriented version of classes is a catastrophic failure bccause
258+
of severe restrictions imposed by type systems on the type of arguments of methods,
259+
which must be contravariant (or invariant), whereas usually we require covariance.
260+
261+
Open recursion solves this problem by providing types and function which are
262+
open to extension, and do not suffer fron the covariance problem because
263+
type variables are invariant.
264+
265+
The system then provides a closure operator, namely the fixpoint operator,
266+
which locks in covariant behaviour of a particular extension of the base type.
267+
The types as coproducts, which are covariant, and so base types are subtypes
268+
of extensions. This impplies the methods of an extension will continue to work
269+
with data of the base type.
270+
271+
@h2 Issues with polymorphic variants
272+
Polymorphic variants (as in Felix or Ocaml) are essential for open recursion
273+
to work. However as is the case with all structural types with user supplied
274+
componenmts, including records, compiler error diagnostics are very hard to
275+
understand due at least in part the fact that all the components must be listed
276+
to identify the type. By contrast, nominal types are easy to refer to, since
277+
they have a single unique and simple name.
278+
279+
Ocaml has made significant progress in this area by the diagnostics ability
280+
to search the symbol to table to see if a compnent set happens to have a named
281+
alias.
282+
283+
@h2 Multivariant Open Recursion
284+
In our simple example, the open version of a type has a single type variable,
285+
and the open version of a function has a functional parameter: the type variable
286+
and the paramater are eliminated by self-reference by using the fixpoint operators.
287+
288+
However in complex systems such as a compiler, we usually have main types,
289+
and auxilliay types they depend on; sometimes, we have two of more major
290+
types which are convoluted and inseparable: in these cases two or more
291+
type variables and function parameters may be required
292+
293+
This leads to a very difficult combinatorial explosion because now we
294+
can fixate one type variable whilst leaving the other open. Multiple extensions
295+
of one type can be used with multiple extensions of another.
296+
297+
In Felix, the type system terms in the compiler have at least 6 auxilliary types
298+
for which multiple flat extensions cold be provided leading to an unmanagably
299+
large potential set of closed terms. of course this is <em>not</em> a problem
300+
with open recursion at all: it is a simple fact, and a blessing that open recursion
301+
provides the machine to represent these choices. The existence of fixpoint combinators
302+
are then crucial because fixation closures are anonymous and can be provided as required
303+
"on the fly".
304+
305+
Nevertheless, using this technology in complex applications whilst the very environment
306+
where the modularity provided is of most benefit, is also the environment where
307+
it is hardest to get right. In the Felix compiler I found it so difficult,
308+
dynamic typing was prefered; that is, handling terms that should have been
309+
erased by throwing an exception was a lot easier than constructing a type
310+
for every use case so as to obtain a compile time error.
311+
312+
I think it remains to develop language constructions that can leverage
313+
this technology in a more manageable way.
249314

‎web/openrecursion.html

+102-40
Original file line numberDiff line numberDiff line change
@@ -310,7 +310,10 @@
310310
"Extension to subtraction",
311311
"Fixpoint operator.",
312312
"Extension to multiplication",
313-
"Mixing it all together"
313+
"Mixing it all together",
314+
"Open/Closed Principle",
315+
"Issues with polymorphic variants",
316+
"Multivariant Open Recursion"
314317
];
315318
function expand_all(dummy)
316319
{
@@ -377,7 +380,12 @@
377380
<div class=m2><a href="#Extension_to_multiplication_h">Extension to multiplication</a></div>
378381
<div class=m2><a href="#Mixing_it_all_together_h">Mixing it all together</a></div>
379382
</div>
380-
<script>counter_max=1;</script>
383+
<div class=m1 onclick="mshow('menu2','#Open/Closed Principle_h')"> <a href="#Open/Closed_Principle_h">Open/Closed Principle</a></div>
384+
<div class=sm id=menu2>
385+
<div class=m2><a href="#Issues_with_polymorphic_variants_h">Issues with polymorphic variants</a></div>
386+
<div class=m2><a href="#Multivariant_Open_Recursion_h">Multivariant Open Recursion</a></div>
387+
</div>
388+
<script>counter_max=2;</script>
381389
</div>
382390
<!--End Left Margin Toc-->
383391

@@ -429,10 +437,10 @@
429437
<span class="lineno" id=line3></span> `Add of adde * adde
430438
<span class="lineno" id=line4></span> );
431439
</pre></p><p>Notice, it is a recursive data type. The function we want is
432-
</p><p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> eval (term: adde) =&gt;
440+
</p><p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> evala (term: adde) =&gt;
433441
<span class="lineno" id=line2></span> <span class="small_keyword" title="match statement or expression">match</span> term <span class="small_keyword" title="type-class constraint">with</span>
434442
<span class="lineno" id=line3></span> | `Int j =&gt; j
435-
<span class="lineno" id=line4></span> | `Add (a,b) =&gt; eval a + eval b
443+
<span class="lineno" id=line4></span> | `Add (a,b) =&gt; evala a + evala b
436444
<span class="lineno" id=line5></span> <span class="small_keyword" title="end a match statement or expression">endmatch</span>
437445
<span class="lineno" id=line6></span> ;
438446
</pre></p><p>Again notice it is a recursive function. We are going to recode
@@ -449,7 +457,7 @@
449457
</p><p>And here's the open version of the function:
450458
</p><pre class='inclusion'>
451459
examples/openrecursion/openrec.flx</pre>
452-
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_eval[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_adde[T]) =&gt;
460+
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_evala[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_adde[T]) =&gt;
453461
<span class="lineno" id=line2></span> <span class="small_keyword" title="match statement or expression">match</span> term <span class="small_keyword" title="type-class constraint">with</span>
454462
<span class="lineno" id=line3></span> | `Int j =&gt; j
455463
<span class="lineno" id=line4></span> | `Add (a,b) =&gt; eval a + eval b
@@ -461,7 +469,7 @@
461469
</p><pre class='inclusion'>
462470
examples/openrecursion/openrec.flx</pre>
463471
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define an alias for a type expression">typedef</span> adde = o_adde[adde];
464-
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> eval (term:adde):<span class="library" title="binding of C int type">int</span> =&gt; o_eval[adde] eval term;
472+
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> evala (term:adde):<span class="library" title="binding of C int type">int</span> =&gt; o_evala[adde] evala term;
465473
</pre></p><p>What we have done is close the open data type by
466474
replacing the type variable with a self-reference.
467475
Similarly, we have closed the function, by replacing
@@ -471,9 +479,9 @@
471479
</p><p>Here is a test case:
472480
</p><pre class='inclusion'>
473481
examples/openrecursion/openrec.flx</pre>
474-
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a mutable variable">var</span> x : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
475-
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a mutable variable">var</span> y = eval x;
476-
<span class="lineno" id=line3></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y;
482+
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a mutable variable">var</span> xa : adde = `Add (`Add (`Int 39, `Int 2), `Int 1);
483+
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a mutable variable">var</span> yaa = evala xa;
484+
<span class="lineno" id=line3></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ya="</span>+yaa.<span class="library" title="Convert a value to a string">str</span>;
477485
</pre></p></div><h2 id='Extension_to_subtraction_h'><img src='/share/src/web/images/minus.gif' id='Extension to subtraction' onclick='toggle(this,"Extension_to_subtraction_d")' alt='+'/> 1.2 Extension to subtraction</h2><div id='Extension_to_subtraction_d' style='display:block'>
478486
<p>Now we're going to add a new feature: subtraction.
479487
</p><p>Here is the open version of the type and evaluator:
@@ -483,16 +491,16 @@
483491
<span class="lineno" id=line2></span> | o_adde[T]
484492
<span class="lineno" id=line3></span> | `Sub of T * T
485493
<span class="lineno" id=line4></span> );
486-
<span class="lineno" id=line5></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_eval2[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_sube[T]):<span class="library" title="binding of C int type">int</span> =&gt;
494+
<span class="lineno" id=line5></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_evals[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_sube[T]):<span class="library" title="binding of C int type">int</span> =&gt;
487495
<span class="lineno" id=line6></span> <span class="small_keyword" title="match statement or expression">match</span> term <span class="small_keyword" title="type-class constraint">with</span>
488496
<span class="lineno" id=line7></span> | `Sub (a,b) =&gt; eval a - eval b
489-
<span class="lineno" id=line8></span> | o_adde[T] :&gt;&gt; k =&gt; o_eval eval k
497+
<span class="lineno" id=line8></span> | o_adde[T] :&gt;&gt; k =&gt; o_evala eval k
490498
<span class="lineno" id=line9></span> <span class="small_keyword" title="end a match statement or expression">endmatch</span>
491499
<span class="lineno" id=line10></span> ;
492500
</pre></p><p>Notice both the type and function delegate to the existing code for addition
493501
and only add support for our new operation, subtraction.
494502
</p></div><h2 id='Fixpoint_operator._h'><img src='/share/src/web/images/minus.gif' id='Fixpoint operator.' onclick='toggle(this,"Fixpoint_operator._d")' alt='+'/> 1.3 Fixpoint operator.</h2><div id='Fixpoint_operator._d' style='display:block'>
495-
<p>The closure of the the open type and function ic called <em>fixating</em> them.
503+
<p>The closure of the the open type and function is called <em>fixating</em> them.
496504
What we have done is to manually introduce the self-reference.
497505
For the data type, we used a self-refering type alias; for the function
498506
we used eta-expansion.
@@ -503,7 +511,7 @@
503511
examples/openrecursion/openrec.flx</pre>
504512
<p><pre class='flxbg'><span class="lineno" id=line1></span> typefun o_sube_f (T:TYPE) : TYPE =&gt; o_sube[T];
505513
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define an alias for a type expression">typedef</span> sube = tfix&lt;TYPE&gt; o_sube_f;
506-
<span class="lineno" id=line3></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> eval2 (term:sube):<span class="library" title="binding of C int type">int</span> =&gt; (fix[sube,<span class="library" title="binding of C int type">int</span>] o_eval2[sube]) term;
514+
<span class="lineno" id=line3></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> evals (term:sube):<span class="library" title="binding of C int type">int</span> =&gt; (fix[sube,<span class="library" title="binding of C int type">int</span>] o_evals[sube]) term;
507515
</pre></p><p>Here are the definitions from the standard library:
508516
</p><p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> fix[D,C] (f:(D-&gt;C)-&gt;D-&gt;C) (x:D) : C =&gt; f (fix f) x;
509517
<span class="lineno" id=line2></span> typefun tfix&lt;K&gt; (f: K -&gt;K):K =&gt; f x as x:K;
@@ -516,11 +524,11 @@
516524
</p><p>Finally a test case:
517525
</p><pre class='inclusion'>
518526
examples/openrecursion/openrec.flx</pre>
519-
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a mutable variable">var</span> x2 : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
520-
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a mutable variable">var</span> y2 = eval2 x2;
521-
<span class="lineno" id=line3></span> <span class="big_keyword" title="Define a mutable variable">var</span> y3 = eval2 x; <span class="comment">// ORGINAL DATA</span>
522-
<span class="lineno" id=line4></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y2;
523-
<span class="lineno" id=line5></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y3;
527+
<p><pre class='flxbg'><span class="lineno" id=line1></span> <span class="big_keyword" title="Define a mutable variable">var</span> xs : sube = `Add (`Sub (`Int 39, `Int 2), `Int 1);
528+
<span class="lineno" id=line2></span> <span class="big_keyword" title="Define a mutable variable">var</span> yss = evals xs;
529+
<span class="lineno" id=line3></span> <span class="big_keyword" title="Define a mutable variable">var</span> ysa = evals xa; <span class="comment">// ORGINAL DATA</span>
530+
<span class="lineno" id=line4></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ys="</span>+yss.<span class="library" title="Convert a value to a string">str</span>;
531+
<span class="lineno" id=line5></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ya="</span>+ysa.<span class="library" title="Convert a value to a string">str</span>;
524532
</pre></p><p>It's very important to notice that the original data also works with
525533
the new function! Of course it's obvious why: the function <code>sube</code>
526534
delegates to <code>adde</code> in that case.
@@ -540,20 +548,20 @@
540548
<span class="lineno" id=line2></span> | o_adde[T]
541549
<span class="lineno" id=line3></span> | `Mul of T * T
542550
<span class="lineno" id=line4></span> );
543-
<span class="lineno" id=line5></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_eval3[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_mule[T]):<span class="library" title="binding of C int type">int</span> =&gt;
551+
<span class="lineno" id=line5></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_evalm[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_mule[T]):<span class="library" title="binding of C int type">int</span> =&gt;
544552
<span class="lineno" id=line6></span> <span class="small_keyword" title="match statement or expression">match</span> term <span class="small_keyword" title="type-class constraint">with</span>
545553
<span class="lineno" id=line7></span> | `Mul(a,b) =&gt; eval a * eval b
546-
<span class="lineno" id=line8></span> | o_adde[T] :&gt;&gt; k =&gt; o_eval eval k
554+
<span class="lineno" id=line8></span> | o_adde[T] :&gt;&gt; k =&gt; o_evala eval k
547555
<span class="lineno" id=line9></span> <span class="small_keyword" title="end a match statement or expression">endmatch</span>
548556
<span class="lineno" id=line10></span> ;
549557
<span class="lineno" id=line11></span> typefun o_mule_f (T:TYPE) : TYPE =&gt; o_mule[T];
550558
<span class="lineno" id=line12></span> <span class="big_keyword" title="Define an alias for a type expression">typedef</span> mule = tfix&lt;TYPE&gt; o_mule_f;
551-
<span class="lineno" id=line13></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> eval3 (term:mule):<span class="library" title="binding of C int type">int</span> =&gt; (fix[mule,<span class="library" title="binding of C int type">int</span>] o_eval3[mule]) term;
552-
<span class="lineno" id=line14></span> <span class="big_keyword" title="Define a mutable variable">var</span> x3 : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
553-
<span class="lineno" id=line15></span> <span class="big_keyword" title="Define a mutable variable">var</span> y4 = eval3 x3;
554-
<span class="lineno" id=line16></span> <span class="big_keyword" title="Define a mutable variable">var</span> y5 = eval3 x; <span class="comment">// ORGINAL DATA</span>
555-
<span class="lineno" id=line17></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y4;
556-
<span class="lineno" id=line18></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y5;
559+
<span class="lineno" id=line13></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> evalm (term:mule):<span class="library" title="binding of C int type">int</span> =&gt; (fix[mule,<span class="library" title="binding of C int type">int</span>] o_evalm[mule]) term;
560+
<span class="lineno" id=line14></span> <span class="big_keyword" title="Define a mutable variable">var</span> xm : mule = `Add (`Mul(`Int 39, `Int 2), `Int 1);
561+
<span class="lineno" id=line15></span> <span class="big_keyword" title="Define a mutable variable">var</span> ymm = evalm xm;
562+
<span class="lineno" id=line16></span> <span class="big_keyword" title="Define a mutable variable">var</span> yma = evalm xa; <span class="comment">// ORGINAL DATA</span>
563+
<span class="lineno" id=line17></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ym="</span>+ymm.<span class="library" title="Convert a value to a string">str</span>;
564+
<span class="lineno" id=line18></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ya="</span>+yma.<span class="library" title="Convert a value to a string">str</span>;
557565
</pre></p></div><h2 id='Mixing_it_all_together_h'><img src='/share/src/web/images/minus.gif' id='Mixing it all together' onclick='toggle(this,"Mixing_it_all_together_d")' alt='+'/> 1.5 Mixing it all together</h2><div id='Mixing_it_all_together_d' style='display:block'>
558566
<p>We're no going to mix it all together and also add division.
559567
</p><pre class='inclusion'>
@@ -563,17 +571,17 @@
563571
<span class="lineno" id=line3></span> | o_mule[T]
564572
<span class="lineno" id=line4></span> | `Div of T * T
565573
<span class="lineno" id=line5></span> );
566-
<span class="lineno" id=line6></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_eval4[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_dive[T]):<span class="library" title="binding of C int type">int</span> =&gt;
574+
<span class="lineno" id=line6></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> o_evald[T] (eval: T -&gt; <span class="library" title="binding of C int type">int</span>) (term: o_dive[T]):<span class="library" title="binding of C int type">int</span> =&gt;
567575
<span class="lineno" id=line7></span> <span class="small_keyword" title="match statement or expression">match</span> term <span class="small_keyword" title="type-class constraint">with</span>
568576
<span class="lineno" id=line8></span> | `Div(a,b) =&gt; eval a / eval b
569-
<span class="lineno" id=line9></span> | o_sube[T] :&gt;&gt; k =&gt; o_eval2 eval k
570-
<span class="lineno" id=line10></span> | o_mule[T] :&gt;&gt; k =&gt; o_eval3 eval k
577+
<span class="lineno" id=line9></span> | o_sube[T] :&gt;&gt; k =&gt; o_evals eval k
578+
<span class="lineno" id=line10></span> | o_mule[T] :&gt;&gt; k =&gt; o_evalm eval k
571579
<span class="lineno" id=line11></span> <span class="small_keyword" title="end a match statement or expression">endmatch</span>
572580
<span class="lineno" id=line12></span> ;
573581
<span class="lineno" id=line13></span> typefun o_dive_f (T:TYPE) : TYPE =&gt; o_dive[T];
574582
<span class="lineno" id=line14></span> <span class="big_keyword" title="Define an alias for a type expression">typedef</span> dive = tfix&lt;TYPE&gt; o_dive_f;
575-
<span class="lineno" id=line15></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> eval4 (term:dive):<span class="library" title="binding of C int type">int</span> =&gt; (fix[dive,<span class="library" title="binding of C int type">int</span>] o_eval4[dive]) term;
576-
<span class="lineno" id=line16></span> <span class="big_keyword" title="Define a mutable variable">var</span> x4 : dive =
583+
<span class="lineno" id=line15></span> <span class="big_keyword" title="Define a function with no side-effects">fun</span> evald (term:dive):<span class="library" title="binding of C int type">int</span> =&gt; (fix[dive,<span class="library" title="binding of C int type">int</span>] o_evald[dive]) term;
584+
<span class="lineno" id=line16></span> <span class="big_keyword" title="Define a mutable variable">var</span> xd : dive =
577585
<span class="lineno" id=line17></span> `Add (
578586
<span class="lineno" id=line18></span> `Mul (
579587
<span class="lineno" id=line19></span> `Int 39,
@@ -586,15 +594,69 @@
586594
<span class="lineno" id=line26></span> `Int 66
587595
<span class="lineno" id=line27></span> )
588596
<span class="lineno" id=line28></span> ;
589-
<span class="lineno" id=line29></span> <span class="big_keyword" title="Define a mutable variable">var</span> y6 = eval4 x4;
590-
<span class="lineno" id=line30></span> <span class="big_keyword" title="Define a mutable variable">var</span> y7 = eval4 x; <span class="comment">// ORGINAL DATA</span>
591-
<span class="lineno" id=line31></span> <span class="big_keyword" title="Define a mutable variable">var</span> y8 = eval4 x2; <span class="comment">// ORGINAL DATA</span>
592-
<span class="lineno" id=line32></span> <span class="big_keyword" title="Define a mutable variable">var</span> y9 = eval4 x3; <span class="comment">// ORGINAL DATA</span>
593-
<span class="lineno" id=line33></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y6;
594-
<span class="lineno" id=line34></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y7;
595-
<span class="lineno" id=line35></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y8;
596-
<span class="lineno" id=line36></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ y9;
597-
</pre></p></div></div><!--Main Content Body End-->
597+
<span class="lineno" id=line29></span> <span class="big_keyword" title="Define a mutable variable">var</span> ydd = evald xd;
598+
<span class="lineno" id=line30></span> <span class="big_keyword" title="Define a mutable variable">var</span> yda = evald xa; <span class="comment">// ORGINAL DATA</span>
599+
<span class="lineno" id=line31></span> <span class="big_keyword" title="Define a mutable variable">var</span> yds = evald xs; <span class="comment">// ORGINAL DATA</span>
600+
<span class="lineno" id=line32></span> <span class="big_keyword" title="Define a mutable variable">var</span> ydm = evald xm; <span class="comment">// ORGINAL DATA</span>
601+
<span class="lineno" id=line33></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"yd="</span>+ydd.<span class="library" title="Convert a value to a string">str</span>;
602+
<span class="lineno" id=line34></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ya="</span>+yda.<span class="library" title="Convert a value to a string">str</span>;
603+
<span class="lineno" id=line35></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ys="</span>+yds.<span class="library" title="Convert a value to a string">str</span>;
604+
<span class="lineno" id=line36></span> <span class="library" title="Print a string to standard output with newline appended">println</span>$ <span class="fstring">"ym="</span>+ydm.<span class="library" title="Convert a value to a string">str</span>;
605+
</pre></p></div></div><h1 id='Open/Closed_Principle_h'><img src='/share/src/web/images/minus.gif' id='Open/Closed Principle' onclick='toggle(this,"Open/Closed_Principle_d")' alt='+'/> 2 Open/Closed Principle</h1><div id='Open/Closed_Principle_d' style='display:block'>
606+
<p>In "Object Oriented Software Construction" Bertran Meyer named a crucial
607+
system design principe the "Open/Closed Principle". It states that a system
608+
should have a unit of modularity which is simultaneously closed so it can
609+
be used and also open so it can be extended. This gave rise to the idea
610+
of classes which are closed object factories, but can be extended by
611+
inheritance.
612+
</p><p>The object oriented version of classes is a catastrophic failure bccause
613+
of severe restrictions imposed by type systems on the type of arguments of methods,
614+
which must be contravariant (or invariant), whereas usually we require covariance.
615+
</p><p>Open recursion solves this problem by providing types and function which are
616+
open to extension, and do not suffer fron the covariance problem because
617+
type variables are invariant.
618+
</p><p>The system then provides a closure operator, namely the fixpoint operator,
619+
which locks in covariant behaviour of a particular extension of the base type.
620+
The types as coproducts, which are covariant, and so base types are subtypes
621+
of extensions. This impplies the methods of an extension will continue to work
622+
with data of the base type.
623+
</p><h2 id='Issues_with_polymorphic_variants_h'><img src='/share/src/web/images/minus.gif' id='Issues with polymorphic variants' onclick='toggle(this,"Issues_with_polymorphic_variants_d")' alt='+'/> 2.1 Issues with polymorphic variants</h2><div id='Issues_with_polymorphic_variants_d' style='display:block'>
624+
<p>Polymorphic variants (as in Felix or Ocaml) are essential for open recursion
625+
to work. However as is the case with all structural types with user supplied
626+
componenmts, including records, compiler error diagnostics are very hard to
627+
understand due at least in part the fact that all the components must be listed
628+
to identify the type. By contrast, nominal types are easy to refer to, since
629+
they have a single unique and simple name.
630+
</p><p>Ocaml has made significant progress in this area by the diagnostics ability
631+
to search the symbol to table to see if a compnent set happens to have a named
632+
alias.
633+
</p></div><h2 id='Multivariant_Open_Recursion_h'><img src='/share/src/web/images/minus.gif' id='Multivariant Open Recursion' onclick='toggle(this,"Multivariant_Open_Recursion_d")' alt='+'/> 2.2 Multivariant Open Recursion</h2><div id='Multivariant_Open_Recursion_d' style='display:block'>
634+
<p>In our simple example, the open version of a type has a single type variable,
635+
and the open version of a function has a functional parameter: the type variable
636+
and the paramater are eliminated by self-reference by using the fixpoint operators.
637+
</p><p>However in complex systems such as a compiler, we usually have main types,
638+
and auxilliay types they depend on; sometimes, we have two of more major
639+
types which are convoluted and inseparable: in these cases two or more
640+
type variables and function parameters may be required
641+
</p><p>This leads to a very difficult combinatorial explosion because now we
642+
can fixate one type variable whilst leaving the other open. Multiple extensions
643+
of one type can be used with multiple extensions of another.
644+
</p><p>In Felix, the type system terms in the compiler have at least 6 auxilliary types
645+
for which multiple flat extensions cold be provided leading to an unmanagably
646+
large potential set of closed terms. of course this is <em>not</em> a problem
647+
with open recursion at all: it is a simple fact, and a blessing that open recursion
648+
provides the machine to represent these choices. The existence of fixpoint combinators
649+
are then crucial because fixation closures are anonymous and can be provided as required
650+
"on the fly".
651+
</p><p>Nevertheless, using this technology in complex applications whilst the very environment
652+
where the modularity provided is of most benefit, is also the environment where
653+
it is hardest to get right. In the Felix compiler I found it so difficult,
654+
dynamic typing was prefered; that is, handling terms that should have been
655+
erased by throwing an exception was a lot easier than constructing a type
656+
for every use case so as to obtain a compile time error.
657+
</p><p>I think it remains to develop language constructions that can leverage
658+
this technology in a more manageable way.
659+
</p></div></div><!--Main Content Body End-->
598660

599661
</div> <!-- rightpanel contents end -->
600662
<hr>

0 commit comments

Comments
 (0)
Please sign in to comment.