Constraint handling rules with binders, patterns and generic quantification

DOI10.1017/S1471068417000230MaRDI QIDQ4592722zbMATH OpenOpenAlexFDO

Authors Alejandro Serrano, Jurriaan Hage

Publication date 8 November 2017

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1707.02754

zbMATH Keywords

constraint handling rulesgeneric quantificationpattern unification

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Grammars and rewriting systems (68Q42) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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 $abla$ generic quantifier is introduced, which is used to create new fresh constants.

Recommendations

• Haskell type constraints unleashed
• Principles of constraint systems and constraint solvers
• Type inference using constraint handling rules
• scientific article; zbMATH DE number 873325
• scientific article; zbMATH DE number 2086602

Cites work

• \textsc{OutsideIn(X)}: modular type inference with local assumptions
• A Framework for Extended Algebraic Data Types
• A logic for reasoning about generic judgments
• A logic programming language with lambda-abstraction, function variables, and simple unification
• A proof theory for generic judgments
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Abella: a system for reasoning about relational specifications
• As time goes by: constraint handling rules
• Complete and easy bidirectional typechecking for higher-rank polymorphism
• Constraint Handling Rules
• FreshML: programming with binders made simple
• scientific article; zbMATH DE number 1696799 (Why is no real title available?)
• scientific article; zbMATH DE number 1158760 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Linear unification of higher-order patterns
• Logic Programming
• Observable Confluence for Constraint Handling Rules
• Practical type inference for arbitrary-rank types
• Programming languages and systems. 4th Asian symposium, APLAS 2006, Sydney, Australia, November 8--10, 2006. Proceedings
• Termination Analysis of CHR Revisited
• The locally nameless representation
• Theory and practice of constraint handling rules
• Understanding functional dependencies via constraint handling rules
• Visible type application

Describes a project that uses

Uses Software

• Abella

This page was built for publication: Constraint handling rules with binders, patterns and generic quantification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4592722)