Implicit reboxing of unboxed tuple in let-patterns

[Spiwack, Arnaud]

Iavor:

Yeah, I think these are nice examples that illustrate some of the problems
with the current behavior of GHC. For example, I think it is weird that b
non-terminates, but c does, because z is not used. I would expect those to
be equivalent.

What about if I rewrite all these patterns as

data X = MkX Int#
a = let ~(MkX 3#) = undefined in ()b = let ~(MkX z) = undefined in ()c
= let ~(MkX _) = undefined in ()d = let ~(MkX {}) = undefined in ()e =
let ~(_ :: X) = undefined in ()

Do you still expect c to diverge?

On Thu, Sep 3, 2020 at 9:04 PM chessai <chessai1996 at gmail.com> wrote:

> Not saying it's the best option, but it is an idea: Perhaps the behaviour
> could stay the same, but the proposed behaviour could sit behind a language
> pragma? I myself would always enable that pragma.
>
> On Thu, Sep 3, 2020, 13:59 Domínguez, Facundo <facundo.dominguez at tweag.io>
> wrote:
>
>> > I guess a more explicit option would be to make it an error to use a
>> lazy pattern on an unlifted type, and require programmers to manually add
>> the `!` but I am not sure that gains much, and is more work in the compiler.
>>
>> Not being used to deal with unlifted types, this would be my preferred
>> option. Having the meaning of let change depending on the levity of the
>> type is a good opportunity for confusion.
>>
>> Cheers,
>> Facundo
>>
>>
>> On Thu, Sep 3, 2020 at 3:43 PM Iavor Diatchki <iavor.diatchki at gmail.com>
>> wrote:
>>
>>> Yeah, I think these are nice examples that illustrate some of the
>>> problems with the current behavior of GHC.   For example, I think it is
>>> weird that `b` non-terminates, but `c` does, because `z` is not used.  I
>>> would expect those to be equivalent.
>>>
>>> My preference would be to use the simple rule I mentioned before, but
>>> change how bang patterns work in pattern bindings.  In particular, I think
>>> writing a bang pattern should constitute a use of the banged value.  I
>>> think two equivalent ways to specify this is to say that a) writing a
>>> nested bang pattern implicitly adds bangs to the enclosing patterns, or I
>>> think equivalently b) writing `!p` is the same as writing `x at p` and
>>> adding `seq x` the same way we do for simple `!x = e` definitions
>>>
>>> With this interpretation, all but `e` would diverge, which matches my
>>> intuition of how unboxed types should work.
>>>
>>> -Iavor
>>>
>>>
>>> On Thu, Sep 3, 2020 at 11:02 AM Richard Eisenberg <rae at richarde.dev>
>>> wrote:
>>>
>>>>
>>>>
>>>> On Sep 3, 2020, at 1:51 PM, Iavor Diatchki <iavor.diatchki at gmail.com>
>>>> wrote:
>>>>
>>>> How about the following rule:  unlifted patterns are always strict
>>>> (i.e., you desugar them as if they had an explicit  `!`).   A pattern is
>>>> "unlifted" if the type it examines is unlifted.   Seems simple enough and,
>>>> I think, it would do what most folks would expect.
>>>>
>>>>
>>>> I don't think it's this simple. For example:
>>>>
>>>> > data X = MkX Int#
>>>> >
>>>> > a = let MkX 3# = undefined in ()
>>>> > b = let MkX z = undefined in ()
>>>> > c = let MkX _ = undefined in ()
>>>> > d = let MkX {} = undefined in ()
>>>> > e = let _ :: X = undefined in ()
>>>>
>>>> Which of these diverge? e definitely converges, as X is lifted. b
>>>> definitely diverges, because it binds z, a variable of an unlifted type, to
>>>> a component of a diverging computation.
>>>>
>>>> In GHC today, all the cases other than b converge.
>>>>
>>>> Iavor suggests that a should diverge: 3# is a pattern of an unlifted
>>>> type. What about c? What about d? Very unclear to me.
>>>>
>>>> Note that banging the pattern nested inside the MkX does not change the
>>>> behavior (in GHC today) for any of the cases where this makes sense to do
>>>> so.
>>>>
>>>> Richard
>>>>
>>>>
>>>> I guess a more explicit option would be to make it an error to use a
>>>> lazy pattern on an unlifted type, and require programmers to manually add
>>>> the `!` but I am not sure that gains much, and is more work in the compiler.
>>>>
>>>> -Iavor
>>>>
>>>> On Thu, Sep 3, 2020 at 10:38 AM Richard Eisenberg <rae at richarde.dev>
>>>> wrote:
>>>>
>>>>>
>>>>>
>>>>> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud <arnaud.spiwack at tweag.io>
>>>>> wrote:
>>>>>
>>>>> This is all a tad tricky, I must say.
>>>>>
>>>>>
>>>>> ... which is one of the reasons I originally wanted one simple rule.
>>>>> I'm not now saying I was in the right, but it is an attractive resting
>>>>> point for this discussion.
>>>>>
>>>>> To be clear, I don't think there's going to be any concrete action
>>>>> here without a proposal, so perhaps once this thread finds a resting point
>>>>> different than the status quo, someone will have to write it up.
>>>>>
>>>>> Richard
>>>>> _______________________________________________
>>>>> ghc-devs mailing list
>>>>> ghc-devs at haskell.org
>>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>>>
>>>>
>>>> _______________________________________________
>>> ghc-devs mailing list
>>> ghc-devs at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>
>> _______________________________________________
>> ghc-devs mailing list
>> ghc-devs at haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20200904/df7208ca/attachment.html>