Linear types: stepping stone

Authored by aspiwack on Nov 30 2018, 5:28 PM.



This is the first step towards implementation of the linear-type
proposal ( , Trac #15981 ).

It features

  • Linearity checking in Core Lint
  • Core-to-core passes are compatible with linearity
  • 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)
  • Do-notation, with rebindable syntax, is compatible with linear types (even multiplicity-polymorphic types, presumably, but they don't work well enough to be tested with this feature)
  • GADT syntax defaults to linear without -XLinearTypes

It doesn't have yet

  • Full multiplicity inference (multiplicities are really only checked)
  • Decent linearity error messages
  • Proper multiplicity polymorphism in constructors (as a simplification, all constructors have a single multiplicity parameter, instead of one per linear field)
  • Linear let, where, and case expressions in the surface language (each of these currently introduce the unresricted variant)
  • Multiplicity-parametric data types
  • 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
  • Full support for Typable with linear types (typable will refuse to decompose linear functions)
  • Template Haskell support for linear types

A high-level description can be found at
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

Diff Detail

rGHC Glasgow Haskell Compiler
Lint WarningsExcuse: As far as possible I tried to avoid long lines in files without long lines, but this patch is rather large, so some may have fallen through the cracks.
Warningcompiler/backpack/RnModIface.hs:647TXT3Line Too Long
Warningcompiler/basicTypes/DataCon.hs:580TXT3Line Too Long
Warningcompiler/basicTypes/DataCon.hs:888TXT3Line Too Long
Warningcompiler/basicTypes/DataCon.hs:959TXT3Line Too Long
Warningcompiler/basicTypes/DataCon.hs:1154TXT3Line Too Long
Warningcompiler/basicTypes/DataCon.hs:1363TXT3Line Too Long
Warningcompiler/basicTypes/Demand.hs:1957TXT3Line Too Long
Warningcompiler/basicTypes/Id.hs:231TXT3Line Too Long
Warningcompiler/basicTypes/Id.hs:350TXT3Line Too Long
Warningcompiler/basicTypes/Id.hs:366TXT3Line Too Long
Warningcompiler/basicTypes/Id.hs:373TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:565TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:811TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:815TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:828TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:860TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:913TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:950TXT3Line Too Long
Warningcompiler/basicTypes/MkId.hs:953TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:1TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:5TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:6TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:121TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:177TXT3Line Too Long
Warningcompiler/basicTypes/Multiplicity.hs:189TXT3Line Too Long
No Unit Test Coverage
Build Status
Buildable 25538
Build 64906: [GHC] Linux/amd64: Continuous Integration
Build 64905: [GHC] OSX/amd64: Continuous Integration
Build 64904: [GHC] Windows/amd64: Continuous Integration
Build 64903: arc lint + arc unit
aspiwack created this revision.Nov 30 2018, 5:28 PM

The description of the implementation and the Core formalism, are not up to date. We'll be updating it in the coming days and report back here.

Known issues

  • Unboxed tuples and sums are not multiplicity-polymorphic. This causes some partial application do have a wrong type.
  • Multiplicity polymorphism appears in some messages
  • Omega (!) appears in messages involving pattern synonyms
  • As (->) is a type synonym, :info (->) doesn't show instances anymore
  • There are various indication that some core-2-core passes are less performant (in some cases I suspect the additional wrappers to confuse the pass, e.g. )
  • Guard-exaustiveness checking seems to usually fail. Probably because of the wrapper around the True data constructor.

Generally speaking we have some tests which don't pass. They are marked as expect_broken, when followed by a 3-digit number, then it's a reference to a issue in our local issue tracker at .

All the incorrect and otherwise suspicious behaviours can be found in the backwards compatibility column of .

I also believe that the linter is more lenient than master's (too lenient). I haven't yet characterised the issue, so it's only a sentiment. But I'm pretty sure that I've seen the linter let things through which it shouldn't. I suspect we merged something wrong. It may be hiding bugs.

monoidal updated this revision to Diff 18978.Dec 3 2018, 4:15 AM
monoidal added a subscriber: monoidal.

Whitespace, remove accidentally commited file

I do intend to take a close look at this, but it likely won't happen until after classes end, in about 2 weeks.

In the meantime, what is your intent in posting this? Is it to get early feedback on your implementation and then to close without merging? Do you expect to update this diff periodically as you write more features? Is this meant to be a stable intermediate state that (after review) should be merged?

Thanks! :)

