(I’ve set the fix version to the module system and separate compilation release, since this issue has something to do with separate compilation, composition, and modularity)

Let me introduce this proposal by a small example. Suppose that you
want to implement an extensible interpreter. This interpreter accepts
a higher order strategy argument for evaluating extensions.

The strategy argument of the extension parameter is the strategy to invoke recursively for evaluation.

---

eval(EvalExtension: (t -> t) * t -> t) =
rec rec(
EvalExtension(rec)
<+ Eval(rec)
)

Eval(rec) :
Plus(e1, e2) -> (e1’, e2’)
where
e1 => e1’
; e2 => e2’
———————————————

(Please ignore the ugliness of the recursive calls in the rules for
this example)

An example of an extension:
———————————————
EvalTimesExtension(rec) :
Mul(e1, e2) -> (e1’, e2’)
where
e1 => e1’
; e2 => e2’
———————————————

Now, suppose that we have no extension. In this case,
EvalExtension(rec) should fail. You would like to specify this as:

---

eval(fail)
———————————————

But, fail is not a higher order strategy, so this is not correct (but
unfortunately only the C compiler will complain, see STR-97).

The correct solution is:
———————————————
let no-extension(s) = fail
in eval(no-extension)
end
———————————————

So, my first proposal is that ‘fail’ and ‘id’ should be first-order
and arbitrary higher-order strategies.

But, that’s not enough. Suppose that we have two extensions,
implemented in two strategies:

---

extension1(rec) = …
extension2(rec) = …
———————————————

You would like to invoke eval as:
———————————————
eval(extension1 + extension2)
———————————————

But, of course this does not work, since + cannot compose higher order
strategies: it can only compose first-order ‘t -> t’ strategies. So,
the solution is:

---

let extensions(s) = extension1(s) + extension2(s)
in eval(extensions)
end
———————————————

Which is a bit awkward.

A different solution is to use the same names:
———————————————
extension(rec) = …
extension(rec) = …
———————————————

These definitions can be composed by the compiler. But, sometimes you
don’t want to give the rules the same name and it is also a problem
with separate compilation.

So, basically my proposal is that all strategy combinators of Stratego
should also be combinators for higher order strategies. Similar to the
proposal for fail and id, strategy combinators should be able to
compose arbitrary higher order as well first-order strategy argyments
(of course the types of the arguments have to match).

Higher order strategies have always felt a bit complicated to me in
Stratego, leading to proposals such as STR-75 (lambda
abstractions). Maybe the reason for this is that we like to compose
strategies and know how to do that. However, higher order strategies
cannot be composed in the same way as simple strategies.

Of course, this is currently not trivial to implement, since we need a
better type checker for the current type system of Stratego. Also,
there are some open questions, such as what to do if a first-order and
higher-order variant exists of some strategy. This can probably be
solved by using target typing (considering the formal parameter or lhs
of a strategy definition).

Submitted on 27 August 2005 at 18:05