Compiling Pattern Matching to good Decision Trees
📜 Abstract
We address the issue of compiling ML pattern matching to efficient decisions trees. Traditionally, compilation to decision trees is optimized by (1) implementing decision trees as dags with maximal sharing; (2) guiding a simple compiler with heuristics. We first design new heuristics that are inspired by necessity, a notion from lazy pattern matching that we rephrase in terms of decision tree semantics. Thereby, we simplify previous semantical frameworks and demonstrate a direct connection between necessity and decision tree runtime efficiency. We complete our study by experiments, showing that optimized compilation to decision trees is competitive. We also suggest some heuristics precisely.
✨ Summary
Summary
The paper studies compilation of ML pattern matching into decision trees, emphasizing the choice of which subject-value subterm to test at each step. It formalizes necessity in terms of decision-tree paths and uses this concept to derive new column-selection heuristics: needed columns, needed prefixes, and constructor prefixes. The compilation scheme is shown to preserve ML’s first-match semantics regardless of column choices.
The experiments evaluate 54 pattern-matching expressions extracted from OCaml, Coq, Why, and CIL-related software. They report that maximal sharing is important for code size, while necessity-based heuristics—especially p, q, and n—generally improve path length. The combined heuristic pba is identified as the best overall experimental choice, while qba is recommended when usefulness analysis is to be avoided. The authors also integrate decision-tree compilation into OCaml and report measurable speed differences for a pattern-matching-intensive PCF interpreter.
Subsequent use of the paper’s ideas is directly documented in several places. OCaml compiler documentation identifies the work as relevant background for its pattern-matching compilation pipeline. (ocamlverse.net) The Runtime Verification LLVM backend states that its pattern-matching algorithm is heavily based on Maranget’s paper and adapts its pattern matrices, specialization, default decomposition, decision trees, and heuristics. (github.com) An independent OCaml implementation also explicitly describes itself as implementing the paper’s algorithm, using DAG construction and hash-consing to avoid duplicated decision subtrees. (github.com) Bibliographic records confirm its publication in ML 2008 and its continued citation in later technical literature. (dblp.org)