Performance-critical applications, including large-scale program analyses, graph analyses, and distributed system analyses, rely on fixed-point computations. The introduction of recursion using the WITH RECURSIVE keyword in SQL:1999 extended the ability of relational database systems to handle fixed-point computations, unlocking significant performance advantages by allowing computation to move closer to the data. Yet, with recursion, SQL becomes a Turing-complete programming language with new correctness and safety risks. Full SQL lacks a fixed semantics, as the SQL specification is written in natural language with ambiguities that database vendors resolve in divergent ways. As a result, reasoning about the correctness of recursive SQL programs must rely on isolated, composable properties of queries rather than wrestling a unified formal model out of a language with notoriously inconsistent implementations across systems. To address these challenges, we propose a calculus, λ_RQL, that derives properties from embedded recursive queries using the host-language type system and, depending on the database backend, rejects queries that may lead to the three classes of recursive query errors: runtime database exceptions, incorrect results, and nontermination. Queries that respect all properties are guaranteed to find the minimal fixed point in a finite number of steps. We introduce TyQL, a practical implementation in Scala for safe, recursive language-integrated query. TyQL uses modern type system features of Scala 3, namely Named-Tuples and type-level pattern matching, to ensure query portability and safety. TyQL shows no performance penalty compared to SQL queries expressed as embedded strings while enabling a three-order-of-magnitude speedup over non-recursive SQL.

Substructural type systems provide static guarantees about resource usage in programs. In most practical systems, however, the available usage constraints and their composition are predetermined by the language design, with only limited support for application programmers to customize them. We present a technique for expressing modular substructural constraints on function arrows in embedded domain-specific languages, enabling resource disciplines to be customized to the heterogeneous requirements of real-world domains. We formalize the design as an extension of the simply-typed lambda calculus and provide a Scala 3 implementation that uses type-level programming to enforce constraints at compile-time without host-compiler modifications. We illustrate the approach on a Linear Datalog case study, showing no performance overhead on practical programs.

Performance-critical industrial applications, including large-scale program, network, and distributed system analyses, are increasingly reliant on recursive queries for data analysis. Yet traditional relational algebra-based query optimization techniques do not scale well to recursive query processing due to the iterative nature of query evaluation, where relation cardinalities can change unpredictably during the course of a single query execution. To avoid error-prone cardinality estimation, adaptive query processing techniques use runtime information to inform query optimization, but these systems are not optimized for the specific needs of recursive query processing. In this paper, we introduce Adaptive Metaprogramming, an innovative technique that shifts recursive query optimization and code generation from compile-time to runtime using principled metaprogramming, enabling dynamic optimization and re-optimization before and after query execution has begun. We present a custom join-ordering optimization applicable at multiple stages during query compilation and execution. Through Carac, a custom Datalog engine, we evaluate the optimization potential of Adaptive Metaprogramming and show unoptimized recursive query execution time can be improved by three orders of magnitude and hand-optimized queries by 6x.