diff options
Diffstat (limited to 'docs/users_guide')
| -rw-r--r-- | docs/users_guide/8.12.1-notes.rst | 9 | ||||
| -rw-r--r-- | docs/users_guide/debugging.rst | 10 | ||||
| -rw-r--r-- | docs/users_guide/exts/levity_polymorphism.rst | 2 | ||||
| -rw-r--r-- | docs/users_guide/exts/linear_types.rst | 196 | ||||
| -rw-r--r-- | docs/users_guide/exts/types.rst | 1 |
5 files changed, 218 insertions, 0 deletions
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst index a66ab06514..c729a8ec6c 100644 --- a/docs/users_guide/8.12.1-notes.rst +++ b/docs/users_guide/8.12.1-notes.rst @@ -10,6 +10,15 @@ following sections. Highlights ---------- +* The :extension:`LinearTypes` extension enables linear function syntax + ``a #-> b``, as described in the `Linear Types GHC proposal + <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst>`__. + + The GADT syntax can be used to define data types with linear and nonlinear fields. + + This extension is considered experimental: it doesn't implement the full proposal yet and the details + are subject to change. + * NCG - The linear register allocator saw improvements reducing the number diff --git a/docs/users_guide/debugging.rst b/docs/users_guide/debugging.rst index c777ccc25c..4b86617093 100644 --- a/docs/users_guide/debugging.rst +++ b/docs/users_guide/debugging.rst @@ -837,6 +837,16 @@ Checking for consistency Turn on heavyweight intra-pass sanity-checking within GHC, at Core level. (It checks GHC's sanity, not yours.) +.. ghc-flag:: -dlinear-core-lint + :shortdesc: Turn on internal sanity checking + :type: dynamic + + Turn on linearity checking in GHC. Currently, some optimizations + in GHC might not preserve linearity and they valid programs might + fail Linear Core Lint. + In the near future, this option will be removed and folded into + normal Core Lint. + .. ghc-flag:: -dstg-lint :shortdesc: STG pass sanity checking :type: dynamic diff --git a/docs/users_guide/exts/levity_polymorphism.rst b/docs/users_guide/exts/levity_polymorphism.rst index d7954915a0..a65f878b41 100644 --- a/docs/users_guide/exts/levity_polymorphism.rst +++ b/docs/users_guide/exts/levity_polymorphism.rst @@ -89,6 +89,8 @@ These functions do not bind a levity-polymorphic variable, and so are accepted. Their polymorphism allows users to use these to conveniently stub out functions that return unboxed types. +.. _printing-levity-polymorphic-types: + Printing levity-polymorphic types --------------------------------- diff --git a/docs/users_guide/exts/linear_types.rst b/docs/users_guide/exts/linear_types.rst new file mode 100644 index 0000000000..1b725f36cc --- /dev/null +++ b/docs/users_guide/exts/linear_types.rst @@ -0,0 +1,196 @@ +Linear types +============ + +.. extension:: LinearTypes + :shortdesc: Enable linear types. + + :since: 8.12.1 + + Enable the linear arrow ``a #-> b`` and the multiplicity-polymorphic arrow + ``a # m -> b``. + +**This extension is currently considered experimental, expect bugs, +warts, and bad error messages; everything down to the syntax is +subject to change**. See, in particular, +:ref:`linear-types-limitations` below. We encourage you to experiment +with this extension and report issues in the GHC bug tracker `the GHC +bug tracker <https://gitlab.haskell.org/ghc/ghc/issues>`__, adding the +tag ``LinearTypes``. + +A function ``f`` is linear if: when its result is consumed *exactly +once*, then its argument is consumed *exactly once*. Intuitively, it +means that in every branch of the definition of ``f``, its argument +``x`` must be used exactly once. Which can be done by + +* Returning ``x`` unmodified +* Passing ``x`` to a *linear* function +* Pattern-matching on ``x`` and using each argument exactly once in the + same fashion. +* Calling it as a function and using the result exactly once in the same + fashion. + +With ``-XLinearTypes``, you can write ``f :: a #-> b`` to mean that +``f`` is a linear function from ``a`` to ``b``. If +:extension:`UnicodeSyntax` is enabled, the ``#->`` arrow can be +written as ``⊸``. + +To allow uniform handling of linear ``a #-> b`` and unrestricted ``a +-> b`` functions, there is a new function type ``a # m -> b``. This +syntax is, however, not implemented yet, see +:ref:`linear-types-limitations`. Here, ``m`` is a type of new kind +``Multiplicity``. We have: + +:: + + data Multiplicity = One | Many -- Defined in GHC.Types + + type a #-> b = a # 'One -> b + type a -> b = a # 'Many -> b + +(See :ref:`promotion`). + +We say that a variable whose multiplicity constraint is ``Many`` is +*unrestricted*. + +The multiplicity-polymorphic arrow ``a # m -> b`` is available in a prefix +version as ``GHC.Exts.FUN m a b``, which can be applied +partially. See, however :ref:`linear-types-limitations`. + +Linear and multiplicity-polymorphic arrows are *always declared*, +never inferred. That is, if you don't give an appropriate type +signature to a function, it will be inferred as being a regular +function of type ``a -> b``. + +Data types +---------- +By default, all fields in algebraic data types are linear (even if +``-XLinearTypes`` is not turned on). Given + +:: + + data T1 a = MkT1 a + +the value ``MkT1 x`` can be constructed and deconstructed in a linear context: + +:: + + construct :: a #-> MkT1 a + construct x = MkT1 x + + deconstruct :: MkT1 a #-> a + deconstruct (MkT1 x) = x -- must consume `x` exactly once + +When used as a value, ``MkT1`` is given a multiplicity-polymorphic +type: ``MkT1 :: forall {m} a. a # m -> T1 a``. This makes it possible +to use ``MkT1`` in higher order functions. The additional multiplicity +argument ``m`` is marked as inferred (see +:ref:`inferred-vs-specified`), so that there is no conflict with +visible type application. When displaying types, unless +``-XLinearTypes`` is enabled, multiplicity polymorphic functions are +printed as regular functions (see :ref:`printing-linear-types`); +therefore constructors appear to have regular function types. + +:: + + mkList :: [a] -> [MkT1 a] + mkList xs = map MkT1 xs + +Hence the linearity of type constructors is invisible when +``-XLinearTypes`` is off. + +Whether a data constructor field is linear or not can be customized using the GADT syntax. Given + +:: + + data T2 a b c where + MkT2 :: a -> b #-> c #-> T2 a b -- Note unrestricted arrow in the first argument + +the value ``MkT2 x y z`` can be constructed only if ``x`` is +unrestricted. On the other hand, a linear function which is matching +on ``MkT2 x y z`` must consume ``y`` and ``z`` exactly once, but there +is no restriction on ``x``. + +If :extension:`LinearTypes` is disabled, all fields are considered to be linear +fields, including GADT fields defined with the ``->`` arrow. + +In a ``newtype`` declaration, the field must be linear. Attempting to +write an unrestricted newtype constructor with GADT syntax results in +an error. + +.. _printing-linear-types: + +Printing multiplicity-polymorphic types +--------------------------------------- +If :extension:`LinearTypes` is disabled, multiplicity variables in types are defaulted +to ``Many`` when printing, in the same manner as described in :ref:`printing-levity-polymorphic-types`. +In other words, without :extension:`LinearTypes`, multiplicity-polymorphic functions +``a # m -> b`` are printed as normal Haskell2010 functions ``a -> b``. This allows +existing libraries to be generalized to linear types in a backwards-compatible +manner; the general types are visible only if the user has enabled +:extension:`LinearTypes`. +(Note that a library can declare a linear function in the contravariant position, +i.e. take a linear function as an argument. In this case, linearity cannot be +hidden; it is an essential part of the exposed interface.) + +.. _linear-types-limitations: + +Limitations +----------- +Linear types are still considered experimental and come with several +limitations. If you have read the full design in the proposal (see +:ref:`linear-types-references` below), here is a run down of the +missing pieces. + +- The syntax ``a # p -> b`` is not yet implemented. You can use ``GHC.Exts.FUN + p a b`` instead. However, be aware of the next point. +- Multiplicity polymorphism is incomplete and experimental. You may + have success using it, or you may not. Expect it to be really unreliable. +- There is currently no support for multiplicity annotations such as + ``x :: a # p``, ``\(x :: a # p) -> ...``. +- All ``case``, ``let`` and ``where`` statements consume their + right-hand side, or scrutiny, ``Many`` times. That is, the following + will not type check: + + :: + + g :: A #-> (A, B) + h :: A #-> B #-> C + + f :: A #-> C + f x = + case g x of + (y, z) -> h y z + + This can be worked around by defining extra functions which are + specified to be linear, such as: + + :: + + g :: A #-> (A, B) + h :: A #-> B #-> C + + f :: A #-> C + f x = f' (g x) + where + f' :: (A, B) #-> C + f' (y, z) = h y z +- There is no support for linear pattern synonyms. +- ``@``-patterns and view patterns are not linear. +- The projection function for a record with a single linear field should be + multiplicity-polymorphic; currently it's unrestricted. +- Attempting to use of linear types in Template Haskell will probably + not work. + +.. _linear-types-references: + +Design and further reading +-------------------------- + +* The design for this extension is described in details in the `Linear + types proposal + <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst>`__ +* This extension has been originally conceived of in the paper `Linear + Haskell: practical linearity in a higher-order polymorphic language + <https://www.microsoft.com/en-us/research/publication/linear-haskell-practical-linearity-higher-order-polymorphic-language/>`__ + (POPL 2018) +* There is a `wiki page dedicated to the linear types extension <https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types>`__ diff --git a/docs/users_guide/exts/types.rst b/docs/users_guide/exts/types.rst index f5fd5d130e..2cd9d059f5 100644 --- a/docs/users_guide/exts/types.rst +++ b/docs/users_guide/exts/types.rst @@ -22,6 +22,7 @@ Types type_applications rank_polymorphism impredicative_types + linear_types type_errors defer_type_errors roles |