[Git][ghc/ghc][master] Expand Note [Linear types] with the stance on linting linearity
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Wed Nov 23 17:45:34 UTC 2022
Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC
Commits:
04d0618c by Arnaud Spiwack at 2022-11-23T12:45:14-05:00
Expand Note [Linear types] with the stance on linting linearity
Per the discussion on #22123
- - - - -
2 changed files:
- compiler/GHC/Core/Lint.hs
- compiler/GHC/Core/Multiplicity.hs
Changes:
=====================================
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]
~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
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
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04d0618c16157f61cc03981f8875c96a9adeb879
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/04d0618c16157f61cc03981f8875c96a9adeb879
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20221123/07627f53/attachment-0001.html>
More information about the ghc-commits
mailing list