Search papers, labs, and topics across Lattice.
This paper introduces linear constraints, a qualified type system that acts as implicit linear arguments, addressing the bureaucratic overhead of explicit linear arguments in Linear Haskell. The system extends GHC's constraint solver algorithm, allowing the compiler to automatically fill in linear arguments, ensuring safe resource management. Soundness is guaranteed through desugaring into Linear Haskell, with a simplified formal system and constraint solver compared to prior work.
Automate resource management in Linear Haskell with linear constraints, eliminating the need for explicit linear arguments and streamlining development.
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.
