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

Show
Ignore:
Timestamp:
06/17/11 15:44:18 (2 years ago)
Comment:

--

Unmodified
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.
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