Odd in-hole behaviour.

[mamysa]

I have the following language (which doesn't make any sense as I am deliberately trying to break things)

(define-language HoleTest
  (n  ::= number)
  (e ::= (+ e e) n)
  (x ::= variable-not-otherwise-mentioned)
  (P ::= (+ E E))
  (E ::= (E hole) hole))

Now, doing the following

(redex-match HoleTest (in-hole P x) (term 3))

raises in-hole first argument is expected to match exactly one hole error because in P we can have (+ hole hole), for example.

However, by putting P into the sequence and doing the following

(redex-match HoleTest (in-hole (P) x) (term 3))

does not seem to raise any errors and returns #f instead despite that P can still match multiple holes. Is it intended behaviour, and, if so, why is it the case?

[rfindler]

Thanks for the issue!

It looks like a bug to me. And possibly the fix as issue #225.

Robby

On Sat, Jun 13, 2020 at 7:28 AM mamysa notifications@github.com wrote:

I have the following language (which doesn't make any sense as I am deliberately trying to break things)

(define-language HoleTest (n ::= number) (e ::= (+ e e) n) (x ::= variable-not-otherwise-mentioned) (P ::= (+ E E)) (E ::= (E hole) hole))

Now, doing the following

(redex-match HoleTest (in-hole P x) (term 3))

raises in-hole first argument is expected to match exactly one hole error because in P we can have (+ hole hole), for example.

However, by putting P into the sequence and doing the following

(redex-match HoleTest (in-hole (P) x) (term 3))

does not seem to raise any errors and returns #f instead despite that P can still match multiple holes. Is it intended behaviour, and, if so, why is it the case?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/226, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNMFX6YAQOHTI7QRFQGTRWNWGDANCNFSM4N47AB7A .

[mfelleisen]

(Speaking as a a redex semanticist a production such as P ::= (+ E E) rarely makes sense. Even for parallelism we probably want single-hole contexts. ~~ This has nothing to do with the bug. I have been fighting redex static checking too.)

[rfindler]

It may be that we want to move the static check from the use of in-hole to the mere construction of the pattern itself. I was worried that that would be too agressive, I think, but maybe I was being too conservative.

Certainly internally it is tracking the right information to do that, it just waits before signaling the error, allowing someone to use the matcher on such patterns against terms that have holes in them (but disallowing décompositions).

Robby

On Sat, Jun 13, 2020 at 8:15 AM Matthias Felleisen notifications@github.com wrote:

(Speaking as a a redex semanticist a production such as P ::= (+ E E) rarely makes sense. Even for parallelism we probably want single-hole contexts. ~~ This has nothing to do with the bug. I have been fighting redex static checking too.)

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/racket/redex/issues/226#issuecomment-643622350, or unsubscribe https://github.com/notifications/unsubscribe-auth/AADBNMETQ6AI44FHZHNCT5TRWN3W3ANCNFSM4N47AB7A .

[mfelleisen]

!! I think if the aggressive approach accepts our examples and the book, it's worth a try.

[rfindler]

I'm not sure I'm understanding your comment, @mfelleisen

!! I think if the aggressive approach accepts our examples and the book, it's worth a try.

FWIW (and you probably could guess this but just in case), the basic idea of how the check is done is to calculate, for each non-terminal, whether it always produces 0 holes, always produces 1 hole, or might do something else (with a fixed-point computation that happens as a language is built). Then that information is stored and used to check any pattern that appears in the first argument to in-hole. This information could also be used to rule out any non-terminal that doesn't either have exactly 0 or exactly 1 hole all the time, perhaps by complaining about two productions that don't match or because of ellipses or ... various other reasons that one can imagine. (The question of how to report the error is orthogonal, as the source locations and the reason for mismatch can be saved and reported at any time.)

If we wanted to do the aggressive thing and just disallow any pattern/non-terminal that isn't always 0- or always 1-hole producing, we'd want to audit a lot of redex code to be sure we're not breaking too many things. I think the book would be a good thing to audit, but there is more that we'd want to audit. (Unfortunately, the book isn't very ryr so it will not be easy to audit.) Checking the ryr popl paper isn't hard, tho, as that's in the test suites. Of course, we would hope that the examples here and in #225 are ruled out (but perhaps that's what your comment means?).

Since the question of when to enforce is fairly simple from the redex perspective and the information being built is currently wrong, perhaps we should split these two concerns, tho.

[mfelleisen]

@frindler

Yes, I figured out both points: how/what you’d check (I recently scanned the code) and what kind of code we’d have to audit. My gut feeling is that we’d find very little code would fail, actually I am pretty sure none.

The other point to consider is whether we’d want multi-hole contexts at some point in the future. I have found reasons in proofs to use them. I have considered modeling parallelism with this device but I never thought it was really the right tool (though I have recently begun to re-think this point).