Changes between Version 1 and Version 2 of Commentary/Compiler/SeqMagic


Ignore:
Timestamp:
Jun 17, 2011 10:44:18 PM (4 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Commentary/Compiler/SeqMagic

    v1 v2  
    11= Seq magic = 
    22 
    3 The innocent-looking `seq` operator causes all manner of mayhem in GHC. This page summarises the issues. 
     3The innocent-looking `seq` operator causes all manner of mayhem in GHC. This page summarises the issues.  See also discussion in Trac #5129. 
    44 
    55== The baseline position == 
     
    1717}}} 
    1818 
    19 == Problems == 
     19But this approach has problems; see `Note [Deguaring seq]` in `DsUtils`. 
    2020 
    21 Here are some of the problems that showed up.  See `Note [Deguaring seq]` in `DsUtils`. 
    22  
    23  
    24 Trac #1031.  Consider 
     21=== Problem 1 (Trac #1031) === 
     22Consider 
    2523{{{ 
    2624   f x y = x `seq` (y `seq` (# x,y #)) 
    2725}}} 
    28 The `[CoreSyn let/app invariant]` means that, other things being equal, because  
     26The `[CoreSyn let/app invariant]` (see `CoreSyn`) means that, other things being equal, because  
    2927the argument to the outer `seq` has an unlifted type, we'll use call-by-value thus: 
     28{{{ 
     29   f x y = case (y `seq` (# x,y #)) of v -> x `seq` v 
     30}}} 
     31But that is bad for two reasons:  
     32  * we now evaluate `y` before `x`, and  
     33  * we can't bind `v` to an unboxed pair 
    3034 
    31    f x y = case (y `seq` (# x,y #)) of v -> x `seq` v 
    32  
    33 But that is bad for two reasons:  
    34   (a) we now evaluate y before x, and  
    35   (b) we can't bind v to an unboxed pair 
    36  
    37 Seq is very, very special!  So we recognise it right here, and desugar to 
     35Seq is very, very special!  Treating it as a two-argument function, strict in 
     36both arguments, doesn't work. We "fixed" this by treating `seq` as a language 
     37construct, desugared by the desugarer, rather than as a function that may (or 
     38may not) be inlined by the simplifier.  So the above term is desugared to: 
    3839{{{ 
    3940        case x of _ -> case y of _ -> (# x,y #) 
    4041}}} 
    41 Note [Desugaring seq (2)]  cf Trac #2273 
    42 ~~~~~~~~~~~~~~~~~~~~~~~~~ 
     42 
     43=== Problem 2 (Trac #2273) === 
     44 
    4345Consider 
     46{{{ 
    4447   let chp = case b of { True -> fst x; False -> 0 } 
    4548   in chp `seq` ...chp... 
    46 Here the seq is designed to plug the space leak of retaining (snd x) 
     49}}} 
     50Here the `seq` is designed to plug the space leak of retaining `(snd x)` 
    4751for too long. 
    4852 
    49 If we rely on the ordinary inlining of seq, we'll get 
     53If we rely on the ordinary inlining of `seq`, we'll get 
     54{{{ 
    5055   let chp = case b of { True -> fst x; False -> 0 } 
    5156   case chp of _ { I# -> ...chp... } 
    52  
    53 But since chp is cheap, and the case is an alluring contet, we'll 
    54 inline chp into the case scrutinee.  Now there is only one use of chp, 
     57}}} 
     58But since `chp` is cheap, and the case is an alluring contet, we'll 
     59inline `chp` into the case scrutinee.  Now there is only one use of `chp`, 
    5560so we'll inline a second copy.  Alas, we've now ruined the purpose of 
    5661the seq, by re-introducing the space leak: 
     62{{{ 
    5763    case (case b of {True -> fst x; False -> 0}) of 
    5864      I# _ -> ...case b of {True -> fst x; False -> 0}... 
    59  
     65}}} 
    6066We can try to avoid doing this by ensuring that the binder-swap in the 
    6167case happens, so we get his at an early stage: 
     68{{{ 
    6269   case chp of chp2 { I# -> ...chp2... } 
     70}}} 
    6371But this is fragile.  The real culprit is the source program.  Perhaps we 
    6472should have said explicitly 
     73{{{ 
    6574   let !chp2 = chp in ...chp2... 
    66  
    67 But that's painful.  So the code here does a little hack to make seq 
    68 more robust: a saturated application of 'seq' is turned *directly* into 
     75}}} 
     76But that's painful.  So the desugarer does a little hack to make `seq` 
     77more robust: a saturated application of `seq` is turned '''directly''' into 
    6978the case expression, thus: 
     79{{{ 
    7080   x  `seq` e2 ==> case x of x -> e2    -- Note shadowing! 
    7181   e1 `seq` e2 ==> case x of _ -> e2 
    72  
     82}}} 
    7383So we desugar our example to: 
     84{{{ 
    7485   let chp = case b of { True -> fst x; False -> 0 } 
    7586   case chp of chp { I# -> ...chp... } 
     87}}} 
    7688And now all is well. 
    7789 
    78 The reason it's a hack is because if you define mySeq=seq, the hack 
    79 won't work on mySeq.   
     90Be careful not to desugar 
     91{{{ 
     92   True `seq` e  ==> case True of True { ... } 
     93}}} 
     94which stupidly tries to bind the datacon 'True'. This is easily avoided. 
    8095 
    81 Note [Desugaring seq (3)] cf Trac #2409 
    82 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
    83 The isLocalId ensures that we don't turn  
    84         True `seq` e 
    85 into 
    86         case True of True { ... } 
    87 which stupidly tries to bind the datacon 'True'.  
     96The whole thing is a hack though; if you define `mySeq=seq`, the hack 
     97won't work on `mySeq`.   
    8898 
    89 === The need for special rules === 
     99=== Problem 3 (Trac #5262) === 
     100 
     101Consider 
     102{{{ 
     103  f x = x `seq` (\y.y) 
     104}}} 
     105With the above desugaring we get 
     106{{{ 
     107  f x = case x of x { _ -> \y.y } 
     108}}} 
     109and now ete expansion gives 
     110{{{ 
     111  f x y = case x of x { _ -> y } 
     112}}} 
     113Now suppose that we have 
     114{{{ 
     115       f (length xs) `seq` 3 
     116}}} 
     117Plainly `(length xs)` should be evaluated... but it isn't because `f` has arity 2. 
     118(Without -O this doesn't happen.) 
     119 
     120=== Problem 4: seq in the IO monad == 
     121 
     122See the extensive discussion in Trac #5129. 
     123 
     124=== Problem 5: the need for special rules === 
    90125 
    91126Roman found situations where he had 
     
    102137enough support that you can do this using a rewrite rule: 
    103138{{{ 
    104   RULE "f/seq" forall n.  seq (f n) e = seq n e 
     139  RULE "f/seq" forall n e.  seq (f n) e = seq n e 
    105140}}} 
    106141You write that rule.  When GHC sees a case expression that discards 
     
    112147into a case expression on the LHS of a rule. 
    113148 
    114 To increase applicability of these user-defined rules, we also have the following built-in rule for `seq` 
     149To increase applicability of these user-defined rules, we also 
     150have the following built-in rule for `seq`  
    115151{{{ 
    116152  seq (x |> co) y = seq x y 
     
    124160 
    125161 
     162= A better way = 
     163 
     164Here's our new plan.  
     165 * Introduce a new primop `seq# :: a -> State# s -> (# a, State# s #)` 
     166 * An application of the primop is not considered cheap. 
     167 * Desugar `seq` thus: 
     168{{{ 
     169   x  `seq` e2 ==> case seq# x RW of (# x, _ #) -> e2    -- Note shadowing! 
     170   e1 `seq` e2 ==> case seq# x RW of (# _, _ #) -> e2 
     171}}} 
     172 * Define `evaluate` thus 
     173{{{ 
     174  evaluate :: a -> IO () 
     175  evaluate x = IO (\s -> case seq# x s of 
     176                           (# _, s' #) -> (# (), s' #) 
     177}}} 
     178 
     179All the same equations hold as with the old defn for `seq`, but the problems 
     180go away: 
     181  * Problem 1: (seq x y) is elaborated in the desugarer 
     182  * Problem 2: problem largely unaffected 
     183  * Problem 3: if we regard `(seq# a b)` as expensive, we won't eta expand. 
     184  * Problem 4: unchanged