Re: COMPLETE pragmas
You are my hero. On Thu, Sep 3, 2020 at 9:22 AM Sebastian Graf wrote: > Hi folks, > > I implemented what I had in mind in > https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3959. CI should turn > green any hour now, so feel free to play with it if you want to. > With the wonderful https://github.com/mpickering/ghc-artefact-nix it will > just be `ghc-head-from 3959`. > > Cheers, > Sebastian > > Am Di., 1. Sept. 2020 um 22:09 Uhr schrieb Joachim Breitner < > m...@joachim-breitner.de>: > >> Am Dienstag, den 01.09.2020, 10:11 +0200 schrieb Sebastian Graf: >> > > 2.) Another scenario that I'd really love to see supported with >> > > COMPLETE pragmas is a way to use | notation with them like you can >> > > with MINIMAL pragmas. >> > >> > (2) is a neat idea, but requires a GHC proposal I'm not currently >> > willing to get into. I can also see a design discussion around >> > allowing arbitrary "formulas" (e.g., not only what is effectively >> > CNF). >> > >> > A big bonus of your design is that it's really easy to integrate into >> > the current implementation, which is what I'd gladly do in case such >> > a proposal would get accepted. >> >> in the original ticket where a COMPLETE pragma was suggested ( >> https://gitlab.haskell.org/ghc/ghc/-/issues/8779) the ability to >> specify arbitrary boolean formulas was already present: >> >> “So here is what I think might work well, inspired by the new MINIMAL >> pragma: … The syntax is essentially the same as for MINIMAL, i.e. a >> boolean formula, with constructors and pattern synonyms as atoms. In >> this case” >> >> So one _could_ say that this doesn’t need a proposal, because it would >> just be the implementation finishing the original task ;-) >> >> >> Cheers, >> Joachim >> >> -- >> Joachim Breitner >> m...@joachim-breitner.de >> http://www.joachim-breitner.de/ >> >> >> ___ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
> 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
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@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
> wrote:
>
>>
>>
>> On Sep 3, 2020, at 1:51 PM, Iavor Diatchki
>> 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
>> wrote:
>>
>>>
>>>
>>> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud
>>> 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@haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>>
>>
>> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: COMPLETE pragmas
wonderful! On Thu, Sep 3, 2020 at 12:22 PM Sebastian Graf wrote: > Hi folks, > > I implemented what I had in mind in > https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3959. CI should turn > green any hour now, so feel free to play with it if you want to. > With the wonderful https://github.com/mpickering/ghc-artefact-nix it will > just be `ghc-head-from 3959`. > > Cheers, > Sebastian > > Am Di., 1. Sept. 2020 um 22:09 Uhr schrieb Joachim Breitner < > m...@joachim-breitner.de>: > >> Am Dienstag, den 01.09.2020, 10:11 +0200 schrieb Sebastian Graf: >> > > 2.) Another scenario that I'd really love to see supported with >> > > COMPLETE pragmas is a way to use | notation with them like you can >> > > with MINIMAL pragmas. >> > >> > (2) is a neat idea, but requires a GHC proposal I'm not currently >> > willing to get into. I can also see a design discussion around >> > allowing arbitrary "formulas" (e.g., not only what is effectively >> > CNF). >> > >> > A big bonus of your design is that it's really easy to integrate into >> > the current implementation, which is what I'd gladly do in case such >> > a proposal would get accepted. >> >> in the original ticket where a COMPLETE pragma was suggested ( >> https://gitlab.haskell.org/ghc/ghc/-/issues/8779) the ability to >> specify arbitrary boolean formulas was already present: >> >> “So here is what I think might work well, inspired by the new MINIMAL >> pragma: … The syntax is essentially the same as for MINIMAL, i.e. a >> boolean formula, with constructors and pattern synonyms as atoms. In >> this case” >> >> So one _could_ say that this doesn’t need a proposal, because it would >> just be the implementation finishing the original task ;-) >> >> >> Cheers, >> Joachim >> >> -- >> Joachim Breitner >> m...@joachim-breitner.de >> http://www.joachim-breitner.de/ >> >> >> ___ >> ghc-devs mailing list >> ghc-devs@haskell.org >> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs >> > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
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@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 wrote:
>
>
> On Sep 3, 2020, at 1:51 PM, Iavor Diatchki
> 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
> wrote:
>
>>
>>
>> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud
>> 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@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>>
>
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
> On Sep 3, 2020, at 1:51 PM, Iavor Diatchki 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 > wrote:
>
>
>> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud > > 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@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
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 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 wrote: > > > On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud > 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@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
> On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: COMPLETE pragmas
Hi folks, I implemented what I had in mind in https://gitlab.haskell.org/ghc/ghc/-/merge_requests/3959. CI should turn green any hour now, so feel free to play with it if you want to. With the wonderful https://github.com/mpickering/ghc-artefact-nix it will just be `ghc-head-from 3959`. Cheers, Sebastian Am Di., 1. Sept. 2020 um 22:09 Uhr schrieb Joachim Breitner < m...@joachim-breitner.de>: > Am Dienstag, den 01.09.2020, 10:11 +0200 schrieb Sebastian Graf: > > > 2.) Another scenario that I'd really love to see supported with > > > COMPLETE pragmas is a way to use | notation with them like you can > > > with MINIMAL pragmas. > > > > (2) is a neat idea, but requires a GHC proposal I'm not currently > > willing to get into. I can also see a design discussion around > > allowing arbitrary "formulas" (e.g., not only what is effectively > > CNF). > > > > A big bonus of your design is that it's really easy to integrate into > > the current implementation, which is what I'd gladly do in case such > > a proposal would get accepted. > > in the original ticket where a COMPLETE pragma was suggested ( > https://gitlab.haskell.org/ghc/ghc/-/issues/8779) the ability to > specify arbitrary boolean formulas was already present: > > “So here is what I think might work well, inspired by the new MINIMAL > pragma: … The syntax is essentially the same as for MINIMAL, i.e. a > boolean formula, with constructors and pattern synonyms as atoms. In > this case” > > So one _could_ say that this doesn’t need a proposal, because it would > just be the implementation finishing the original task ;-) > > > Cheers, > Joachim > > -- > Joachim Breitner > m...@joachim-breitner.de > http://www.joachim-breitner.de/ > > > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
> > 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. >> > > I think the intuition I followed so far was "bindings with unlifted *RHS* > are strict". > This is a very different rule indeed! And one which gives a strict semantic to the initial offender. But there are holes in it: if I `let (x, y) = blah in …` and `x` is at an unlifted type, the pattern _needs_ to be strict (this is solved by the current rule as described by Richard) despite the rhs being at a lifted type. That's because binding `x` forces the pattern anyway, by definition. There are questions about nested patterns, as well. What about `let (U x, y) = blah in …`, where `U` is some unlifted type. Is the nested `U x` pattern strict? or is it lazy? There is no corresponding right-hand side. This is all a tad tricky, I must say. ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
Hi, 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. > I think the intuition I followed so far was "bindings with unlifted *RHS* are strict". So if I take a program in a strict language with Haskell syntax (Idris with a different syntax, not like -XStrict) and replace all types with their unlifted counterparts (which should be possible once we have -XUnliftedDatatypes), then I get exactly the same semantics in GHC Haskell. I find this property very useful. As a special case that means that any binders of unlifted type are bound strictly, if only for uniformity with simple variable bindings. I think my intuition is different to Richard's rule only for the "unlifted constructor match with nested lifted-only variable matches" case. Sebastian Am Do., 3. Sept. 2020 um 14:48 Uhr schrieb Spiwack, Arnaud < arnaud.spiw...@tweag.io>: > 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? >> > > My intuition would be: for all unlifted types. I'd submit that the > distinction between lazy and strict pattern-matching doesn't really make a > ton of sense for unlifted types. To implement lazy pattern-matching on an > unlifted type, one has to actually indirect through another type, which I > find deeply suspicious. > > That being said > > 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. >> > > I realise that there are a lot of subtil details to get right to specify > pattern-matching. Or at the very least, that it's difficult to come up with > a straightforward specification which is as clear as the one above. > > I'm wondering though: have there been discussions which led to the above > rule, or did it just come to be, mostly informally? (and if there have been > explicit discussions, are they recorded somewhere?) > ___ > ghc-devs mailing list > ghc-devs@haskell.org > http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs > ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Re: Implicit reboxing of unboxed tuple in let-patterns
> > 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? > My intuition would be: for all unlifted types. I'd submit that the distinction between lazy and strict pattern-matching doesn't really make a ton of sense for unlifted types. To implement lazy pattern-matching on an unlifted type, one has to actually indirect through another type, which I find deeply suspicious. That being said 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. > I realise that there are a lot of subtil details to get right to specify pattern-matching. Or at the very least, that it's difficult to come up with a straightforward specification which is as clear as the one above. I'm wondering though: have there been discussions which led to the above rule, or did it just come to be, mostly informally? (and if there have been explicit discussions, are they recorded somewhere?) ___ ghc-devs mailing list ghc-devs@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
