Fixpoints for the masses: programming with first-class Datalog constraints

Magnus Madsen, Ondrej Lhoták

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

Abstract

Datalog is a declarative logic programming language that has been used in a variety of applications, including big-data analytics, language processing, networking and distributed systems, and program analysis. In this paper, we propose first-class Datalog constraints as a mechanism to construct, compose, and solve Datalog programs at run time. The benefits are twofold: We gain the full power of a functional programming language to operate on Datalog constraints-as-values, while simultaneously we can use Datalog where it really shines: to declaratively express and solve fixpoint problems. We present an extension of the lambda calculus with first-class Datalog constraints, including its semantics and a type system with row polymorphism based on Hindley-Milner. We prove soundness of the type system and implement it as an extension of the Flix programming language.

Original languageEnglish
Title of host publicationProceedings of the ACM on Programming Languages
Number of pages28
Volume4
PublisherAssociation for Computing Machinery
Publication date13 Nov 2020
EditionOOPSLA
DOIs
Publication statusPublished - 13 Nov 2020
SeriesACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages and Applications

Keywords

  • first-class datalog
  • functional programming
  • logic programming

Fingerprint

Dive into the research topics of 'Fixpoints for the masses: programming with first-class Datalog constraints'. Together they form a unique fingerprint.

Cite this