LinearTypes

Since: 9.0.1 Enable the linear arrow
a %1 > b
and the multiplicitypolymorphic 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 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  Patternmatching 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 multiplicitypolymorphic 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 multiplicitypolymorphic 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
.
6.4.17.1. 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 multiplicitypolymorphic 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 multiplicitypolymorphic 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 multiplicitypolymorphic 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), multiplicitypolymorphic 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.17.2. Printing multiplicitypolymorphic types
If LinearTypes
is disabled, multiplicity variables in types are defaulted to Many
when printing, in the same manner as described in Printing representationpolymorphic types. In other words, without LinearTypes
, multiplicitypolymorphic functions a %m > b
are printed as normal Haskell2010 functions a > b
. This allows existing libraries to be generalized to linear types in a backwardscompatible 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.17.3. 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 such as
x :: a %p
,\(x :: a %p) > ...
.  A
case
expression may consume its scrutineeOne
time, orMany
times. But the inference is still experimental, and may overeagerly guess that it ought to consume the scrutineeMany
times. All
let
andwhere
statements consume their right hand sideMany
times. That is, the following will not type check:g :: A %1 > (A, B) h :: A %1 > B %1 > C f :: A %1 > C f x = let (y, z) = g x in h y z
This can be worked around by defining extra functions which are specified to be linear, such as:
g :: A %1 > (A, B) h :: A %1 > B %1 > C f :: A %1 > C f x = f' (g x) where f' :: (A, B) %1 > 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 multiplicitypolymorphic; currently it’s unrestricted.
 Attempting to use of linear types in Template Haskell will probably not work.
6.4.17.4. 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 higherorder polymorphic language (POPL 2018)
 There is a wiki page dedicated to the linear types extension