Linearly Qualified Types: Generic inference for capabilities and uniqueness
A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used safely. However,writing code with explicit linear arguments requires bureaucracy. This paper presents linear constraints, a front-end feature for linear typing that decreases the bureaucracy of working with linear types. Linear constraints are implicit linear arguments that are filled in automatically by the compiler. We present linear constraints 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.
Wed 14 SepDisplayed time zone: Belgrade, Bratislava, Budapest, Ljubljana, Prague change
15:50 - 16:50 | Effects and Type InferenceICFP Papers and Events at Linhart Chair(s): Ben Lippmeier Ghost Locomotion | ||
15:50 20mTalk | Modular Probabilistic Models via Algebraic Effects ICFP Papers and Events Minh Nguyen University of Bristol, Roly Perera Alan Turing Institute, Meng Wang University of Bristol, Nicolas Wu Imperial College London DOI | ||
16:10 20mTalk | Constraint-based type inference for FreezeML ICFP Papers and Events Frank Emrich University of Edinburgh, UK, Jan Stolarek University of Edinburgh, UK, James Cheney University of Edinburgh; Alan Turing Institute, Sam Lindley The University of Edinburgh, UK DOI | ||
16:30 20mTalk | Linearly Qualified Types: Generic inference for capabilities and uniqueness ICFP Papers and Events Arnaud Spiwack Tweag, Csongor Kiss Imperial College London, Jean-Philippe Bernardy University of Gothenburg, Sweden, Nicolas Wu Imperial College London, Richard A. Eisenberg Jane Street Link to publication DOI Pre-print | ||