Deriving Distributive Laws for Graded Linear Types

TL;DR

This paper introduces a method to automatically derive distributive laws for graded linear types, facilitating composition and data-flow reasoning in type theories and practical programming languages like Granule and Linear Haskell.

Contribution

It presents an automated deriving procedure for distributive laws in graded linear types, enhancing compositional programming and type reasoning capabilities.

Findings

Automated derivation of distributive combinators for graded linear types.

Implementation of the deriving procedure in Granule and Linear Haskell.

Enabling easier pattern matching analysis and structural combinator derivation.

Abstract

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.