Overview
Linear Core is a type system that understands linearity in the presence of
laziness, unlike traditional type systems which fail to see linearity when
non-strictness makes it less apparent (e.g. by aliasing).
This interaction arises naturally in languages with both linearity and
non-strictness, or in linear strict languages with lazy features.
That said, our primary motivation is the intermediate language of the Glasgow
Haskell Compiler, called Core -- a language which not only combines linearity
with laziness, but also aggressively transforms these programs during the
optimisation passes.
In fact, Core's linear type system cannot understand linearity soon after
optimisations start being applied because they transform the program in a way
which makes linearity no longer syntactic, but still valid. The compiler
optimisations should never turn a linear program into a non-linear one, and
being able to validate linearity throughout the optimisation pipeline, like it
does types, is invaluable as a sanity-check to identify and prevent bugs.
At the moment, the linearity information is simply thrown away before
optimisations.
Claims
Our artifact contains a prototype implementation of Linear Core as a plugin for
the Glasgow Haskell Compiler (GHC). The plugin validates the linearity, according to
Linear Core, at the start of every optimisation pass, of every intermediate
program. It will never interrupt compilation, simply printing FAILED when an
intermediate program is not accepted by our implementation of Linear Core.
We believe Linear Core is a good target for the intermediate language of GHC
because, while being an extension of the existing intermediate language, can
reconcile linearity and laziness in a way robust to all optimisations carried
out by GHC. Our prototype displayed this in practice by accepting almost every
program produced by the GHC pipeline, while rejecting very few -- including
identifying programs which are truly invalid.
We claim our prototype accepts the vast majority of programs produced by the
compiler when compiling linearity-heavy Haskell libraries (over 99% of
intermediate programs from the libraries we tested it on).
Installation
Installation requires an installation of GHC 9.10. We recommend downloading it using GHCup:
export BOOTSTRAP_HASKELL_GHC_VERSION=9.10.3
curl --proto '=https' --tlsv1.2 -sSf https://get-ghcup.haskell.org | sh
Make sure it succeeded and that cabal packages are up to date by running:
ghc --version
cabal --version
cabal update
Second, we need to download the packages we want to test using the linear-core-prototype plugin.
We tested the plugin on the largest open linear Haskell packages we found: linear-base, priority-sesh, linear-smc
How to reproduce the plugin results
Let's reproduce the results individually for the three packages. Note: the
numbers will not match exactly due to changes in the compiler since the numbers
were first produced, but the vast majority of intermediate programs should be
accepted and only few rejected.
linear-base
- Fetch the source
cabal get linear-base-0.5.0
cd linear-base-0.5.0
- Add the plugin to
linear-base.cabal:
diff --git a/linear-base.cabal b/linear-base.cabal
index efab84d..4f7a57e 100644
--- a/linear-base.cabal
+++ b/linear-base.cabal
@@ -144,6 +144,8 @@ library
transformers,
vector >=0.12.2,
primitive
+ build-depends: linear-core-prototype == 0.1.0.0
+ ghc-options: -fplugin=Linear.Core.Plugin
library examples
import: build-opts
- Build the package and pipe to
output:
cabal build linear-base 2>&1 | tee output
- Compute the metrics:
echo "TOTAL REJECTED:"
cat output | grep -A1 FAILED | grep -e '^ ' | wc -l
echo "UNIQUE REJECTED:"
cat output | grep -A1 FAILED | grep -e '^ ' | sort | uniq | wc -l
echo "TOTAL ACCEPTED"
grep SUCCESS output | awk '{print $2}' | tr '\n' '+' | sed 's/+$//' | bc
linear-smc
As above, but for a different package:
- Fetch the source
cabal get linear-smc-2.2.3
cd linear-smc-2.2.3
- Add the plugin to
linear-base.cabal:
diff --git a/linear-smc.cabal b/linear-smc.cabal
index d3d3226..f76eae3 100644
--- a/linear-smc.cabal
+++ b/linear-smc.cabal
@@ -83,6 +83,8 @@ library
build-depends: constraints >= 0.13.4 && < 666
build-depends: array >= 0.5 && < 666
build-depends: base >=4.16.4.0 && < 666
+ build-depends: linear-core-prototype == 0.1.0.0
+ ghc-options: -fplugin=Linear.Core.Plugin
-- Directories containing source files.
hs-source-dirs: .
- Build the package and pipe to
output:
cabal build linear-smc 2>&1 | tee output
- Compute the metrics:
echo "TOTAL REJECTED:"
cat output | grep -A1 FAILED | grep -e '^ ' | wc -l
echo "UNIQUE REJECTED:"
cat output | grep -A1 FAILED | grep -e '^ ' | sort | uniq | wc -l
echo "TOTAL ACCEPTED"
grep SUCCESS output | awk '{print $2}' | tr '\n' '+' | sed 's/+$//' | bc
priority-sesh
- Fetch sources
git clone https://github.com/wenkokke/priority-sesh.git
cd priority-sesh
- Add the plugin
diff --git a/priority-sesh.cabal b/priority-sesh.cabal
index 28b51ac..12b3aba 100644
--- a/priority-sesh.cabal
+++ b/priority-sesh.cabal
@@ -40,6 +40,8 @@ library
, Data.Type.Priority
, System.IO.Linear.Cancellable
hs-source-dirs: src
+ build-depends: linear-core-prototype == 0.1.0.0
+ ghc-options: -fplugin=Linear.Core.Plugin
test-suite test-priority-sesh
import: common-depends
- Build the package
cabal build priority-sesh --allow-newer=linear-base 2>&1 | tee output
- Compute the metrics with the same commands as above
-
Add linear-core-prototype to the build-depends of the package you want to
validate
-
Add -fplugin=Linear.Core.Plugin to the ghc-options field of the package
you want to validate
-
Output cabal build into a file output, e.g. cabal build lib:linear-base -j1 2>&1 | tee output
-
Print out total number of failures
cat output | grep -A1 FAILED | grep -e '^ ' | wc -l
-
Print out number of unique failures
cat output | grep -A1 FAILED | grep -e '^ ' | sort | uniq | wc -l
-
Print out total number of successes
grep SUCCESS output | awk '{print $2}' | tr '\n' '+' | sed 's/+$//' | bc
