Pattern-driven Reduction in Haskell

Haskell is a functional programming language with nominally non-strict semantics, implying that evaluation of a Haskell expression proceeds by demand-driven reduc-tion. However, Haskell also provides pattern matching on arguments of functions, in let expressions and in the match clauses of case expressions. Pattern-matching requires data-driven reduction to the extent necessary to evaluate a pattern match or to bind variables introduced in a pattern. In this paper we provide both an ab-stract semantics and a logical characterization of pattern-matching in Haskell and the reduction order that it entails.