6.4.21. Linear types¶
-
LinearTypes
¶ Implies: MonoLocalBinds
Since: 9.0.1 Status: Experimental Enable the linear arrow
a %1 -> b
and the multiplicity-polymorphic arrowa %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,
Limitations below. We encourage you to experiment
with this extension and report issues in the GHC
bug tracker, 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 %1 -> b
to mean that
f
is a linear function from a
to b
. If
UnicodeSyntax
is enabled, the %1 ->
arrow can be
written as ⊸
.
To allow uniform handling of linear a %1 -> b
and unrestricted a
-> b
functions, there is a new function type a %m -> b
.
Here, m
is a type of new kind Multiplicity
. We have:
data Multiplicity = One | Many -- Defined in GHC.Types
type a %1 -> b = a %One -> b
type a -> b = a %Many -> b
(See Datatype 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 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
. The same principle holds for
representation polymorphism (see Inference and defaulting).
6.4.21.1. Expressions¶
When defining a function either as a lambda \x -> u
or with
equations f x = u
, the multiplicity of the variable x
will be
inferred from the context. For equations, the context will typically
be a type signature. For instance here is a linear function
f :: (a -> b) %1 -> a -> b
f g x = g x
In this example, g
must be used linearly while x
is
unrestricted.
6.4.21.1.1. Bindings¶
Let and where bindings can be linear as well, the multiplicity of bindings is typically inferred
f :: A %1 -> B
g :: B %1 -> C
h :: A %1 -> C
h x = g y
where
y = f x
If you don’t want, or aren’t able, to rely on inference, let and where bindings can be annotated with a multiplicity
f :: A %1 -> B
g :: B %1 -> C
h :: A %1 -> C
h x = g y
where
%1 y = f x
The precise rules are, that you can annotate a binding with a multiplicity if:
- The binding is not top-level
- The binding is non-recursive
- The binding is a pattern binding (including a simple variable)
p=e
(you can’t writelet %1 f x = u
, instead writelet %1 f = \x -> u
) - Either
p
is strict (see infra) orp
is a variable. In particular neitherx@y
nor(x)
are covered by “is a variable”
When there’s no multiplicity annotation, the multiplicity is inferred as follows:
- Toplevel bindings are inferred as having multiplicity
Many
- Recursive bindings are inferred as having multiplicity
Many
- Lazy non-variable pattern bindings are inferred as having
multiplicity
Many
(note that in let- and where-bindings, patterns are lazy by default, so thatlet (x,y) = rhs
always have multiplicityMany
, whereaslet !(x,y) = rhs
can have multiplicity1
). - In all other cases, including function bindings
let f x1...xn = rhs
, the multiplicity is inferred from the term.
When -XMonoLocalBinds
is off, the following also holds:
- Multiplicity-annotated non-variable pattern-bindings (such as
let %1 !(x,y) = rhs
) are never generalised. - Non-variable pattern bindings which are inferred as polymorphic or
qualified are inferred as having multiplicity
Many
.
6.4.21.1.2. Strict patterns¶
GHC considers that non-variable lazy patterns consume the scrutinee
with multiplicity Many
. In practice, a pattern is strict (hence
can be linear) if (otherwise the pattern is lazy):
- The pattern is a case alternative and isn’t annotated with a
~
- The pattern is a let-binding, and is annotated with a
!
- The pattern is a let-binding,
Strict
is on, and isn’t annotated with a~
- The pattern is nested inside a strict pattern
Here are some examples of the impact on linear typing:
Without -XStrict
:
-- good
let %1 x = u in …
-- good
let %1 !x = u in …
-- bad
let %1 (x, y) = u in …
-- good
let %Many (x, y) = u in …
-- good
let %1 !(x, y) = u in …
-- good
let %1 (!(x, y)) = u in …
-- inferred unrestricted
let (x, y) = u in …
-- can be inferred linear
case u of (x, y) -> …
-- inferred unrestricted
case u of ~(x, y) -> …
- With
-XStrict
:: – good let %1 x = u in …
– good let %1 !x = u in …
– good let %1 (x, y) = u in …
– bad let %1 ~(x, y) = u in …
– good let %Many ~(x, y) = u in …
– can be inferred linear let (x, y) = u in …
– inferred unrestricted let ~(x, y) = u in …
6.4.21.2. 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 %1 -> T1 a
construct x = MkT1 x
deconstruct :: T1 a %1 -> 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
Inferred vs. specified type variables), 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 Printing multiplicity-polymorphic types);
therefore constructors appear to have regular function types.
mkList :: [a] -> [T1 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 %1 -> c %1 -> T2 a b c -- 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
.
It is also possible to define a multiplicity-polymorphic field:
data T3 a m where
MkT3 :: a %m -> T3 a m
While linear fields are generalized (MkT1 :: forall {m} a. a %m -> T1 a
in the previous example), multiplicity-polymorphic fields are not;
it is not possible to directly use MkT3
as a function a -> T3 a One
.
If 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.
6.4.21.3. Printing multiplicity-polymorphic types¶
If LinearTypes
is disabled, multiplicity variables in types are defaulted
to Many
when printing, in the same manner as described in Printing representation-polymorphic types.
In other words, without 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
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.)
6.4.21.4. Limitations¶
Linear types are still considered experimental and come with several limitations. If you have read the full design in the proposal (see Design and further reading below), here is a run down of the missing pieces.
- Multiplicity polymorphism is incomplete and experimental. You may have success using it, or you may not. Expect it to be really unreliable. (Multiplicity multiplication is not supported yet.)
- There is currently no support for multiplicity annotations on
function arguments such as
\(%p x :: a) -> ...
, only on let-bound variables. - A
case
expression may consume its scrutineeOne
time, orMany
times. But the inference is still experimental, and may over-eagerly guess that it ought to consume the scrutineeMany
times. - 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.
6.4.21.5. Design and further reading¶
- The design for this extension is described in details in the Linear types proposal
- This extension has been originally conceived of in the paper Linear Haskell: practical linearity in a higher-order polymorphic language (POPL 2018)
- There is a wiki page dedicated to the linear types extension