Redex- fixing incompatible ellipsis match counts for template

Questions & Answers
1

Here's a small redex example that I would like to work:

#lang racket

(require redex)

(define-language L
  [numbers (number ...)]
  [pairs ((number number) ...)])

(define-judgment-form
  L
  #:contract (make-pairs numbers numbers pairs)
  #:mode (make-pairs I I O)
  [(side-condition
    (equal? (length (term (number_i ...)))
            (length (term (number_j ...)))))
   ------------------------
   (make-pairs (number_i ...) (number_j ...) ((number_i number_j) ...))])

(judgment-holds
  (make-pairs (1) (2 3) pairs)
  pairs)

When make-pairs is given two lists of different lengths, I would like the judgment to fail.
However, instead we get an error syntax: incompatible ellipsis match counts for template.

I think it has to do with redex's order of evaluation- the side condition isn't preventing the instantiation of the template. Is there a way to fix this?

2

You have to name the ellipsis to make that work. A named ellipsis matches other ones when their lengths are the same. Like this:

#lang racket
(require redex/reduction-semantics)

(define-language L
  [numbers (number ...)]
  [pairs ((number number) ...)])

(define-judgment-form
  L
  #:contract (make-pairs numbers numbers pairs)
  #:mode (make-pairs I I O)
  [------------------------
   (make-pairs (number_i ..._1) (number_j ..._1) ((number_i number_j) ...))])

(judgment-holds
  (make-pairs (1) (2 3) pairs)
  pairs)

(judgment-holds
  (make-pairs (1 2) (3 4) pairs)
  pairs)

Stepping back, I spent a lot of time using ellipses in complex and fancy ways and, in the end, I'm not sure it was time well spent as you end up using things that your average PL reader doesn't already know (although your average Racketeer and Schemer do...!). So it may make sense to start with definitions like this:

(define-language L
  [numbers · (number numbers)]
  [pairs · ((number number) pairs)])

depending on what you want to do. Of course, this means there's a lot of Redex fanciness you cannot use but if you're trying to communicate with others via your Redex model, this may be best.

Of course, if you're instead using Redex to prototype and help you validate your own ideas and the communication aspect isn't as important, then knock yourself out with the ellipses! They're pretty fun. :slight_smile:

3

Interesting, that does work for me. I do feel it might be less confusing for readers if I use a side condition and typeset it nicely. Is there a reason we get that error even with the side-condition? Should redex delay that check until after side conditions?

Hmm, it's true ellipses can get hairy. I've found them to be quite nice most of the time.

4

This is a good point. Looking at the expansion, it seems to be turning into something like this:

(term-let ([(any_1 ...) (list 1 2 3)]
           [(any_2 ...) (list 4 5)])
          (and #f
               (term ((any_1 any_2) ...))))

which does not signal an error. So I'm missing something or there's a bug somewhere.

5

Oh, duh. side-condition in define-reduction-relation is not an automatically-unquoted position! (It is designed for metafunctions that returns booleans and it works that way because of the extra support that define-metafunction has for random generation that doesn't work with arbitrary racket code.)

Classic gotcha.

6

Oops, I've done that several times already! Thanks

7

This brings me to another burning question I've had-
Why is side-condition a racket expression for reduction relations? I've been resorting to (where #t some-metafunction)

8

An accident of history, I suppose. Redex has actually come very far from its original design; if you look at the code fragments in the RTA 2004 paper ( "A Visual Environment for Developing Context-Sensitive Term Rewriting Systems"), you'll find them completely unrecognizable.

9

Makes sense. Out of the three forms I like define-judgment the best, it's pretty useful and composes better.

Would it be possible to add a side-condition that is a term to reduction relations? I could also hack up a way to typeset my (where #t) hack by using where/hidden

10

I think that adding a few special cases to the typesettting for things like (where #t ...) or (side-condition (term ...)) make sense and maybe one of those is even in there already.