Linear types: projections of records
Currently, record selectors are always non-linear functions.
data P a b = P { p1 :: a, p2 :: b }
p1 :: P a b -> a
p2 :: P a b -> b
However, if a record contains only one field, we can make the projection function linear. This is especially useful for newtypes:
newtype N = N { unN :: A }
unN :: N -> A -- could be N #-> A
-- but because of backwards compat, we must use forall {m}. N # m -> A
This is similar to constructors being multiplicity polymorphic.
Once we have syntax for multiplicity in record fields #18462, this can apply more generally to records where all fields except one are unrestricted, e.g. in data R = R { unrestrictedField # 'Many :: A, linearField # 'One :: B }
the linearField
projection can be linear.
This is not completely trivial to implement - it changes the output in TH (T11103), interacts with overloaded record fields. The case
in the definition of unN
in Core needs to be case[1]
, while the current method uses case[Many]
. My old (not working) attempt is at https://github.com/tweag/ghc/commit/5cdd5893570d694056c9f1717d8bb77191601a43.