Linear type systems guarantee linear resources are used exactly once. Traditionally, using a resource is synonymous with its syntactic occurrence in the program, however, under the lens of non-strict evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is executed. Semantic linearity becomes especially vital when considering the internal language of an optimising compiler, where optimisations heavily rewrite the source program in ways that can often break syntactic linearity but that aim to preserve the program's semantics. We present Linear Core, the first type system that understands semantic linearity in the presence of non-strict evaluation, suitable for the Core intermediate language of the Glasgow Haskell Compiler. We prove Linear Core is sound and guarantees linear resource usage and prove multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base.

Cross-stage persistence rules are commonly admitted in multi-stage programming languages. These rules codify the assumption that all module and package dependencies are available at all stages. However, in practice, only a small number of dependencies may be needed at each particular stage. This paper introduces Explicit Level Imports, a mechanism which gives programmers precise control about which dependencies are required at each stage. Imports are annotated with a modifier which brings identifiers into scope at a specific level. This precision means it is straightforward for the compiler to work out what is exactly needed at each stage, and only provide that. The result is faster compilation times and the potential for improved cross-compilation support. We have implemented these ideas in GHC Haskell, consider a wide variety of practical considerations in the design, and finally demonstrate that the feature solves a real-world issue in a pragmatic way.

Linear type systems guarantee linear resources are used exactly once. Traditionally, using a resource is synonymous with its syntactic occurrence in the program, however, under the lens of lazy evaluation, linearity can be further understood semantically, where a syntactic occurrence of a resource does not necessarily entail using that resource when the program is evaluated. Semantic linearity is especially necessary in optimising compilers for languages combining linearity and laziness: optimisations leverage laziness to heavily rewrite the source program, pushing the interaction of linearity and laziness to its limit, regardless of the original program typing linearity conservatively. We present Linear Core, the first type system that understands semantic linearity in the presence of laziness, suit- able for the Core intermediate language of the Glasgow Haskell Compiler. We prove Linear Core is both type safe and that multiple optimising transformations preserve linearity in Linear Core while failing to do so in Core. We have implemented Linear Core as a compiler plugin to validate the system against linearity-heavy libraries, including linear-base, in the heart of the compiler.

Type-driven program synthesis is concerned with automatic generation of programs that satisfy a given specification, formulated as a type. One of the key challenges of program synthesis lies in finding candidate solutions that adhere to both the specification and the user’s intent in an actionable amount of time. In this work, we explore how linear types allow for precise specifications suitable for synthesis, and present a framework for synthesis with linear types that, through the Curry- Howard correspondence, leverages existing proof-search techniques for Linear Logic to efficiently find type-correct programs. We implement the synthesis framework both as a standalone language which supports classical linear types extended with recursive algebraic data types, parametric polymorphism and basic refinements; and as a GHC type-hole plugin that synthesises expressions for Haskell program holes, using the recently introduced linear types feature – showing it can generate precise solutions, remarkably fast.