WIP: Linear types (#15981)
This is the first step towards implementation of the linear types proposal (https://github.com/ghc-proposals/ghc-proposals/pull/111, #15981).
- A language extension -XLinearTypes
- Syntax for linear functions in the surface language
- Syntax for multiplicity-polymorphic functions in the surface language (experimental, incomplete, and unstable)
- Linearity checking in Core Lint
- Core-to-core passes are compatible with linearity
- Fields in a data type can be linear or unrestricted; linear fields have multiplicity-polymorphic constructors. If -XLinearTypes is disabled, the GADT syntax defaults to linear fields,
There are several issues which are not yet completed and need to be fixed before this PR is merged. However, they shouldn't block review, and they will be local changes to the commit.
- Syntax. The branch uses
a ->. b(for the linear arrow),
a -->.(m) b(for the multiplicity-polymorphic arrow),
FUN(the multiplicity-polymorphic arrow which can be partially applied). This will be changed according to the decision of the committee.
- Template Haskell is currently unsupported. This will be fixed and depends on the decision of the committee.
- There are 11 failing tests in total that were marked as expect_broken. They concern Template Haskell (will be fixed together with the previous point), partially applied unboxed tuples, holes (output changes because of issue #16456 (closed)), multiplicity coercions (the test LinearPolyType), Haddock (bug https://github.com/haskell/haddock/issues/1048).
The following items are not supported.
- Full multiplicity inference (multiplicities are really only checked)
- Decent linearity error messages
- Linear let, where, and case expressions in the surface language (each of these currently introduce the unrestricted variant)
- Multiplicity-parametric fields
- Syntax for annotating lambda-bound or let-bound with a multiplicity
- Syntax for non-linear/multiple-field-multiplicity records
- Linear projections for records with a single linear field
- Linear pattern synonyms
The important changes, which guide the implementation and can be read first are:
- The file
Multiplicity, which defines
type Mult = Type, the
Scaledtype and functions
linear, pattern synonyms
Omega, quick submultiplicity test
- The change to
TyCoRep, where the multiplicity argument is added
- The change to
- The new
Varhas now a new field
varMult; functions such as
updateVarTypeAndMultcan be used to update multiplicity (e.g. when zonking). In Core, the multiplicity of a lambda is indicated by its
varMult; multiplicity of a case expression is indicated by
varMultof the case binder.
- The functions
basicTypes/DataCon, which are adding multiplicity variables to constructors. The change to
wrapper_reqdmeans that all data constructors have a wrapper now.
- The file
UsageEnvdefines a map from a variable to its multiplicity, used when typechecking
- Calls to
tcSubMult, which guide multiplicity checking in the type checker
ensureSubMultand its calls, which guide multiplicity checking in Lint
A high-level description can be found at https://ghc.haskell.org/trac/ghc/wiki/LinearTypes/Implementation Following the link above you will find a description of the changes made to Core.
This commit has been authored by
- Krzysztof Gogolewski
- Matthew Pickering
- Arnaud Spiwack
With contributions from:
- Mark Barbone
- Alexander Vershilov