Linear Constraints

TL;DR

This paper introduces linear constraints in Haskell, enabling implicit resource management through a qualified type system and an inference algorithm that extends GHC's constraint solver.

Contribution

It presents a new feature for linear constraints as implicit linear arguments, with a formal system, an inference algorithm, and applications, simplifying linear resource management in Haskell.

Findings

Linear constraints act as implicit linear arguments in Haskell.

The inference algorithm extends GHC's existing constraint solver.

The formal system and solver have been significantly simplified and extended.

Abstract

Linear constraints are the linear counterpart of Haskell's class constraints. Linearly typed parameters allow the programmer to control resources such as file handles and manually managed memory as linear arguments. Indeed, a linear type system can verify that these resources are used safely. However, writing code with explicit linear arguments requires bureaucracy. Linear constraints address this shortcoming: a linear constraint acts as an implicit linear argument that can be filled in automatically by the compiler. We present this new feature as a qualified type system, together with an inference algorithm which extends GHC's existing constraint solver algorithm. Soundness of linear constraints is ensured by the fact that they desugar into Linear Haskell. This paper is a revised and extended version of a previous paper by the same authors (arXiv:2103.06127). The formal system and the constraint solver have been significantly simplified and numerous additional applications are described.