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 λ-tree syntax, in which binding is explicit; and a new ∇ generic quantifier is introduced, which is used to create new fresh constants.
|Number of pages||18|
|Journal||Theory and Practice of Logic Programming|
|Early online date||22 Aug 2017|
|Publication status||Published - Sept 2017|
- Constraint Handling Rules
- pattern unification
- generic quantification