Constraint Handling Rules with Binders, Patterns and Generic Quantification

TL;DR

This paper enhances Constraint Handling Rules by integrating explicit binding structures using λ-tree syntax and introducing a new quantifier, enabling better handling of constraints with binding, such as higher-rank types.

Contribution

It introduces λ-tree syntax and a new ∇ quantifier to improve Constraint Handling Rules for constraints involving binding structures.

Findings

Enables explicit representation of binding in constraints.

Introduces a new ∇ quantifier for generating fresh constants.

Improves constraint solvers for higher-rank types.

Abstract

Constraint Handling Rules provide descriptions for constraint solvers. However, they fall short when those constraints specify some binding structure, like higher-rank types in a constraint-based type inference algorithm. In this paper, the term syntax of constraints is replaced by $\lambda$-tree syntax, in which binding is explicit; and a new $\nabla$ generic quantifier is introduced, which is used to create new fresh constants.