Logic Programming with Extensible Types

TL;DR

The paper presents a practical approach to embedding logic programming in a statically typed functional language by leveraging extensible types, a general unification mechanism, and a domain-specific language for predicates. It demonstrates how logic variables can inhabit host-language data structures while maintaining type safety, enabling polymorphic and higher-order logic programming within the host language (Haskell). Key contributions include a minimal set of primitives and combinators, existential quantification, a unification-based DSL, and a cut/negation framework that supports controlled backtracking. A compact implementation in Haskell illustrates the feasibility of the embedding, while situating the work relative to prior functional-logic languages and embeddings, and outlining multiple avenues for future enhancements and broader applicability.

Abstract

Logic programming languages present clear advantages in terms of declarativeness and conciseness. However, the ideas of logic programming have been met with resistance in other programming communities, and have not generally been adopted by other paradigms and languages. This paper proposes a novel way to incorporate logic programming in an existing codebase in a typed functional programming language. Our approach integrates with the host language without sacrificing static typing, and leverages strengths of typed functional programming such as polymorphism and higher-order. We do so by combining three ideas. First, we use the extensible types technique to allow values of the host language to contain logic variables. Second, we implement a unification algorithm that works for any data structure that supports certain operations.Third, we introduce a domain-specific language to define and query predicates. We demonstrate our proposal via a series of examples, and provide aids to make the notation convenient for users, showing that the proposed approach is not just technically possible but also practical. Our ideas have been implemented in the language Haskell with very good results.