The Lam_Dat calculus brings together the power of functional and declarative logic programming in one language. In the Lam_Dat calculus, 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 imposes the simple requirement that Datalog programs must not use recursion through negation.

For a Datalog program, this requirement is straightforward to check, but for a Lam_Dat calculus program, it is not so simple: A Lam_Dat calculus 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 Lam_Dat calculus. 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.