Confusing behavior when a binding form is also an expression

[howell]

I was confused by some behavior when working on a test case for the issue I opened yesterday. I formulated a simple lambda-calculus language with pattern-matching on tuples (shown below). It is essentially the same as the lc-bind+patterns example in the docs, except I used tuple where lc-bind+patterns uses list and listp not understanding the importance of that distinction.

What I've inferred is that having a binding form (that is, something with a #:exports clause) that also looks like an expression is trouble. Identifiers that look like uses will be interpreted as bindings.

I don't think this behavior is itself an issue, but I could see it tripping up another person like me that tries to use the same syntax for both pattens and expressions. Pointing the behavior out in the documentation would have helped me; maybe a sentence like

"Variable uses and bindings must always be distinguished syntactically, which is why we use list and listp instead of just list."

or

"Redex determines whether an identifier is a binding or a use syntactically; as a consequence, if a form may contain both types of variables some form of distinguishing syntax must be used. Here, we use list and listp to mark that when an identifier appears in an expression (signified by list) it is a reference, while when it appears in a pattern (listp) it is a binding."

would do the trick?

#lang racket

(require redex)

(define-language LCP
  (M (M M) X (λ P M) (tuple M ...) b)
  (b number)
  (V (λ P M) b (tuple V ...))
  (X variable-not-otherwise-mentioned)
  (P X b (tuple P ...))
  (E hole (E M) (V E) (tuple V ... E M ...))
  (ρ ([X V] ...))
  (⊥ bot)
  #:binding-forms
  (tuple P ...) #:exports (shadow P ...)
  (λ P M #:refers-to P))

(define ->
  (reduction-relation
   LCP
   (==> ((λ P M) V)
        (subst-all ρ M)
        (where ρ (match P V)))
   with
   [(--> (in-hole E x) (in-hole E y))
    (==> x y)]))

(define-metafunction LCP
  match : P V -> ρ or ⊥
  [(match b b) ()]
  [(match X V) ([X V])]
  [(match (tuple P ..._1) (tuple V ..._1))
   ([X_bind V_bind] ... ...)
   (where (([X_bind V_bind] ...) ...) ((match P V) ...))]
  [(match P V) bot])

(define-metafunction LCP
  subst-all : ρ M -> M
  [(subst-all () M) M]
  [(subst-all ([X_0 V_0] [X_1 V_1] ...) M)
   (subst-all ([X_1 V_1] ...) (substitute M X_0 V_0))])

(define-term t
    (λ (tuple x 2)
      (tuple x x)))

(term (substitute t x hello) #:lang LCP)
;; => '(λ (tuple x«0» 2) (tuple x«1» x«2»))