Skip to content

Linear types (#15981)

Krzysztof Gogolewski requested to merge tweag/ghc:linear-types-submission into master

This is the first step towards implementation of the linear types proposal (https://github.com/ghc-proposals/ghc-proposals/pull/111, #15981 (closed)).

It features

  • A language extension -XLinearTypes
  • Syntax for linear functions in the surface language
  • 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.

The following items are not supported.

  • a # m -> b syntax (only prefix FUN is supported for now)
  • 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
  • Multiplicity coercions (test LinearPolyType)

The important changes, which guide the implementation and can be read first are:

  • The file Multiplicity, which defines type Mult = Type, the Scaled type and functions unrestricted, linear, pattern synonyms One and Omega, quick submultiplicity test submult
  • The change to FunTy and new mkFunTy in TyCoRep, where the multiplicity argument is added
  • The change to funTyCon in TysPrim
  • The new unrestrictedFunTyCon and multiplicityTy in TysWiredIn
  • Var has now a new field varMult; functions such as updateVarTypeAndMult can 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 varMult of the case binder.
  • The file UsageEnv defines a map from a variable to its multiplicity, used when typechecking
  • Calls to submult and tcSubMult, which guide multiplicity checking in the type checker
  • ensureSubMult and 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

  • Richard Eisenberg
  • Krzysztof Gogolewski
  • Matthew Pickering
  • Arnaud Spiwack

With contributions from:

  • Mark Barbone
  • Alexander Vershilov
Edited by Krzysztof Gogolewski

Merge request reports