Does this mean that

f :: ()
f = let t = undefined :: (# () #)
    in ()

would still diverge (because t is of unlifted type), while

g :: ()
g = let (# u #) = undefined :: (# () #)
    in ()

would now evaluate to () (because u is of lifted type)?

@rwbarton , yes, precisely.

It also means that

z = ()
  where _ = undefined :: Int#

will evaluate to () while

z = ()
  where _x = undefined :: Int#

will throw an exception.

However, this kind of silliness is present in GHC 8. If we have

data T = K Int# Int

and then say

y = ()
  where K _ _x = undefined

we can evaluate y to (). But if I say

y = ()
  where K _z _x = undefined

now I get an error saying I should bang the pattern. Under this proposal, I would get the unbanged-strict-patterns warning in this last example, but then y would throw an exception when evaluated.

My z example above makes me think we should require the bang even on bare variables, but that would break a lot of code I think.

To be clear, an "unlifted id", in the definition of an "unlifted bind", is an freshly-bound identifier whose type is unlifted, right?

Also, might "unlifted pattern" be a better term than "unlifted bind"? IIUC the single where clause in

foo = ()
  where (# #) = undefined

would be affected by this (would evaluate to () instead of throwing an exception), yet contains no bindings.

I like both parts of this proposal. It's a dark corner, and we should strive for simplicity in the specification. This does exactly that.

Clarified points as requested by @Ericson2314 , who is right on both counts.

I actually like it that unboxed tuple bindings are strict (even though it was probably accidental) because it matches my intuition that every unlifted binding is strict. It feels like a special case to make unboxed tuple bindings lazy. Do we have a compelling use case for this, or is it just that (a) it's easy and (b) it's slightly more general? It might lead to less efficient code in some cases, and if someone is using unboxed tuples they probably care about performance.

It would be nice if ~ could be used to make an unboxed tuple binding lazy.

By all means make the error about nonbanged strict patterns into a warning. I'm not sure why it was made an error, but we did go through a series of changes where it was originally made a warning and then an error, and I recall a lot of churn particularly with making code work across multiple GHC versions.

This is tricky stuff to specify, and the proposal still isn't very clear.

The proposal say "Define an "unlifted pattern" to be any pattern that binds variable with an unlifted type.". That's good.

Then it uses the term "strict pattern"; I think that's precisely the same as "unlifted pattern", but I'm not sure. I'll stick to "unlifted pattern" alone.

Now, a binding p = e, where p is an unlifted pattern, must compile to a case expression. That means:

• It must not be top-level
• It must not be recursive
• It must not be polymorphic or overloaded

So it's pretty restrictive.

Define a "banged binding" to be one of form !p = e. A banged binding cannot be top-level, but it can be recursive, polymorphic, or overloaded. Why? See the FORCE rule in Section 9.28.4 of the manual: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#dynamic-semantics-of-bang-patterns. To take a recursive example, the binding

let ![x,y] = f x y z in blah

desugars to

let t = case f x y z of [x,y] -> (x,y)
    x = case t of (x,y) -> x
    y = case t of (x,y) -> y
in t `seq` blah

This might diverge; but it also might not. The banged binding means that before evaluating blah we seq on a full match of the banged pattern.

OK, having set the scene, what about unboxed tuple bindings?

(# x,y #) = e

We could:

1. Treat them uniformly (this is Richard's proposal)
2. Treat them like a banged binding
3. Treat them like a unlifted pattern binding.

Richard's proposal is (1). It's unclear whether Simon M is suggesting (2) or (3). I think (2) would be better: it is more expressive, but in the common case of a non-recursive binding you get the case expression you probably expected. But I suppose we could chose (3).

There are no technical issues at stake here; it's a free stylistic choice.

Simon, in point (3) I think you meant "unlifted pattern" rather than "strict pattern", correct?

So yes, I was thinking of (3), I hadn't considered (2). (3) seems simpler (to me), because it desugars directly to the case expression rather than requiring subsequent optimisations, but (2) is more expressive. I don't feel very strongly about any of this, but it does seem intuitive to me to treat an unboxed tuple binding like other unlifted pattern bindings.

in point (3) I think you meant "unlifted pattern" rather than "strict pattern", correct?

Yes! I've updated my comment. Sorry.

It would be nice if ~ could be used to make an unboxed tuple binding lazy.

Since "~" cancels "!", that desire would be uniformly supported with (2); but not with (3). So that argues for (2)

Sorry for being a bit loose with the terms. (perhaps "unlifted pattern" is an unfortunate terminology since it doesn't mean that the pattern is unlifted. How about "unlifted-variable pattern"?)

Note that this proposal is now half-way through its four week discussion period. At the end of this period we ask @goldfirere to summarize the discussion and bring the proposal to the GHC committee for consideration. Thanks!

This proposal has not attracted discussion for a while. Please consider submitting it to the Committee for discussion, if you think it is ready, or close it, if you have abandoned this proposal.

Another ping. @goldfirere, whither this proposal?

Oops. I missed the first ping. I will update this proposal with respect to recent commentary and then submit for a decision.

@goldfirere Another ping about this proposal… :-)

I have updated the proposal to incorporate feedback here. I would like to submit this for a decision, @nomeata.

For the intermediate proposal, can we also have let 3# = 4# in () diverge, but let ~3# = 4# in () evaluate to ()? Then the intermediate proposal only depends on whether the type of the pattern is lifted, not anything to do with the binding of variables.

Philosophically, I see as the lazy matching of unlifted types as a sort of "static laziness". With this static laziness, the compiler is allowed to delay evaluation (or perhaps more broadly rewrite the term just worrying about preserving semantics in the case that the bound expression terminates) as long as no new thunking or boxing is introduced.

@goldfirere's variable binding rule is somewhat a special case of this principle where, because of the lack of unlifted bindings with the pattern, thunks are "already available" for every possible data dependency with the potential to force the match.

Oh, I missed that this was submitted for review… will act immediately.

I tend to agree with @simonmar that we should do what is best for performance, which is where we need explicit use of unboxed tuples. But ... I guess there's some performance risk to going too strict by default as it might introduce extra "thunk-evaluated?" checks in scenarios where we know the thunks are already evaluated?

I wish there were a simple rule like if a pattern variable binds Int#, it needs !. Or that they never do. Personally, I'm not really a fan of having bangs on unlifted-bindings, because I wanted to think of bangs, operationally, as forcing thunks just like seq. In the case of unlifted-primitive-bindings they're not doing that, they're just documenting something you already know: that Int# is unlifted.

@goldfirere, I'd like to reply here to some of the text in the proposal:

requiring bangs on unboxed tuple patterns that bind a variable of an unlifted type

Wait, does this language mean that we could need double bangs to avoid warnings? !(# !a, !b #)?

Again, I believe we want to generate the strict behavior by default most of the time. That is, that we don't want to make it easy for the user to accidentally generate this code shown in the manual:

f x = let t = case h x of { (# p,q #) -> (p,q) }
          p = fst t
          q = snd t
      in ..body..

Almost always, when I'm mucking with unboxed tuples because I'm explicitly trying to squeeze the allocation out of a loop. This terrible code above would reintroduce mystery thunk allocations (for p and q) and destroy the performance of my loop in a way that causes me to do that much more digging around in the -ddump'd Core and STG.

I'm using unboxed tuples to get away from boxed tuples -- reintroducing boxed tuples implicitly is cruel!

So that leads me to want to leave laziness as "opt in" rather than "opt out". But there are two distinct ways to accomplish that. One is the "option (2)" above, which is described in the Alternatives section of the proposal as:

There is also a middle ground for (A) around unboxed tuples: we could pretend they always have a bang on them.

Ok, that's fine. And @simonmar and @simonpj seem to be at-least-not-opposed to it.

An add-on to that idea seems to be to issue warnings when any unboxed tuple binding lacks the bang, just like we do for other unlifted-type variable bindings in patterns.

Uh, except this bumps up against the fact that we are not uniform in requiring "pattern variables of unlifted types should have a bang" (e.g. !x :: Int#), because we require that for nested fields but not for top-level bindings. So doing the "same" thing as we do for Int# would mean that we issue a warning if there is no bang on "inner" unboxed-tuple patterns, but not at the top-level? (But we would still then interpret the top-level one as having an implicit bang?)

The good thing is that the meaning with the ! or with the ~ is clear, its just the interpretation of patterns without them that's very confusing.

@goldfirere - Do all the discussed designs satisfy these two "theorems"?:

• If there is textually a ! in a pattern, then the pattern binding introduces at least some evaluation (at least one case expr, though it may be nested).
• If there is textually a ~ in a pattern, then the pattern binding introduces code for at least one thunk allocation (though it may be optimized away).

I will number your theorems (A) and (B).

(A) is not true today, and this proposal does not change that fact. Counterexample: let (!x, !y) = (undefined, undefined) in () evaluates to ().

(B) is true today and with this proposal.

I don't believe my proposal gets near to these theorems. The more interesting space (which my proposal does affect) is what happens when there is no bang or twiddle.

I agree with @rrnewton, making an unboxed tuple binding lazy by default seems to be intuitively the wrong choice. I guarantee I would get tripped up by this! Giving unboxed tuples an implicit bang seems reasonable to me.

I am also worried about existing code. People that do careful tricks with unboxed tuples probably require the particular semantics that GHC currently does (and they probably didn’t read the manual :-)). Since evaluation order is not something that is captured by our types, changing something here might cause hard-to-track-down bugs somewhere. I would expect (without looking) that ghc-heap-view would break.

Is there a good example why the documented behavior is actually better than the implementation? I.e. a use-case?

Otherwise I’d be inclined to just update the manual to reflect reality that suited our users for several years, and consider it a bug in the manual, not the code :-)

Catching up on this again, I mis-read the proposal. Could you add to the proposal something about desugaring? That is, you propose that

(# a, Just b #) = e

desguars to

t = case e of (# a, Just b #) -> (a,b)
a = fst t
b = snd t

I was worried about having a thunk with unboxed-tuple type; but in the desugaring we see that all thunks have lifted types.

As to an implicit bang on outermost unboxed tuples, I defer to users. It's a free choice. I agree that making an unboxed tuple lazy (and making the desugaring create a boxed tuple) might be unexpected.

Since this is implemented, should this PR have the "Implemented" label added?