Feature request: “shallow” version of compatible-closure-context

[lexi-lambda]

I would like a slight variant of compatible-closure-context that is “shallow” instead of recursive. This is best explained by example. Consider the following language:

(define-language L
  [e ::= x (λ x e) (e e)]
  [C ::= hole (λ x C) (C e) (e C)]
  [S ::= (λ x hole) (hole e) (e hole)]
  [x ::= variable-not-otherwise-mentioned])

Currently, the pattern (compatible-closure-context e) is equivalent to the pattern C. However, I would like Redex to be able to instead generate the pattern S. I don’t understand the terminology well enough to suggest a name for such a pattern, but it seems straightforward to implement, since it’s really just a small variant on compatible-closure-context.

[mfelleisen]

The notion of a compatible closure is a reasonably standard algebraic closure operation. The resulting set is closed under further application of the transformation function.

I don't quite see how this operation is a closure operation. A slightly different variant,

   F = (hole e) | (v hole)

[in your terms] is often used to deal with "stack frames" for the compatible closure relative to evaluation. But I don't think we need an operation to generate those.

[[ Now as for the actual S I am honestly not sure why one would ever want this. I have seen this once before, in an analysis of control operations relative to classical logic (by a Japanese author), and I thought it was a complete misunderstanding of op.sem. (The \x. hole and the symmetry in the application part are not relevant to computation except perhaps a very richly typed language.)

[lexi-lambda]

I don't quite see how this operation is a closure operation.

It isn’t (which is why I said I don’t really know what it should be named).

Now as for the actual S I am honestly not sure why one would ever want this.

A fair question! I actually do have a nonterminal like your F, which I do indeed use to represent “stack frames” (and actually it would be nice if Redex could generate E from F, but that’s a separate feature request), but the way I use S actually has nothing to do with evaluation. Rather, I use it to implement certain recursive metafunctions over my expressions.

For example, I have a free-vars metafunction defined like this:

(define-metafunction eff
  free-vars : e -> [x ...]
  [(free-vars x) [x]]
  [(free-vars (λv x e))
   ,(remq (term x) (term (free-vars e)))]
  [(free-vars (λ x e))
   ,(remq (term x) (term (free-vars e)))]
  [(free-vars (let [x e_1] e_2))
   ,(remove-duplicates (append (term (free-vars e_1))
                               (remq (term x) (term (free-vars e_2)))))]
  [(free-vars e)
   ,(let ([recur (term-match eff
                   [(in-hole S e) (term (free-vars e))])])
      (remove-duplicates (append* (recur (term e)))))])

I handle variables and binding forms specially, but the last case is a catch-all “recur everywhere” case implemented using S. This is useful for me primarily because my language has a lot of expression forms (38 at the time of this writing, to be exact), and listing them all out for every recursive metafunction like free-vars is tedious. Therefore, I use the S context to capture a kind of “recursion scheme” over the grammar of expressions.

[mfelleisen]

Oh you need to think bigger. Since you'd presumably annotate your grammar with Paul's amazing binding annotations, you should demand that in addition to substitute define-language also generates functions such as free-vars.

Now you may object that there are other homomorphisms you wish to formulate, not just free-vars because it is unreasonable to have to write out the 38 clauses by hand and it is equally unreasonable to obscure the algorithms with this (cool) trick you used (and I have used, too). It's not like FP hasn't dabbled in these kinds of auto-generated abstractions before (say polytypic programming or general folds and so on).

[[ Of course the ultimate objection to abstraction from mathematical oriented readers is that it hurts readability. I think this can be done properly. ]]

[lexi-lambda]

Since you'd presumably annotate your grammar with Paul's amazing binding annotations, you should demand that in addition to substitute define-language also generates functions such as free-vars.

That would certainly also be nice. :)

it is equally unreasonable to obscure the algorithms with this (cool) trick you used

It would definitely be neat to have a more fit for purpose solution to this problem, but that seems like a much bigger ask than what I’m asking for here, which doesn’t sound very hard to implement (and I was considering possibly opening a PR at some point to do so).

Of course the ultimate objection to abstraction from mathematical oriented readers is that it hurts readability.

I think that’s a fair criticism, but in this case I have no intention of actually typesetting these metafunctions—I’m just using Redex to explore some ideas on my own. It seems overly conservative to avoid adding any features to Redex that are difficult to read when typeset if they still provide value for other use cases.

[mfelleisen]

Imagine Racket before for/ and friends.
Imagine yourself asking for sum-of: All (X) [X -> Number] [Listof X] -> Number
;; - - -
Agreed, which is why I propose to raise your aim.