I think this is the consistent way to interpret your rule (1) that unlifted bindings are always strict But that’s not what rule (1) says. It says that a pattern binding is strict iff it binds a variable of unlifted type. Now I think we agree that your proposal says that a pattern binding is strict iff it or any of its sub-patterns has unlifted type, including wild-cards, variables, and constructor patterns; in fact any sub-pattern. Call that (2). So * (1) is necessary. * (2) is strictly stronger, and will make fewer program defined. But is perhaps less surprising. I think you could make a proposal out of that if you wanted. I can’t decide if I like it, myself, but I think that it, too, is simple and consistent. Simon From: Iavor Diatchki Sent: 07 September 2020 20:46 To: Simon Peyton Jones Cc: Richard Eisenberg ; Spiwack, Arnaud ; GHC developers Subject: Re: !RE: Implicit reboxing of unboxed tuple in let-patterns On Mon, Sep 7, 2020 at 5:12 AM Simon Peyton Jones via ghc-devs mailto:ghc-devs@haskell.org> wrote: 1. I don’t understand the details of Iavor’s proposal to add that “unlifted patterns are strict”, in addition to (1). Do you mean “any sub-pattern of the LHS has an unlifted type”? I think this is fully compatible with unlifted user defined data Just (# a,b #) = e would be strict. And even MkT _ = e would be strict if data T = MkT (# Int,Int #) Yes, the first one would be strict up to the tuple, and the second one would also be strict. I think this is the consistent way to interpret your rule (1) that unlifted bindings are always strict, and it shouldn't really matter if you used a variable pattern, or a wild card pattern. I don't think there's any other part of the language where replacing a `_` with an unused name changes the semantics of the program, and I don't think it should in this case either. Just to be fully explicit, the thing I find odd with GHC's current behavior is that these two are different: let MkT x = undefined in () --> undefined let MkT _ = undefined in () --> () Even more explicitly: let (_ :: Int#) = undefined in () --> () -- the value `undefined` is not representable in type `Int#` but GHC is happy to proceed because it doesn't need to represent it let (x :: Int#) = undefined in () --> () -- same situation, but now GHC is strict, even though it still doesn't need to represent the value. I think that the consistent behavior is for all of these to diverge, because laziness does not mix with unlfited values, at least in the presence of non-termination. -Iavor From: ghc-devs mailto:ghc-devs-bounces@haskell.org> On Behalf Of Richard Eisenberg Sent: 02 September 2020 14:47 To: Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io> Cc: GHC developers mailto:ghc-devs@haskell.org> Subject: Re: Implicit reboxing of unboxed tuple in let-patterns On Sep 2, 2020, at 9:39 AM, Spiwack, Arnaud mailto:arnaud.spiwack@tweag.io> wrote: Ooh… pattern synonyms for unboxed tuple. I must confess that I don't know what the semantics of these ought to be. It does look like an interesting can of worms. How do they currently desugar? Right now, there is one rule: if the type of any variable bound in the pattern is unlifted, then the pattern is an unlifter-var pattern and is strict. The pattern must be banged, unless the bound variable is not nested. This rule is consistent across all features. This thread is suggesting to add a special case -- one that seems to match intuition, but it's still a special case. And my question is: should the special case be for unboxed tuples? or should the special case be for any pattern whose overall type is unlifted? Richard _______________________________________________ ghc-devs mailing list ghc-devs@haskell.orgmailto:ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devshttps://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7Ca1b8984af610438e315a08d853669e2b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637351047493622347&sdata=mlcv1AZBJ%2FHQYDQtS7NPQ5YnbhQA17tWx9fzoVe8Gic%3D&reserved=0

Hello, there are multiple things being discussed here, which I think is leading to some confusion, in particular: 1. How do pattern bindings work in normal Haskell? It is not the case that only the outer pattern is lazy---when the patterns are matched depends on how the bound variables are used. I don't think we need to make changes here. 2. How should patterns on unlifted types work in pattern bindings, both nested and at the top level? This is what started this discussion originally. 3. How should nested bang patterns work in pattern bindings? This came out from Richard's examples in response to my suggestion on how (2) might work. 4. Should you always be able to replace `_` with an unused name without changing the semantics, which also came from Richard's examples. Going backward, here are my thoughts: 4. the answer to this should be `yes`, as it would make it consistent with how the rest of the language works. 3. nested bang patterns in pattern bindings should count as "uses" of the value and therefore should be strict. For example if I write `let ( !x, !y ) = undefined in ()`, I think this should be equivalent to `let (x,y) = undefined in x `seq` y `seq` ()`. With the current behavior the bang patterns don't do anything, while my guess would be that most people would expect the suggested behavior instead. As usual, we should not allow that at the top level. 2. I think that an unlifted pattern (meaning "a pattern on a value of an unlifted type") that is only nested in other unlifted patterns should be strict This includes top-level bindings as a special case, as they are not nested in anything. * For unlifted patterns nested in lifted patterns we have a choice: 2.1 I suggested that, for simplicity, these should also be strict, so that you could just say "all unlifted patterns are strict". This would mean that the containing (lifted) value would be always forced. 2.2 I could also see a reasonable case being made for these not forcing the evaluation of their containing value until the unlifted value is demanded. Perhaps this is more consistent with how the rest of the language works, so I'd be on board with that choice too. I think what I am suggesting is consistent with Arnaud's choice (1), except it goes into a bit more details on how nested patterns should work. Hope this clarifies things a bit, -Iavor On Thu, Sep 10, 2020 at 2:17 AM Spiwack, Arnaud wrote:

One thing that I had missed, until Simon pointed it out, is that in a let pat = … expression, only the outermost pattern of pat is lazy. So

let (x,Just y) = (1, undefined) in x `seq` ()

Diverges. (whereas let (x,~(Just y)) = (1, undefined) in x `seq` ()) doesn’t).

