Pattern matching deconstructs a value according to the constructor that created it and binds names to its components.

For a sum type $A+B$, a match must distinguish the two alternatives:

match value:
    inl(a) -> handle_a(a)
    inr(b) -> handle_b(b)

For a product, a pattern can expose both fields at once:

(x, y) -> x + y

Patterns can be nested, so the structure of the program follows the structure of the data.

A match is exhaustive when every possible constructor is covered. If a Boolean-like type has constructors True and False, handling only True leaves an input for which evaluation has no matching branch. A type checker can detect this statically when the constructors are known.

Patterns may also overlap. Languages commonly define either an ordered first-match rule or reject ambiguous forms in contexts where ordering would hide mistakes.

Pattern matching is the elimination mechanism naturally paired with algebraic data constructors: constructors build values; patterns reveal which constructor was used and make its components available. Exhaustiveness checking turns the closed set of alternatives in a sum type into a practical safety guarantee.