Commit | Line | Data |
---|---|---|
7f918cf1 CE |
1 | Fold01N |
2 | ======= | |
3 | ||
4 | A common use pattern of <:Fold:> is to define a variable-arity | |
5 | function that combines multiple arguments together using a binary | |
6 | function. It is slightly tricky to do this directly using fold, | |
7 | because of the special treatment required for the case of zero or one | |
8 | argument. Here is a structure, `Fold01N`, that solves the problem | |
9 | once and for all, and eases the definition of such functions. | |
10 | ||
11 | [source,sml] | |
12 | ---- | |
13 | structure Fold01N = | |
14 | struct | |
15 | fun fold {finish, start, zero} = | |
16 | Fold.fold ((id, finish, fn () => zero, start), | |
17 | fn (finish, _, p, _) => finish (p ())) | |
18 | ||
19 | fun step0 {combine, input} = | |
20 | Fold.step0 (fn (_, finish, _, f) => | |
21 | (finish, | |
22 | finish, | |
23 | fn () => f input, | |
24 | fn x' => combine (f input, x'))) | |
25 | ||
26 | fun step1 {combine} z input = | |
27 | step0 {combine = combine, input = input} z | |
28 | end | |
29 | ---- | |
30 | ||
31 | If one has a value `zero`, and functions `start`, `c`, and `finish`, | |
32 | then one can define a variable-arity function `f` and stepper | |
33 | +`+ as follows. | |
34 | [source,sml] | |
35 | ---- | |
36 | val f = fn z => Fold01N.fold {finish = finish, start = start, zero = zero} z | |
37 | val ` = fn z => Fold01N.step1 {combine = c} z | |
38 | ---- | |
39 | ||
40 | One can then use the fold equation to prove the following equations. | |
41 | [source,sml] | |
42 | ---- | |
43 | f $ = zero | |
44 | f `a1 $ = finish (start a1) | |
45 | f `a1 `a2 $ = finish (c (start a1, a2)) | |
46 | f `a1 `a2 `a3 $ = finish (c (c (start a1, a2), a3)) | |
47 | ... | |
48 | ---- | |
49 | ||
50 | For an example of `Fold01N`, see <:VariableArityPolymorphism:>. | |
51 | ||
52 | ||
53 | == Typing Fold01N == | |
54 | ||
55 | Here is the signature for `Fold01N`. We use a trick to avoid having | |
56 | to duplicate the definition of some rather complex types in both the | |
57 | signature and the structure. We first define the types in a | |
58 | structure. Then, we define them via type re-definitions in the | |
59 | signature, and via `open` in the full structure. | |
60 | [source,sml] | |
61 | ---- | |
62 | structure Fold01N = | |
63 | struct | |
64 | type ('input, 'accum1, 'accum2, 'answer, 'zero, | |
65 | 'a, 'b, 'c, 'd, 'e) t = | |
66 | (('zero -> 'zero) | |
67 | * ('accum2 -> 'answer) | |
68 | * (unit -> 'zero) | |
69 | * ('input -> 'accum1), | |
70 | ('a -> 'b) * 'c * (unit -> 'a) * 'd, | |
71 | 'b, | |
72 | 'e) Fold.t | |
73 | ||
74 | type ('input1, 'accum1, 'input2, 'accum2, | |
75 | 'a, 'b, 'c, 'd, 'e, 'f) step0 = | |
76 | ('a * 'b * 'c * ('input1 -> 'accum1), | |
77 | 'b * 'b * (unit -> 'accum1) * ('input2 -> 'accum2), | |
78 | 'd, 'e, 'f) Fold.step0 | |
79 | ||
80 | type ('accum1, 'input, 'accum2, | |
81 | 'a, 'b, 'c, 'd, 'e, 'f, 'g) step1 = | |
82 | ('a, | |
83 | 'b * 'c * 'd * ('a -> 'accum1), | |
84 | 'c * 'c * (unit -> 'accum1) * ('input -> 'accum2), | |
85 | 'e, 'f, 'g) Fold.step1 | |
86 | end | |
87 | ||
88 | signature FOLD_01N = | |
89 | sig | |
90 | type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) t = | |
91 | ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) Fold01N.t | |
92 | type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) step0 = | |
93 | ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) Fold01N.step0 | |
94 | type ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) step1 = | |
95 | ('a, 'b, 'c, 'd, 'e, 'f, 'g, 'h, 'i, 'j) Fold01N.step1 | |
96 | ||
97 | val fold: | |
98 | {finish: 'accum2 -> 'answer, | |
99 | start: 'input -> 'accum1, | |
100 | zero: 'zero} | |
101 | -> ('input, 'accum1, 'accum2, 'answer, 'zero, | |
102 | 'a, 'b, 'c, 'd, 'e) t | |
103 | ||
104 | val step0: | |
105 | {combine: 'accum1 * 'input2 -> 'accum2, | |
106 | input: 'input1} | |
107 | -> ('input1, 'accum1, 'input2, 'accum2, | |
108 | 'a, 'b, 'c, 'd, 'e, 'f) step0 | |
109 | ||
110 | val step1: | |
111 | {combine: 'accum1 * 'input -> 'accum2} | |
112 | -> ('accum1, 'input, 'accum2, | |
113 | 'a, 'b, 'c, 'd, 'e, 'f, 'g) step1 | |
114 | end | |
115 | ||
116 | structure Fold01N: FOLD_01N = | |
117 | struct | |
118 | open Fold01N | |
119 | ||
120 | fun fold {finish, start, zero} = | |
121 | Fold.fold ((id, finish, fn () => zero, start), | |
122 | fn (finish, _, p, _) => finish (p ())) | |
123 | ||
124 | fun step0 {combine, input} = | |
125 | Fold.step0 (fn (_, finish, _, f) => | |
126 | (finish, | |
127 | finish, | |
128 | fn () => f input, | |
129 | fn x' => combine (f input, x'))) | |
130 | ||
131 | fun step1 {combine} z input = | |
132 | step0 {combine = combine, input = input} z | |
133 | end | |
134 | ---- |