Linear lambda calculus supports arbitrary functors as computational modalities

Arbitrary Functors as Modalities in a Linear Calculus

Programming Languages

Summary

This paper looks at how certain features called modalities can be used inside a version of programming language theory called linear lambda calculus, which carefully tracks resources. The authors interpret these features using mathematical structures called functors, even when those functors don't behave in usual ways like distributing over products. They provide a general mathematical model and then focus on one that describes resources concretely. This lets them develop a method to simplify expressions systematically. Their approach is backed by formal computer-verified proofs to ensure correctness. The work sets the stage for new kinds of programming languages that can use these complex modality features.

What this means in practice

  • For programming language designers: design new programming languages that incorporate complex resource-aware modalities for more precise control of effects and resource management
  • For functional programmers: implement language extensions that safely handle various computational effects using arbitrary functors without requiring product distribution

A theory result. No direct application yet.

Authors

Jean-Philippe Bernardy, Andreas Abel

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.
View PDFOpen arXiv