Thanks Richard!

I intend this differential to be mergeable (and merged): despite its shortcomings it's already useful (it is, however a pain to learn at this point, in particular the error messages are bad, bad, bad!). At least to be merged after the bugs listed in my first comment are fixed, and syntax is decided, I'm hoping review can fish some of them out, to be honest. But we will be investigating on our end too.

Further features however, will be submitted as distinct differentials. Hopefully after some review has help consolidate the quality of this one, which is intended as a solid foundation upon which to build the rest of the proposal.

At least to be merged after the bugs listed in my first comment are fixed, and syntax is decided,

Yes -- we really do need to agree syntax before landing it.

simonpj added inline comments.Dec 13 2018, 9:07 AM

Why do we need this at all? Why not just have Multiplicity = Type.


What is MultThing? What instantiates the 'a'?


I suggest using "smart constructors" since you are not using the pattern synonyms in pattern matching!

mkMultMul :: GMult a -> GMult a -> GMult a


Why Required?

(And generally, Inferred comes first.)


simonpj added inline comments.Dec 13 2018, 9:22 AM

What is Alias?

aspiwack added inline comments.Dec 14 2018, 7:27 AM

We wondered which choice would be better. Initially we settled on having a Mult type because we do quite a bit of algebraic manipulations on multiplicities throughout the code. It's much more convenient and robust to have a data constructors for this than to deconstruct a type. What we didn't think of at the time was to use pattern synonyms for that effect.

Another thing we're using GMult for is to enforce algebraic invariants on the type. Such as there never being a subexpression of the form MulMult One p. In the future I planned to go further and represent multiplicities as something like a list of lists representing sums-of-products (as MulMult distributes over MulAdd and they are both associative).

I see basically three options

  • Keep Mult as it is today
  • Store a Type in FunTy (and in Core's Var, maybe?) in the multiplicity position, and have a view function Type -> Mult. This way we can dispense with almost all traversals on Mult, but we can still get the benefits of Mult where we actually use it. One downside is that we would renormalise multiplicities every time we reason on multiplicities, but I don't imagine that this would be significant. A more serious downside is that types don't warn us when we want to perform non-syntactic equality, which I believe to be what we want for multiplicities (we really want One * p and p to be the same type).
  • Get rid of Mult altogether. And instead use pattern synonyms to perform normalisation on the fly. It's got about the same advantages and disadvantages as the previous option. It's a tad more economical in terms of code, but also a tad trickier.

It's not clear to me, at this point, which is best.


I'll document.


They are pattern synonyms because we pattern match on these, and I really don't want to export the real constructors, as they would make it possible for invariants to be broken.


It is documented in the type definition.

data VarMult
  = Regular Mult
  -- ^ a normal variable, carrying a multiplicity like in the Linear Haskell
  -- paper
  | Alias
  -- ^ a variable typed as a alias for the multiplicity of other variables, this
  -- lets the variable be used differently depending on the branch. Tremendously
  -- useful for join points. But also used for regular lets because of inlining,
  -- float out, and common subexpression elimination.

I'm not hugely fond of the name to be honest. So suggestions are welcome.

monoidal updated this revision to Diff 19236.Dec 24 2018, 8:29 AM

New version

mboes added a subscriber: mboes.Dec 24 2018, 8:47 AM

@simonpj, @goldfire, would you prefer to continue reviewing this here or should we move this to GitLab?

monoidal abandoned this revision.Mar 26 2019, 10:19 AM

We'll be moving the patch to GitLab soon.