Is it good style to use `#:when` instead of `?` in match expression?

Questions & Answers
1

Hi everyone, this question originally came to me while working with Typed Racket. The current Typed Racket seems not to support match very well, so in many cases, ? cannot be used to mark type through predicate. For example, the following code will not work:

#lang typed/racket

(match '[-> Number Number Number]
  [`[-> ,(? symbol? #{ts : (Listof Symbol)}) ... ,(? symbol? t1)]
   (displayln ts)
   (displayln t1)])

And we can use #:when to get the same behavior:

#lang typed/racket

(: listof? (All (A) [-> (pred A) (pred (Listof A))]))
(define listof?
  (λ (pred)
    (λ (arg)
      (and (list? arg)
           (andmap pred arg)))))

(match '[-> Number Number Number]
  [`[-> ,ts ... ,t1]
   #:when (and ((listof? symbol?) ts)
               (symbol? t1))
   (displayln ts)
   (displayln t1)])

And this code looks much clearer than the previous one. So I wonder whether using #:when will reduce the performance of match? If not, should we try to use #:when instead of ? and let Racket support listof? directly to improve code readability (even in untyped version)?

2

Put typed/racket aside. In your examples, it is more of a personal taste. In general, ? allows you put your patterns together

[(? some-predicate-list? (list-rest a d)) (do-something-with a d)]

a #:when version would not look as concise as the code above.

On the other hand, #:when allows you to do conditions on multiple pattern variables from different patterns:

[(list a-pat b-pat c-pat ...) #:when (test a-from-pat b-from-pat c-from-c-pat) .....]

a ? version would look less intuitive in this case.

3

Oh, but wait... let's bring Typed Racket back into the picture!

It turns out that this #:when style preserves information that would be otherwise lost by TR. Specifically, consider the following program:

#lang typed/racket

(define n1s : (Listof Number)
  (match '(a 3 9 d)
    [(list 'a (? number? ns) ... 'd) ns]))

(define n2s : (Listof Number)
  (match '(a 3 9 d)
    [(list 'a ns ... 'd)
     #:when (andmap number? ns)
     ns]))

The first one does not type-check, the second one does.

4

The second way, with #:when, does two traversals of the list, so it can be slower. The ? pattern shown by @capfredf will also do two traversals, but one can be fast if list? is fast.

In general Typed Racket finds it hard to see through the loop generated by ... in match, unless the ... is the end of the list. For example, if you omit the t1 binding then your example typechecks, and similarly for @jbclements' example given an appropriate type annotation.

5

Thanks for your answers! I rarely wrote very complex pats in the past, so I overlooked a lot of ? applies, thanks @capfredf for the example!

Maybe this problem finally has to go back to Typed Racket, because using match in TR, we generally need to use predicate to check the types of pattern variables, so what I want to ask is what @capfredf said about the second case: is it more appropriate to use #:when than ? if I want to match pattern variables.

Judging from @samth's answer, in the #:when case, val-expr needs to be matched by pat first, and then checked by #:when, so that match does a repeat operation.

For me in general it may be rare to match very large data, so I think the cost of using #:when is acceptable to me.

Thanks for all your help!