Context Navigation

SeqMagic

Timestamp:: 06/17/11 15:44:18 (2 years ago)
Author:: simonpj
Comment:: --

Legend:

: Unmodified
: Added
: Removed
: Modified

Commentary/Compiler/SeqMagic

v1	v2
1	1	= Seq magic =
2	2
3		The innocent-looking `seq` operator causes all manner of mayhem in GHC. This page summarises the issues.
	3	The innocent-looking `seq` operator causes all manner of mayhem in GHC. This page summarises the issues. See also discussion in Trac #5129.
4	4
5	5	== The baseline position ==
…	…
17	17	}}}
18	18
19		== Problems ==
	19	But this approach has problems; see `Note [Deguaring seq]` in `DsUtils`.
20	20
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) ===
	22	Consider
25	23	{{{
26	24	f x y = x `seq` (y `seq` (# x,y #))
27	25	}}}
28		The `[CoreSyn let/app invariant]` means that, other things being equal, because
	26	The `[CoreSyn let/app invariant]` (see `CoreSyn`) means that, other things being equal, because
29	27	the 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	}}}
	31	But that is bad for two reasons:
	32	* we now evaluate `y` before `x`, and
	33	* we can't bind `v` to an unboxed pair
30	34
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
	35	Seq is very, very special! Treating it as a two-argument function, strict in
	36	both arguments, doesn't work. We "fixed" this by treating `seq` as a language
	37	construct, desugared by the desugarer, rather than as a function that may (or
	38	may not) be inlined by the simplifier. So the above term is desugared to:
38	39	{{{
39	40	case x of _ -> case y of _ -> (# x,y #)
40	41	}}}
41		Note [Desugaring seq (2)] cf Trac #2273
42		~~~~~~~~~~~~~~~~~~~~~~~~~
	42
	43	=== Problem 2 (Trac #2273) ===
	44
43	45	Consider
	46	{{{
44	47	let chp = case b of { True -> fst x; False -> 0 }
45	48	in chp `seq` ...chp...
46		Here the seq is designed to plug the space leak of retaining (snd x)
	49	}}}
	50	Here the `seq` is designed to plug the space leak of retaining `(snd x)`
47	51	for too long.
48	52
49		If we rely on the ordinary inlining of seq, we'll get
	53	If we rely on the ordinary inlining of `seq`, we'll get
	54	{{{
50	55	let chp = case b of { True -> fst x; False -> 0 }
51	56	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	}}}
	58	But since `chp` is cheap, and the case is an alluring contet, we'll
	59	inline `chp` into the case scrutinee. Now there is only one use of `chp`,
55	60	so we'll inline a second copy. Alas, we've now ruined the purpose of
56	61	the seq, by re-introducing the space leak:
	62	{{{
57	63	case (case b of {True -> fst x; False -> 0}) of
58	64	I# _ -> ...case b of {True -> fst x; False -> 0}...
59
	65	}}}
60	66	We can try to avoid doing this by ensuring that the binder-swap in the
61	67	case happens, so we get his at an early stage:
	68	{{{
62	69	case chp of chp2 { I# -> ...chp2... }
	70	}}}
63	71	But this is fragile. The real culprit is the source program. Perhaps we
64	72	should have said explicitly
	73	{{{
65	74	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	}}}
	76	But that's painful. So the desugarer does a little hack to make `seq`
	77	more robust: a saturated application of `seq` is turned '''directly''' into
69	78	the case expression, thus:
	79	{{{
70	80	x `seq` e2 ==> case x of x -> e2 -- Note shadowing!
71	81	e1 `seq` e2 ==> case x of _ -> e2
72
	82	}}}
73	83	So we desugar our example to:
	84	{{{
74	85	let chp = case b of { True -> fst x; False -> 0 }
75	86	case chp of chp { I# -> ...chp... }
	87	}}}
76	88	And now all is well.
77	89
78		The reason it's a hack is because if you define mySeq=seq, the hack
79		won't work on mySeq.
	90	Be careful not to desugar
	91	{{{
	92	True `seq` e ==> case True of True { ... }
	93	}}}
	94	which stupidly tries to bind the datacon 'True'. This is easily avoided.
80	95
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'.
	96	The whole thing is a hack though; if you define `mySeq=seq`, the hack
	97	won't work on `mySeq`.
88	98
89		=== The need for special rules ===
	99	=== Problem 3 (Trac #5262) ===
	100
	101	Consider
	102	{{{
	103	f x = x `seq` (\y.y)
	104	}}}
	105	With the above desugaring we get
	106	{{{
	107	f x = case x of x { _ -> \y.y }
	108	}}}
	109	and now ete expansion gives
	110	{{{
	111	f x y = case x of x { _ -> y }
	112	}}}
	113	Now suppose that we have
	114	{{{
	115	f (length xs) `seq` 3
	116	}}}
	117	Plainly `(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
	122	See the extensive discussion in Trac #5129.
	123
	124	=== Problem 5: the need for special rules ===
90	125
91	126	Roman found situations where he had
…	…
102	137	enough support that you can do this using a rewrite rule:
103	138	{{{
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
105	140	}}}
106	141	You write that rule. When GHC sees a case expression that discards
…	…
112	147	into a case expression on the LHS of a rule.
113	148
114		To increase applicability of these user-defined rules, we also have the following built-in rule for `seq`
	149	To increase applicability of these user-defined rules, we also
	150	have the following built-in rule for `seq`
115	151	{{{
116	152	seq (x \|> co) y = seq x y
…	…
124	160
125	161
	162	= A better way =
	163
	164	Here'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
	179	All the same equations hold as with the old defn for `seq`, but the problems
	180	go 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