So, really, we are only speaking of the outermost pattern, which does simplify the discussion a little.

I don’t think that I share Iavor’s concern. In fact, I’ve got to say that I personally don’t see (1) as meaning that the pattern is actually strict. I just see a lazy pattern which happens to be immediately forced, because an unlifted variable is bound. In this view, it doesn’t follow that the presence of some unlifted pattern deep inside a lazy pattern ought to force the pattern.

However, if the outermost pattern is unlifted, then it’s most likely that it is not intended for the pattern to be lazy. From there, I see four ways forward:

1. Make let pat = … strict if the outermost pattern is unlifted 2. Make let pat = … emit a warning if the outermost pattern is unlifted, but not explicitly banged. 3. Decide that I’m mistaken, and that the current design is fine 4. Decide that I’m mistaken, and that Iavor’s design it best

What do you think? I’ll try and make a proposal soon (unless (3) is too popular for a proposal to be worth it).

On Tue, Sep 8, 2020 at 12:02 AM Simon Peyton Jones simonpj@microsoft.com http://mailto:simonpj@microsoft.com wrote:

I think this is the consistent way to interpret your rule (1) that

...

unlifted bindings are always strict

But that’s not what rule (1) says. It says that *a pattern binding is strict iff it binds a variable of unlifted type*.

Now I think we agree that your proposal says that *a pattern binding is strict iff it or any of its sub-patterns has unlifted type, *including wild-cards, variables, and constructor patterns; in fact *any* sub-pattern. Call that (2).

So

- (1) is *necessary*. - (2) is strictly stronger, and will make fewer program defined. But is perhaps less surprising.

I think you could make a proposal out of that if you wanted. I can’t decide if I like it, myself, but I think that it, too, is simple and consistent.

Simon

*From:* Iavor Diatchki *Sent:* 07 September 2020 20:46 *To:* Simon Peyton Jones *Cc:* Richard Eisenberg ; Spiwack, Arnaud < arnaud.spiwack@tweag.io>; GHC developers *Subject:* Re: !RE: Implicit reboxing of unboxed tuple in let-patterns

On Mon, Sep 7, 2020 at 5:12 AM Simon Peyton Jones via ghc-devs < ghc-devs@haskell.org> wrote:

1. I don’t understand the details of Iavor’s proposal to add that “unlifted patterns are strict”, in addition to (1). Do you mean “any sub-pattern of the LHS has an unlifted type”? I think this is fully compatible with unlifted user defined data

