GHC: Ticket #2806: Require bang-patterns for unlifted bindings
http://ghc.haskell.org/trac/ghc/ticket/2806
<p>
GHC allows let/where bindings for unlifted values, but they are necessarily <em>strict</em>. That does lead to confusing behaviour. For example, 'f' and 'g' behave differently here:
</p>
<pre class="wiki"> {-# LANGUAGE MagicHash #-}
import GHC.Base
import GHC.Exts
main :: IO ()
main = do print (I# (f 5# 0#))
print (I# (g 4# 0#))
f :: Int# -> Int# -> Int#
f x y | False = x `divInt#` y
f x y = x
g :: Int# -> Int# -> Int#
g x y | False = z
where z = x `divInt#` y
g x y = x
</pre><p>
Suggestion: require that an unlifted let/where binding has a bang on it. That would make lifted and unlifted bindings behave uniformly.
</p>
<p>
Simon
</p>
en-usGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/ticket/2806
Trac 1.0.1guestTue, 25 Nov 2008 16:48:33 GMTcc set
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:1
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:1
<ul>
<li><strong>cc</strong>
<em>id@…</em> added
</li>
</ul>
<p>
I concur. -Isaac D.
</p>
TicketPHOFri, 28 Nov 2008 04:13:12 GMTcc changed
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:2
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:2
<ul>
<li><strong>cc</strong>
<em>pho@…</em> added
</li>
</ul>
TicketiglooSat, 11 Apr 2009 01:10:57 GMTmilestone changed
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:3
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:3
<ul>
<li><strong>milestone</strong>
changed from <em>6.12 branch</em> to <em>6.12.1</em>
</li>
</ul>
TicketsimonpjTue, 21 Apr 2009 15:46:38 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:4
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:4
<p>
Just to record an email exchange.
</p>
<p>
Ian Lynagh:
</p>
<pre class="wiki">It looks like TcBinds.checkStrictBinds is the place to do it.
If we have where clauses
where (b, I# a) = ...
where (b, I# !a) = ...
then we respectively get
mbind = <(b, GHC.Types.I# a) = ...>
mbind = <(b, GHC.Types.I# !a) = ...>
mono_tys = [(), GHC.Prim.Int#]
mono_tys = [(), GHC.Prim.Int#]
but where I get stuck is trying to match up the types with the bangs (or
lack of bangs). One option would be to walk over mbind, but that feels
rather hackish - especially as it's a bag rather than a list! Another
might be to put a boolean for the presence or absence of a bang in the
MonoBindInfo, and then to pair it with the type when making mono_tys.
</pre><p>
Simon PJ replies:
</p>
<pre class="wiki">| It looks like TcBinds.checkStrictBinds is the place to do it.
I agree.
| If we have where clauses
| where (b, I# a) = ...
| where (b, I# !a) = ...
Whoa! I think this is *not* what's proposed. Suppose we have
let (x, !y) = e in ...
This is *not* evaluated strictly. Rather, if 'x' is evaluated,
the pattern is matched, and hence y is evaluated at that moment.
Similarly if 'y' is evaluated, but that makes no difference.
Having a bang on the 'y' doesn't force strict evaluation of the pattern.
In contrast, if we have
let (x, I# y) = e in ..
then we *must* evaluate the whole let strictly (because y:Int#)
so we demand a bang on the whole pattern not on the 'y'.
So we should have written
let !(x, I# y) = in in ...
</pre><p>
Ian says:
</p>
<pre class="wiki">Oh, wow, you are right. So lifted and unlifted bindings wouldn't behave
uniformly after all:
foo1 = 'a'
where !(x, ~(y, !z)) = ('x', ('y', 1 `div` 0))
foo2 = 'a'
where !(x, ~(y, I# z)) = ('x', ('y', 1 `div` 0))
foo1 == 'a', but foo2 == _|_
Even more distressing is:
foo3 = 'a'
where !(x, ~(!y, !z)) = ('x', (1 `div` 0, (3 :: Int)))
foo4 = 'a'
where !(x, ~(!y, I# z)) = ('x', (1 `div` 0, (3 :: Int)))
Again foo3 == 'a' and foo4 == _|_, but in this case it is the evaluation
of !y that is the source of the _|_.
So perhaps ~p, where p contains an unlifted variable, should be rejected
too?
</pre><p>
Simon says
</p>
<pre class="wiki">Yes, absolutely it should. Let's do that at the same time.
I'm not 100% sure where the best place is. Presumably in TcPat, since
\~(x, I# y) -> ...
should also be rejected.
But when checking a ~pattern, we don't have conveniently to hand
the variables bound.
I suspect the easiest thing is going to be in
tc_pat (LazyPat ...)
to do (getPatBinders pat') and check for un-lifted types.
</pre>
TicketguestTue, 21 Apr 2009 19:35:05 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:5
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:5
<p>
In "<tt>where (I# z) = ...</tt>", where are bangs needed? Is "<tt>where !(I# z) = ...</tt>" sufficient, or is "<tt>where !(I# !z) = ...</tt>" required? My intuition suggests to only require that latter bang in the data-definition, not the pattern-match (to require "<tt>data Int = I# !Int#</tt>")... does that make sense?
</p>
<p>
-Isaac Dupree
</p>
TicketiglooTue, 21 Apr 2009 22:22:02 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:6
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:6
<p>
Right, if a pattern contains a binder with an unlifted type, then you need an outermost ! (to negate the implicit ~), and the binder needs to not be (directly or indirectly) inside an explicit ~.
</p>
TicketguestWed, 22 Apr 2009 01:08:35 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:7
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:7
<p>
darn, I (Isaac) realized that what I said was really ambiguous. I'll try with simpler examples:
</p>
<p>
Perhaps
</p>
<pre class="wiki">f (I# z) = ...
</pre><p>
ought not to require a bang on the "z", because the data-type is inherently strict.
</p>
<p>
And to make it clear, another example of this logic is that this would be okay (but needs that bang) :
</p>
<pre class="wiki">g (x, !(I# z)) = ...
</pre><p>
But, I forget the semantics of bang-patterns... would this also be equivalent and permissible?:
</p>
<pre class="wiki">g (x, (I# !z))
</pre><p>
Anyway, if we allow "f" above (or even if not?), I would be more comfortable with -- by analogy -- requiring a bang in any data-type definition where an unlifted type is contained, rather than leaving that form of strictness implied. (In the presence of type-synonyms, it may not always be obviously visible to the reader whether a member type is unlifted.) This makes a difference in currently-allowed expressions like <tt>I# ( 1# +# 1# )</tt> or <tt>I# ( 1# </tt>quot#<tt> 0# )</tt> which would "normally" be lazy as long as there isn't a bang in the data definition of Int (but is strict because of unlifted semantic magic).
</p>
TicketsimonpjWed, 22 Apr 2009 08:52:34 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:8
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:8
<p>
We're getting ourselves confused here. In the rest of this comment I'll write down a more formal account of what I think The Rules should be. If we can agree them, then we can implement them and put them in the user manual.
</p>
<p>
First, let's agree that the semantics of bang patterns is defined here:
</p>
<ul><li><a href="http://www.haskell.org/ghc/docs/latest/html/users_guide/bang-patterns.html">http://www.haskell.org/ghc/docs/latest/html/users_guide/bang-patterns.html</a>
</li></ul><p>
This ticket is concerned with patterns that bind variables of unlifted type (e.g. <tt>Int#</tt>). I propose the following rule:
</p>
<ul><li>A pattern <tt>p</tt> is <strong>strict down to</strong> <tt>v</tt> iff <tt>v</tt> does not appear under a lazy-pattern tilde "<tt>~</tt>".
</li></ul><ul><li>A variable <tt>v</tt> of unlifted type may be bound by a pattern only in the following situations:
<ul><li>In a lambda or <tt>case</tt>, only by a pattern that is strict down to <tt>v</tt>.
</li><li>In a <tt>let</tt> or <tt>where</tt>, only by a binding <tt>!p = e</tt> where <tt>p</tt> is strict down to <tt>v</tt>.
</li></ul></li></ul><p>
Rationale: variables of unlifted type cannot be bound to a thunk, so the pattern must eagerly match all the way down to <tt>v</tt>.
</p>
<p>
Examples. Suppose <tt>v::Int#</tt>. Then here are some legal bindings:
</p>
<pre class="wiki">\v -> e
\(x, I# v) -> e
let !v = e in b
let !(x, I# v) = e in b
\(x, !(I# v)) -> e -- The inner ! is legal but not required
\(x, I# !v) -> e -- The ! on v is legal but not required
</pre><p>
Here are some illegal ones
</p>
<pre class="wiki">\~(I# v) -> e -- Under a tilde
let I# v = e in b -- No bang on the pattern binding
let !(x, ~(I# v)) = e in b -- Under a tilde
</pre>
TicketguestWed, 22 Apr 2009 13:27:56 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:9
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:9
<p>
You're quite right, I was getting myself confused. Really confused actually. I agree that (1) something at least as strict (limiting) as simonpj's rule should be adopted and (2) that simonpj's rule solves a specific existing problem which appears to be the intended focus of this ticket.
</p>
TicketguestWed, 22 Apr 2009 13:54:55 GMT
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:10
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:10
<p>
My more disruptive wish involved:
</p>
<pre class="wiki">type I = Int# --or I = Int. Defined in some other module.
f :: I -> I -> I
f a b = a -- "f !a !b = a" could be required if I = Int#
g :: ... -> I
g ... = f (some_complex_computation_1) (some_complex_computation_2)
</pre><p>
I'm unhappy that GHC has the feature for an unlifted type to change the strictness/space-complexity of unsuspecting functions: a change that lifted and non-built-in types cannot ever bring about even if you wished them to. I noticed this when looking at GHC's "<a class="missing wiki">FastInt?</a>" code that abstracts away from <tt>Int#</tt> slightly (I think it abstracts for historical/potential portability. Admittedly, I think GHC is also the only compiler that supports bang-patterns, currently?)
</p>
<p>
I guess there is also the intermediate (and annoying) option of a warning-flag rather than errors or nothing :-)
</p>
<p>
-Isaac Dupree
</p>
TicketiglooThu, 23 Apr 2009 00:09:18 GMTowner set
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:11
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:11
<ul>
<li><strong>owner</strong>
set to <em>igloo</em>
</li>
</ul>
TicketiglooFri, 05 Jun 2009 15:57:09 GMTstatus changed; testcase, resolution set
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:12
http://ghc.haskell.org/trac/ghc/ticket/2806#comment:12
<ul>
<li><strong>status</strong>
changed from <em>new</em> to <em>closed</em>
</li>
<li><strong>testcase</strong>
set to <em>T2806</em>
</li>
<li><strong>resolution</strong>
set to <em>fixed</em>
</li>
</ul>
<p>
Now completed, documented, and a test added. I've also opened <a class="closed ticket" href="http://ghc.haskell.org/trac/ghc/ticket/3278" title="bug: Make lazy unlifted bindings an error (closed: wontfix)">#3278</a> to remind us to make it an error, rather than a warning, in GHC 6.14.
</p>
Ticket