Note [Data constructors are linear by default]
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
data Maybe a = Nothing | Just a
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. References 0
This Note does not link to any other.
Referenced by 3
- Polymorphisation of linear fields GHC.Core.Multiplicity
- Linear types GHC.Core.Multiplicity
- GHC.Core.Unify call site