Implicit reboxing of unboxed tuple in let-patterns

[Iavor Diatchki]

Yes

On Fri, Sep 4, 2020 at 2:29 AM Spiwack, Arnaud <arnaud.spiwack at tweag.io>
wrote:

> 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
>>
> _______________________________________________
> 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/8a6a1e2a/attachment.html>