Just (# a,b #) = e

would be strict. And even

MkT _ = e

would be strict if data T = MkT (# Int,Int #)

Yes, the first one would be strict up to the tuple, and the second one would also be strict. I think this is the consistent way to interpret your rule (1) that unlifted bindings are always strict, and it shouldn't really matter if you used a variable pattern, or a wild card pattern. I don't think there's any other part of the language where replacing a `_` with an unused name changes the semantics of the program, and I don't think it should in this case either.

Just to be fully explicit, the thing I find odd with GHC's current behavior is that these two are different:

let MkT x = undefined in () --> undefined

let MkT _ = undefined in () --> ()

Even more explicitly:

let (_ :: Int#) = undefined in () --> () -- the value `undefined` is not representable in type `Int#` but GHC is happy to proceed because it doesn't need to represent it

let (x :: Int#) = undefined in () --> () -- same situation, but now GHC is strict, even though it still doesn't need to represent the value.

I think that the consistent behavior is for all of these to diverge, because laziness does not mix with unlfited values, at least in the presence of non-termination.

-Iavor

*From:* ghc-devs *On Behalf Of *Richard Eisenberg *Sent:* 02 September 2020 14:47 *To:* Spiwack, Arnaud *Cc:* GHC developers *Subject:* Re: Implicit reboxing of unboxed tuple in let-patterns

On Sep 2, 2020, at 9:39 AM, Spiwack, Arnaud wrote:

Ooh… pattern synonyms for unboxed tuple. I must confess that I don't know what the semantics of these ought to be. It does look like an interesting can of worms. How do they currently desugar?

Right now, there is one rule: if the type of any variable bound in the pattern is unlifted, then the pattern is an unlifter-var pattern and is strict. The pattern must be banged, unless the bound variable is not nested. This rule is consistent across all features.

This thread is suggesting to add a special case -- one that seems to match intuition, but it's still a special case. And my question is: should the special case be for unboxed tuples? or should the special case be for any pattern whose overall type is unlifted?

Richard

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs https://nam06.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=02%7C01%7Csimonpj%40microsoft.com%7Ca1b8984af610438e315a08d853669e2b%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C637351047493622347&sdata=mlcv1AZBJ%2FHQYDQtS7NPQ5YnbhQA17tWx9fzoVe8Gic%3D&reserved=0

Ah, yes, quite right: since the projections match the whole patterns, the bang patterns in a constructor would be forced as soon as one of the fields in the constructor is used, so this also diverges: ex3 = let (x, !y) = (5,undefined) in x The rule is consistent, to me it just seems quite unintuitive. On Thu, Sep 10, 2020 at 9:18 AM Richard Eisenberg wrote:

This whole area is clearly somewhat troublesome:

On Sep 10, 2020, at 12:05 PM, Iavor Diatchki wrote:

3. nested bang patterns in pattern bindings should count as "uses" of the value and therefore should be strict. For example if I write `let ( !x, !y ) = undefined in ()`, I think this should be equivalent to `let (x,y) = undefined in x `seq` y `seq` ()`. With the current behavior the bang patterns don't do anything, while my guess would be that most people would expect the suggested behavior instead. As usual, we should not allow that at the top level.

This isn't quite right.

Consider

ex0 = let ( !x, !y ) = undefined in () ex1 = let ( !x, !y ) = (5, undefined) in x ex2 = let ( !x, y ) = (5, undefined) in x

ex0 converges, because let-bindings are lazy by default. ex1 diverges, because the bang on y means that, when the patten-match happens at all, x and y are bound strictly. So bangs *do* matter in nested patterns within pattern bindings. By contrast, ex2 converges.

Again, I'm not arguing in favor of the current behavior, but I want to make sure we're all as informed as possible in this debate.

Richard

I am not sure what you'd expect this to do, but under what I was suggesting it would be equivalent to `let ~(x,y) = undefined in x `seq` y `seq ()` Obviously it would be nice to warn/report error that this is probably a mistake, which seems pretty easy to do. What useful functionality do you think is lost by this? The main tricky case I can think of is the interaction with pattern synonyms, as one would have to keep track of strict bindings in those. On Thu, Sep 10, 2020 at 10:12 AM Chris Smith wrote:

I agree that the strictness there was surprising, but I think this may be a case where what is superficially expected is, in the end, inconsistent.

What about:

let ~(!x, !y) = undefined in ()

If nested bang patterns implied strictness of their parents, this valid expression seems not to make any sense. I can see a few ways to deal with that, but none of them seem intuitive to me.

One could disallow it, and only allow strictness annotations on variables rather than all patterns, but this sacrifices a lot of functionality to avoid that surprise. Alternatively, one could say that upward propagation of strictness is only a default, but that definitely feels like a hack. It might make the original example behave as expected, but it is no longer for the expected reasons, and suddenly there is something even more complex going on.

I don't have a strong opinion here, but I think it's important to consider more complex cases when making the decision.

On Thu, Sep 10, 2020, 12:39 PM Iavor Diatchki wrote:

...

Ah, yes, quite right: since the projections match the whole patterns, the bang patterns in a constructor would be forced as soon as one of the fields in the constructor is used, so this also diverges:

ex3 = let (x, !y) = (5,undefined) in x

The rule is consistent, to me it just seems quite unintuitive.

On Thu, Sep 10, 2020 at 9:18 AM Richard Eisenberg wrote:

...

This whole area is clearly somewhat troublesome:

On Sep 10, 2020, at 12:05 PM, Iavor Diatchki wrote:

3. nested bang patterns in pattern bindings should count as "uses" of the value and therefore should be strict. For example if I write `let ( !x, !y ) = undefined in ()`, I think this should be equivalent to `let (x,y) = undefined in x `seq` y `seq` ()`. With the current behavior the bang patterns don't do anything, while my guess would be that most people would expect the suggested behavior instead. As usual, we should not allow that at the top level.

This isn't quite right.

Consider

ex0 = let ( !x, !y ) = undefined in () ex1 = let ( !x, !y ) = (5, undefined) in x ex2 = let ( !x, y ) = (5, undefined) in x

ex0 converges, because let-bindings are lazy by default. ex1 diverges, because the bang on y means that, when the patten-match happens at all, x and y are bound strictly. So bangs *do* matter in nested patterns within pattern bindings. By contrast, ex2 converges.

Again, I'm not arguing in favor of the current behavior, but I want to make sure we're all as informed as possible in this debate.

Richard

_______________________________________________ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs