never executed always true always false
1 {-# LANGUAGE PatternSynonyms #-}
2
3 {-|
4 This module defines the semi-ring of multiplicities, and associated functions.
5 Multiplicities annotate arrow types to indicate the linearity of the
6 arrow (in the sense of linear types).
7
8 Mult is a type synonym for Type, used only when its kind is Multiplicity.
9 To simplify dealing with multiplicities, functions such as
10 mkMultMul perform simplifications such as Many * x = Many on the fly.
11 -}
12 module GHC.Core.Multiplicity
13 ( Mult
14 , pattern One
15 , pattern Many
16 , isMultMul
17 , mkMultAdd
18 , mkMultMul
19 , mkMultSup
20 , Scaled(..)
21 , scaledMult
22 , scaledThing
23 , unrestricted
24 , linear
25 , tymult
26 , irrelevantMult
27 , mkScaled
28 , scaledSet
29 , scaleScaled
30 , IsSubmult(..)
31 , submult
32 , mapScaledType) where
33
34 import GHC.Prelude
35
36 import GHC.Utils.Outputable
37 import GHC.Core.TyCo.Rep
38 import {-# SOURCE #-} GHC.Builtin.Types ( multMulTyCon )
39 import GHC.Core.Type
40 import GHC.Builtin.Names (multMulTyConKey)
41 import GHC.Types.Unique (hasKey)
42
43 {-
44 Note [Linear types]
45 ~~~~~~~~~~~~~~~~~~~
46 This module is the entry point for linear types.
47
48 The detailed design is in the _Linear Haskell_ article
49 [https://arxiv.org/abs/1710.09756]. Other important resources in the linear
50 types implementation wiki page
51 [https://gitlab.haskell.org/ghc/ghc/wikis/linear-types/implementation], and the
52 proposal [https://github.com/ghc-proposals/ghc-proposals/pull/111] which
53 describes the concrete design at length.
54
55 For the busy developer, though, here is a high-level view of linear types is the following:
56
57 - Function arrows are annotated with a multiplicity (as defined by type `Mult`
58 and its smart constructors in this module)
59 - Because, as a type constructor, the type of function now has an extra
60 argument, the notation (->) is no longer suitable. We named the function
61 type constructor `FUN`.
62 - (->) retains its backward compatible meaning: `(->) a b = a -> b`. To
63 achieve this, `(->)` is defined as a type synonym to `FUN Many` (see
64 below).
65 - Multiplicities can be reified in Haskell as types of kind
66 `GHC.Types.Multiplicity`
67 - Ground multiplicity (that is, without a variable) can be `One` or `Many`
68 (`Many` is generally rendered as ω in the scientific literature).
69 Functions whose type is annotated with `One` are linear functions, functions whose
70 type is annotated with `Many` are regular functions, often called “unrestricted”
71 to contrast them with linear functions.
72 - A linear function is defined as a function such that *if* its result is
73 consumed exactly once, *then* its argument is consumed exactly once. You can
74 think of “consuming exactly once” as evaluating a value in normal form exactly
75 once (though not necessarily in one go). The _Linear Haskell_ article (see
76 infra) has a more precise definition of “consuming exactly once”.
77 - Data types can have unrestricted fields (the canonical example being the
78 `Unrestricted` data type), then these don't need to be consumed for a value to
79 be consumed exactly once. So consuming a value of type `Unrestricted` exactly
80 once means forcing it at least once.
81 - Why “at least once”? Because if `case u of { C x y -> f (C x y) }` is linear
82 (provided `f` is a linear function). So we might as well have done `case u of
83 { !z -> f z }`. So, we can observe constructors as many times as we want, and
84 we are actually allowed to force the same thing several times because laziness
85 means that we are really forcing a the value once, and observing its
86 constructor several times. The type checker and the linter recognise some (but
87 not all) of these multiple forces as indeed linear. Mostly just enough to
88 support variable patterns.
89 - Multiplicities form a semiring.
90 - Multiplicities can also be variables and we can universally quantify over
91 these variables. This is referred to as “multiplicity
92 polymorphism”. Furthermore, multiplicity can be formal semiring expressions
93 combining variables.
94 - Contrary to the paper, the sum of two multiplicities is always `Many`. This
95 will have to change, however, if we want to add a multiplicity for 0. Whether
96 we want to is still debated.
97 - Case expressions have a multiplicity annotation too. A case expression with
98 multiplicity `One`, consumes its scrutinee exactly once (provided the entire
99 case expression is consumed exactly once); whereas a case expression with
100 multiplicity `Many` can consume its scrutinee as many time as it wishes (no
101 matter how much the case expression is consumed).
102
103 Note [Usages]
104 ~~~~~~~~~~~~~
105 In the _Linear Haskell_ paper, you'll find typing rules such as these:
106
107 Γ ⊢ f : A #π-> B Δ ⊢ u : A
108 ---------------------------
109 Γ + kΔ ⊢ f u : B
110
111 If you read this as a type-checking algorithm going from the bottom up, this
112 reads as: the algorithm has to find a split of some input context Ξ into an
113 appropriate Γ and a Δ such as Ξ = Γ + kΔ, *and the multiplicities are chosen to
114 make f and u typecheck*.
115
116 This could be achieved by letting the typechecking of `f` use exactly the
117 variable it needs, then passing the remainder, as `Delta` to the typechecking of
118 u. But what does that mean if `x` is bound with multiplicity `p` (a variable)
119 and `f` consumes `x` once? `Delta` would have to contain `x` with multiplicity
120 `p-1`. It's not really clear how to make that works. In summary: bottom-up
121 multiplicity checking forgoes addition and multiplication in favour of
122 subtraction and division. And variables make the latter hard.
123
124 The alternative is to read multiplicities from the top down: as an *output* from
125 the typechecking algorithm, rather than an input. We call these output
126 multiplicities Usages, to distinguish them from the multiplicities which come,
127 as input, from the types of functions. Usages are checked for compatibility with
128 multiplicity annotations using an ordering relation. In other words, the usage
129 of x in the expression u is the smallest multiplicity which can be ascribed to x
130 for u to typecheck.
131
132 Usages are usually group in a UsageEnv, as defined in the UsageEnv module.
133
134 So, in our function application example, the typechecking algorithm would
135 receive usage environements f_ue from the typechecking of f, and u_ue from the
136 typechecking of u. Then the output would be f_ue + (k * u_ue). Addition and
137 scaling of usage environment is the pointwise extension of the semiring
138 operations on multiplicities.
139
140 Note [Zero as a usage]
141 ~~~~~~~~~~~~~~~~~~~~~~
142 In the current presentation usages are not exactly multiplicities, because they
143 can contain 0, and multiplicities can't.
144
145 Why do we need a 0 usage? A function which doesn't use its argument will be
146 required to annotate it with `Many`:
147
148 \(x # Many) -> 0
149
150 However, we cannot replace absence with Many when computing usages
151 compositionally: in
152
153 (x, True)
154
155 We expect x to have usage 1. But when computing the usage of x in True we would
156 find that x is absent, hence has multiplicity Many. The final multiplicity would
157 be One+Many = Many. Oops!
158
159 Hence there is a usage Zero for absent variables. Zero is characterised by being
160 the neutral element to usage addition.
161
162 We may decide to add Zero as a multiplicity in the future. In which case, this
163 distinction will go away.
164
165 Note [Joining usages]
166 ~~~~~~~~~~~~~~~~~~~~~
167 The usage of a variable is defined, in Note [Usages], as the minimum usage which
168 can be ascribed to a variable.
169
170 So what is the usage of x in
171
172 case … of
173 { p1 -> u -- usage env: u_ue
174 ; p2 -> v } -- usage env: v_ue
175
176 It must be the least upper bound, or _join_, of u_ue(x) and v_ue(x).
177
178 So, contrary to a declarative presentation where the correct usage of x can be
179 conjured out of thin air, we need to be able to compute the join of two
180 multiplicities. Join is extended pointwise on usage environments.
181
182 Note [Bottom as a usage]
183 ~~~~~~~~~~~~~~~~~~~~~~
184 What is the usage of x in
185
186 case … of {}
187
188 Per usual linear logic, as well as the _Linear Haskell_ article, x can have
189 every multiplicity.
190
191 So we need a minimum usage _bottom_, which is also the neutral element for join.
192
193 In fact, this is not such as nice solution, because it is not clear how to
194 define sum and multiplication with bottom. We give reasonable definitions, but
195 they are not complete (they don't respect the semiring laws, and it's possible
196 to come up with examples of Core transformation which are not well-typed)
197
198 A better solution would probably be to annotate case expressions with a usage
199 environment, just like they are annotated with a type. Which, probably not
200 coincidentally, is also primarily for empty cases.
201
202 A side benefit of this approach is that the linter would not need to join
203 multiplicities, anymore; hence would be closer to the presentation in the
204 article. That's because it could use the annotation as the multiplicity for each
205 branch.
206
207 Note [Data constructors are linear by default]
208 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
209 Data constructors defined without -XLinearTypes (as well as data constructors
210 defined with the Haskell 98 in all circumstances) have all their fields linear.
211
212 That is, in
213
214 data Maybe a = Nothing | Just a
215
216 We have
217
218 Just :: a %1 -> Just a
219
220 The goal is to maximise reuse of types between linear code and traditional
221 code. This is argued at length in the proposal and the article (links in Note
222 [Linear Types]).
223
224 Note [Polymorphisation of linear fields]
225 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
226 The choice in Note [Data constructors are linear by default] has an impact on
227 backwards compatibility. Consider
228
229 map Just
230
231 We have
232
233 map :: (a -> b) -> f a -> f b
234 Just :: a %1 -> Just a
235
236 Types don't match, we should get a type error. But this is legal Haskell 98
237 code! Bad! Bad! Bad!
238
239 It could be solved with subtyping, but subtyping doesn't combine well with
240 polymorphism. Instead, we generalise the type of Just, when used as term:
241
242 Just :: forall {p}. a %p-> Just a
243
244 This is solely a concern for higher-order code like this: when called fully
245 applied linear constructors are more general than constructors with unrestricted
246 fields. In particular, linear constructors can always be eta-expanded to their
247 Haskell 98 type. This is explained in the paper (but there, we had a different
248 strategy to resolve this type mismatch in higher-order code. It turned out to be
249 insufficient, which is explained in the wiki page as well as the proposal).
250
251 We only generalise linear fields this way: fields with multiplicity Many, or
252 other multiplicity expressions are exclusive to -XLinearTypes, hence don't have
253 backward compatibility implications.
254
255 The implementation is described in Note [Typechecking data constructors]
256 in GHC.Tc.Gen.Head.
257
258 More details in the proposal.
259 -}
260
261 {-
262 Note [Adding new multiplicities]
263 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
264 To add a new multiplicity, you need to:
265 * Add the new type with Multiplicity kind
266 * Update cases in mkMultAdd, mkMultMul, mkMultSup, submult, tcSubMult
267 * Check supUE function that computes sup of a multiplicity
268 and Zero
269 -}
270
271 isMultMul :: Mult -> Maybe (Mult, Mult)
272 isMultMul ty | Just (tc, [x, y]) <- splitTyConApp_maybe ty
273 , tc `hasKey` multMulTyConKey = Just (x, y)
274 | otherwise = Nothing
275
276 {-
277 Note [Overapproximating multiplicities]
278 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
279 The functions mkMultAdd, mkMultMul, mkMultSup perform operations
280 on multiplicities. They can return overapproximations: their result
281 is merely guaranteed to be a submultiplicity of the actual value.
282
283 They should be used only when an upper bound is acceptable.
284 In most cases, they are used in usage environments (UsageEnv);
285 in usage environments, replacing a usage with a larger one can only
286 cause more programs to fail to typecheck.
287
288 In future work, instead of approximating we might add type families
289 and allow users to write types involving operations on multiplicities.
290 In this case, we could enforce more invariants in Mult, for example,
291 enforce that it is in the form of a sum of products, and even
292 that the sumands and factors are ordered somehow, to have more equalities.
293 -}
294
295 -- With only two multiplicities One and Many, we can always replace
296 -- p + q by Many. See Note [Overapproximating multiplicities].
297 mkMultAdd :: Mult -> Mult -> Mult
298 mkMultAdd _ _ = Many
299
300 mkMultMul :: Mult -> Mult -> Mult
301 mkMultMul One p = p
302 mkMultMul p One = p
303 mkMultMul Many _ = Many
304 mkMultMul _ Many = Many
305 mkMultMul p q = mkTyConApp multMulTyCon [p, q]
306
307 scaleScaled :: Mult -> Scaled a -> Scaled a
308 scaleScaled m' (Scaled m t) = Scaled (m' `mkMultMul` m) t
309
310 -- See Note [Joining usages]
311 -- | @mkMultSup w1 w2@ returns a multiplicity such that @mkMultSup w1
312 -- w2 >= w1@ and @mkMultSup w1 w2 >= w2@. See Note [Overapproximating multiplicities].
313 mkMultSup :: Mult -> Mult -> Mult
314 mkMultSup = mkMultMul
315 -- Note: If you are changing this logic, check 'supUE' in UsageEnv as well.
316
317 --
318 -- * Multiplicity ordering
319 --
320
321 data IsSubmult = Submult -- Definitely a submult
322 | Unknown -- Could be a submult, need to ask the typechecker
323 deriving (Show, Eq)
324
325 instance Outputable IsSubmult where
326 ppr = text . show
327
328 -- | @submult w1 w2@ check whether a value of multiplicity @w1@ is allowed where a
329 -- value of multiplicity @w2@ is expected. This is a partial order.
330
331 submult :: Mult -> Mult -> IsSubmult
332 submult _ Many = Submult
333 submult One One = Submult
334 -- The 1 <= p rule
335 submult One _ = Submult
336 submult _ _ = Unknown