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 -