Breaking the Negative Cycle: Exploring the Design Space of Stratification for First-Class Datalog Constraints

TY - GEN

T1 - Breaking the Negative Cycle

T2 - 37th European Conference on Object-Oriented Programming, ECOOP 2023

AU - Starup, Jonathan Lindegaard

AU - Madsen, Magnus

AU - Lhoták, Ondřej

N1 - Publisher Copyright: © Jonathan Lindegaard Starup, Magnus Madsen, and Ondřej Lhoták;

PY - 2023/7

Y1 - 2023/7

N2 - The λDat calculus brings together the power of functional and declarative logic programming in one language. In λDat, Datalog constraints are first-class values that can be constructed, passed around as arguments, returned, composed with other constraints, and solved. A significant part of the expressive power of Datalog comes from the use of negation. Stratified negation is a particularly simple and practical form of negation accessible to ordinary programmers. Stratification requires that Datalog programs must not use recursion through negation. For a Datalog program, this requirement is straightforward to check, but for a λDat program, it is not so simple: A λDat program constructs, composes, and solves Datalog programs at runtime. Hence stratification cannot readily be determined at compile-time. In this paper, we explore the design space of stratification for λDat. We investigate strategies to ensure, at compile-time, that programs constructed at runtime are guaranteed to be stratified, and we argue that previous design choices in the Flix programming language have been suboptimal.

AB - The λDat calculus brings together the power of functional and declarative logic programming in one language. In λDat, Datalog constraints are first-class values that can be constructed, passed around as arguments, returned, composed with other constraints, and solved. A significant part of the expressive power of Datalog comes from the use of negation. Stratified negation is a particularly simple and practical form of negation accessible to ordinary programmers. Stratification requires that Datalog programs must not use recursion through negation. For a Datalog program, this requirement is straightforward to check, but for a λDat program, it is not so simple: A λDat program constructs, composes, and solves Datalog programs at runtime. Hence stratification cannot readily be determined at compile-time. In this paper, we explore the design space of stratification for λDat. We investigate strategies to ensure, at compile-time, that programs constructed at runtime are guaranteed to be stratified, and we argue that previous design choices in the Flix programming language have been suboptimal.

KW - Datalog

KW - first-class Datalog constraints

KW - negation

KW - row polymorphism

KW - stratified negation

KW - the Flix programming language

KW - type system

U2 - 10.4230/LIPIcs.ECOOP.2023.31

DO - 10.4230/LIPIcs.ECOOP.2023.31

M3 - Article in proceedings

AN - SCOPUS:85168901657

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 37th European Conference on Object-Oriented Programming, ECOOP 2023

A2 - Ali, Karim

A2 - Salvaneschi, Guido

PB - Dagstuhl Publishing

Y2 - 17 July 2023 through 21 July 2023

ER -