diff options
author | Arnaud Spiwack <arnaud.spiwack@tweag.io> | 2022-08-31 09:27:23 +0200 |
---|---|---|
committer | Marge Bot <ben+marge-bot@smart-cactus.org> | 2022-11-23 12:45:14 -0500 |
commit | 04d0618c16157f61cc03981f8875c96a9adeb879 (patch) | |
tree | b6af66b7630145f74bbd525aa9b4dbd16a12aeec | |
parent | 0b7fef1112c92d2781a7d74e02dceefd4f8cd870 (diff) | |
download | haskell-04d0618c16157f61cc03981f8875c96a9adeb879.tar.gz |
Expand Note [Linear types] with the stance on linting linearity
Per the discussion on #22123
-rw-r--r-- | compiler/GHC/Core/Lint.hs | 95 | ||||
-rw-r--r-- | compiler/GHC/Core/Multiplicity.hs | 90 |
2 files changed, 146 insertions, 39 deletions
diff --git a/compiler/GHC/Core/Lint.hs b/compiler/GHC/Core/Lint.hs index ea443e3b91..bb192a3278 100644 --- a/compiler/GHC/Core/Lint.hs +++ b/compiler/GHC/Core/Lint.hs @@ -2863,21 +2863,86 @@ we behave as follows (#15057, #T15664): Note [Linting linearity] ~~~~~~~~~~~~~~~~~~~~~~~~ -There is one known optimisations that have not yet been updated -to work with Linear Lint: - -* Optimisations can create a letrec which uses a variable linearly, e.g. - letrec f True = f False - f False = x - in f True - uses 'x' linearly, but this is not seen by the linter. - Plan: make let-bound variables remember the usage environment. - See ticket #18694. - -We plan to fix this issue in the very near future. -For now, -dcore-lint enables only linting output of the desugarer, -and full Linear Lint has to be enabled separately with -dlinear-core-lint. -Ticket #19165 concerns enabling Linear Lint with -dcore-lint. +Core understands linear types: linearity is checked with the flag +`-dlinear-core-lint`. Why not make `-dcore-lint` check linearity? Because +optimisation passes are not (yet) guaranteed to maintain linearity. They should +do so semantically (GHC is careful not to duplicate computation) but it is much +harder to ensure that the statically-checkable constraints of Linear Core are +maintained. The current Linear Core is described in the wiki at: +https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation. + +Why don't the optimisation passes maintain the static types of Linear Core? +Because doing so would cripple some important optimisations. Here is an +example: + + data T = MkT {-# UNPACK #-} !Int + +The wrapper for MkT is + + $wMkT :: Int %1 -> T + $wMkT n = case %1 n of + I# n' -> MkT n' + +This introduces, in particular, a `case %1` (this is not actual Haskell or Core +syntax), where the `%1` means that the `case` expression consumes its scrutinee +linearly. + +Now, `case %1` interacts with the binder swap optimisation in a non-trivial +way. Take a slightly modified version of the code for $wMkT: + + case %1 x of z { + I# n' -> (x, n') + } + +Binder-swap wants to change this to + + case %1 x of z { + I# n' -> let x = z in (x, n') + } + +Now, this is not something that a linear type checker usually considers +well-typed. It is not something that `-dlinear-core-lint` considers to be +well-typed either. But it's only because `-dlinear-core-lint` is not good +enough. However, making `-dlinear-core-lint` recognise this expression as valid +is not obvious. There are many such interactions between a linear type system +and GHC optimisations documented in the linear-type implementation wiki page +[https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types/implementation#core-to-core-passes]. + +PRINCIPLE: The type system bends to the optimisation, not the other way around. + +In the original linear-types implementation, we had tried to make every +optimisation pass produce code that passes `-dlinear-core-lint`. It had proved +very difficult. And we kept finding corner case after corner case. Plus, we +used to restrict transformations when `-dlinear-core-lint` couldn't typecheck +the result. There are still occurrences of such restrictions in the code. But +our current stance is that such restrictions can be removed. + +For instance, some optimisations can create a letrec which uses a variable +linearly, e.g. + + letrec f True = f False + f False = x + in f True + +uses 'x' linearly, but this is not seen by the linter. This issue is discussed +in ticket #18694. + +Plus in many cases, in order to make a transformation compatible with linear +linting, we ended up restricting to avoid producing patterns that were not +recognised as linear by the linter. This violates the above principle. + +In the future, we may be able to lint the linearity of the output of +Core-to-Core passes (#19165). But right now, we can't. Therefore, in virtue of +the principle above, after the desguarer, the optimiser should take no special +pains to preserve linearity (in the type system sense). + +In general the optimiser tries hard not to lose sharing, so it probably doesn't +actually make linear things non-linear. We postulate that any program +transformation which breaks linearity would negatively impact performance, and +therefore wouldn't be suitable for an optimiser. An alternative to linting +linearity after each pass is to prove this statement. + +There is a useful discussion at https://gitlab.haskell.org/ghc/ghc/-/issues/22123 Note [checkCanEtaExpand] ~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/compiler/GHC/Core/Multiplicity.hs b/compiler/GHC/Core/Multiplicity.hs index 4132533b1b..89cb89936b 100644 --- a/compiler/GHC/Core/Multiplicity.hs +++ b/compiler/GHC/Core/Multiplicity.hs @@ -51,22 +51,30 @@ The detailed design is in the _Linear Haskell_ article [https://arxiv.org/abs/1710.09756]. Other important resources in the linear types implementation wiki page [https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation], and the -proposal [https://github.com/ghc-proposals/ghc-proposals/pull/111] which +proposal [https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst] which describes the concrete design at length. For the busy developer, though, here is a high-level view of linear types is the following: - Function arrows are annotated with a multiplicity (as defined by type `Mult` and its smart constructors in this module) - - Because, as a type constructor, the type of function now has an extra - argument, the notation (->) is no longer suitable. We named the function - type constructor `FUN`. - - (->) retains its backward compatible meaning: `(->) a b = a -> b`. To - achieve this, `(->)` is defined as a type synonym to `FUN Many` (see + - Multiplicities, in Haskell, are types of kind `GHC.Types.Multiplicity`. + as in + + map :: forall (p :: Multiplicity). (a %p -> b) -> [a] %p -> [b] + + - The type constructor for function types (FUN) has type + + FUN :: forall (m :: Multiplicity) -> forall {r1) {r2}. TYPE r1 -> TYPE r2 -> Type + + The argument order is explained in https://gitlab.haskell.org/ghc/ghc/-/issues/20164 + - (->) retains its backward compatible meaning: + + (->) a b = a -> b = a %'Many -> b + + To achieve this, `(->)` is defined as a type synonym to `FUN Many` (see below). -- Multiplicities can be reified in Haskell as types of kind - `GHC.Types.Multiplicity` -- Ground multiplicity (that is, without a variable) can be `One` or `Many` +- A ground multiplicity (that is, without a variable) can be `One` or `Many` (`Many` is generally rendered as ω in the scientific literature). Functions whose type is annotated with `One` are linear functions, functions whose type is annotated with `Many` are regular functions, often called “unrestricted” @@ -75,19 +83,9 @@ For the busy developer, though, here is a high-level view of linear types is the consumed exactly once, *then* its argument is consumed exactly once. You can think of “consuming exactly once” as evaluating a value in normal form exactly once (though not necessarily in one go). The _Linear Haskell_ article (see - infra) has a more precise definition of “consuming exactly once”. -- Data types can have unrestricted fields (the canonical example being the - `Unrestricted` data type), then these don't need to be consumed for a value to - be consumed exactly once. So consuming a value of type `Unrestricted` exactly - once means forcing it at least once. -- Why “at least once”? Because if `case u of { C x y -> f (C x y) }` is linear - (provided `f` is a linear function). So we might as well have done `case u of - { !z -> f z }`. So, we can observe constructors as many times as we want, and - we are actually allowed to force the same thing several times because laziness - means that we are really forcing a the value once, and observing its - constructor several times. The type checker and the linter recognise some (but - not all) of these multiple forces as indeed linear. Mostly just enough to - support variable patterns. + supra) has a more precise definition of “consuming exactly once”. +- Data constructors are linear by default. + See Note [Data constructors are linear by default]. - Multiplicities form a semiring. - Multiplicities can also be variables and we can universally quantify over these variables. This is referred to as “multiplicity @@ -102,6 +100,8 @@ For the busy developer, though, here is a high-level view of linear types is the multiplicity `Many` can consume its scrutinee as many time as it wishes (no matter how much the case expression is consumed). +For linear types in the linter see Note [Linting linearity] in GHC.Core.Lint. + Note [Usages] ~~~~~~~~~~~~~ In the _Linear Haskell_ paper, you'll find typing rules such as these: @@ -208,8 +208,8 @@ branch. Note [Data constructors are linear by default] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Data constructors defined without -XLinearTypes (as well as data constructors -defined with the Haskell 98 in all circumstances) have all their fields linear. +All data constructors defined without -XLinearTypes, as well as data constructors +defined with the Haskell 98 in all circumstances, have all their fields linear. That is, in @@ -219,10 +219,52 @@ We have Just :: a %1 -> Just a +Irrespective of whether -XLinearTypes is turned on or not. Furthermore, when +-XLinearTypes is turned off, the declaration + + data Endo a where { MkIntEndo :: (Int -> Int) -> T Int } + +gives + + MkIntEndo :: (Int -> Int) %1 -> T Int + +With -XLinearTypes turned on, instead, this would give + + data EndoU a where { MkIntEndoU :: (Int -> Int) -> T Int } + MkIntEndoU :: (Int -> Int) -> T Int + +With -XLinearTypes turned on, to get a linear field with GADT syntax we +would need to write + + data EndoL a where { MkIntEndoL :: (Int -> Int) %1 -> T Int } + The goal is to maximise reuse of types between linear code and traditional code. This is argued at length in the proposal and the article (links in Note [Linear types]). +Unrestricted field don't need to be consumed for a value to be consumed exactly +once. So consuming a value of type `IntEndoU a` exactly once means forcing it at +least once. + +Why “at least once”? Because if `case u of { MkIntEndoL x -> f (MkIntEndoL x) }` +is linear (provided `f` is a linear function). But we might as well have done +`case u of { !z -> f z }`. So, we can observe constructors as many times as we +want, and we are actually allowed to force the same thing several times because +laziness means that we are really forcing the value once, and observing its +constructor several times. The type checker and the linter recognise some (but +not all) of these multiple forces as indeed linear. Mostly just enough to +support variable patterns. + +In summary: + +- Fields of data constructors defined with Haskell 98 syntax are always linear + (even if `-XLinearTypes` is off). This choice has been made to favour sharing + types between linearly typed Haskell and traditional Haskell. To avoid an + ecosystem split. +- When `-XLinearTypes` is off, GADT-syntax declaration can only use the regular + arrow `(->)`. However all the fields are linear. + + Note [Polymorphisation of linear fields] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The choice in Note [Data constructors are linear by default] has an impact on |