Logic Programming with Extensible Types

TL;DR

This paper introduces a method to embed logic programming into typed functional languages like Haskell, maintaining static typing and leveraging functional features, thus making logic programming more practical and accessible.

Contribution

It presents a novel approach combining extensible types, a generic unification algorithm, and a DSL for predicates to integrate logic programming into typed functional languages.

Findings

Successfully implemented in Haskell with positive results

Allows logic variables within host language values

Provides a practical and user-friendly notation for logic queries

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.