doc/guide/src/Fold01N.adoc

   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 +&grave;+ 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 ----