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