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