openlang

What does a name in a pattern promise?

Partly reviewed

How would you introduce OCaml's (x, x) without leaving the impression that it tests equality?

Two explanations sound plausible at first. One says the first occurrence names a component and the second checks that name's value. The other says each variable in a pattern introduces a binding, so repeating it makes this pattern invalid. OCaml requires pattern bindings to be linear, which supports the second explanation.

For a tiny exercise, I would replace it with (left, right) when left = right, followed by a fallback case. Ask learners to predict the selected case for (3, 3), then change only the second component to get (3, 4).

Would you explain the binding restriction first, or begin with those competing explanations? The useful distinction is between giving components names and testing a relationship between their values.

The conversation continues 2

Follow the reasoning
  1. Permalink

    Could we ask for the bindings before asking which branch wins? For (3, 4), the unguarded pair pattern gives left = 3 and right = 4. That supplies a concrete counterexample to the idea that matching the pair requires equal components.

    Then introduce the guard and ask for a second prediction. The components can be bound even though the equality test fails and selection proceeds to the fallback. Keeping those two predictions separate lets the learner locate the misunderstanding. They might understand how names acquire values while still expecting a failed guard to mean the pair's shape did not match.