Searcharxiv⌕ Search
Home/Archive/arXiv

arXiv · 2610.23023

Arbitrary Functors as Modalities in a Linear Calculus

Jean-Philippe Bernardy·Andreas Abel
View original source ↗Read source document ↗Export metadata ↓

Abstract

We study modalities in the linear lambda calculus, by interpreting them as endofunctors in monoidal closed categories. We support functors that do not distribute over products, including (co)monads. We also support arbitrary natural transformations as conversion between modalities. We provide a generic categorical semantics, which we then specialise to a sound and complete resource semantics. We use this resource semantics to derive normalisation by evaluation. Along the way, we describe several applications of such models. This work aims at providing a foundation for future programming languages with modalities. The paper is backed by a mechanisation in Agda.

Explore related subjects

cs.PL

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Jean-Philippe Bernardy, Andreas Abel. 2026-10-16. Arbitrary Functors as Modalities in a Linear Calculus. https://arxiv.org/abs/2610.23023

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

arXiv2026

Operon: Incremental Construction of Ragged Data via Named Dimensions

Modern data processing workflows frequently encounter ragged data: collections with variable-length elements that arise naturally in domains like natural language processing, scientific measurements, and autonomous AI agents. Existing workflow engines lack native support for tracking the shapes and dependencies inherent to ragged data, forcing users to manage complex indexing and dependency bookkeeping manually. We present Operon, a Rust-based workflow engine that addresses these challenges through a novel formalism of named dimensions with explicit dependency relations. Operon provides a domain-specific language where users declare pipelines with dimension annotations that are statically verified for correctness, while the runtime system dynamically schedules tasks as data shapes are incrementally discovered during execution. We formalize the mathematical foundation for reasoning about partial shapes and prove that Operon's incremental construction algorithm guarantees deterministic and confluent execution in parallel settings. The system's explicit modeling of partially-known states enables robust persistence and recovery mechanisms, while its per-task multi-queue architecture achieves efficient parallelism across heterogeneous task types. Empirical evaluation demonstrates that Operon outperforms an existing workflow engine with 14.94x baseline overhead reduction while maintaining near-linear end-to-end output rates as workloads scale, making it particularly suitable for large-scale data generation pipelines in machine learning applications.

cs.PL↗
arXiv2026

Dimensional Type Systems and Deterministic Memory Management

We present a dimensional type system whose annotations remain available through the stages that require them, allowing numeric representation and deterministic memory management to be resolved within a single Program Semantic Graph (PSG). Based on Andrew Kennedy's Units of Measure, dimensions constrain admissible operations and the application of domain laws, forming our Native Type Universe (NTU). Range analysis combines those constraints with values, guards, and declared boundaries. A covering representation then determines word width and memory footprint, which participate in allocation and transfer decisions alongside lifetime and target constraints. Our Dimensional Type System (DTS) extends Hindley-Milner inference with abelian-group unification. Within that algebraic fragment, inference is decidable and admits principal types. Measures form part of source-level type identity, while numeric width and storage layout are coeffects resolved from context. A known range that exceeds every available representation produces an error at representation commitment. During program elaboration, unresolved facts can remain pending while further context is supplied. Deterministic Memory Management (DMM) uses the same graph to relate escape paths to storage lifetimes. Closure capture, return, and by-reference use supply different lifetime requirements. Allocation follows the lifetime classification and the platform's declared storage capabilities. Our unique implementation of a posit quire illustrates the interaction: exact accumulation requires a suitable numeric format, adequate capacity, and storage that persists across the accumulation. We also examine how these constraints would apply to automatic differentiation. A shared graph would allow language services to present dimensional resolution and proof status alongside the reasons for representation and placement decisions.

cs.PL↗
arXiv2026

The Program Hypergraph: Multi-Way Relational Structure for Geometric Algebra, Spatial Compute, and Physics-Aware Compilation

Source code organizes a program as expressions and declarations, which a compiler can represent as an abstract syntax tree (AST). Some compilers introduce a further abstraction of the computation as a graph. Nodes represent operations, while connections record how values pass between them and how execution proceeds. Yet these connections can leave the full scope of conditions governing a computation implicit. Developers may then need defensive checks, rely on compiler hacks, pragmas, and implementation-specific code to maintain those conditions as the program evolves. Our thesis is that a hypergraph more faithfully represents complex computation across all targets by making joint constraints inherent to its structure, with an overall less burdensome design-time API. Our Program Hypergraph (PHG) extends our Semantic Graph with relations that connect across an operation's participants, their dependencies, and the invariants they must preserve. Joint resolution in the graph guides lowering into standard Multi-Level Intermediate Representation (MLIR). Satisfiability modulo theories (SMT) checks intrinsic to the graph discharge applicable proof obligations. Supporting information remains available until the decisions that require it are complete. As a primary benefit, verification follows from the rules used to construct and transform the graph. For properties established this way before execution, the generated program needs no added runtime checks, no 'boxing' or 'tagging' or other managed runtime support. We develop this account through geometric algebra, shared-memory capacity, and spatial placement, distinguishing structural guarantees from numerical and resource obligations that require further evidence. The proposed integration makes the same information available at design-time, so engineers can inspect the consequences of a choice before it becomes an implementation constraint.

cs.PL↗