Modular Substructural Constraints for Embedded DSLs

Abstract

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.