Deriving Distributive Laws for Graded Linear Types

Jack Hughes
(University of Kent)
Michael Vollmer
(University of Kent)
Dominic Orchard
(University of Kent)

The recent notion of graded modal types provides a framework for extending type theories with fine-grained data-flow reasoning. The Granule language explores this idea in the context of linear types. In this practical setting, we observe that the presence of graded modal types can introduce an additional impediment when programming: when composing programs, it is often necessary to 'distribute' data types over graded modalities, and vice versa. In this paper, we show how to automatically derive these distributive laws as combinators for programming. We discuss the implementation and use of this automated deriving procedure in Granule, providing easy access to these distributive combinators. This work is also applicable to Linear Haskell (which retrofits Haskell with linear types via grading) and we apply our technique there to provide the same automatically derived combinators. Along the way, we discuss interesting considerations for pattern matching analysis via graded linear types. Lastly, we show how other useful structural combinators can also be automatically derived.

In Ugo Dal Lago and Valeria de Paiva: Proceedings Second Joint International Workshop on Linearity & Trends in Linear Logic and Applications (Linearity&TLLA 2020), Online, 29-30 June 2020, Electronic Proceedings in Theoretical Computer Science 353, pp. 109–131.
Published: 30th December 2021.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: