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@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@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@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@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@richarde.dev> wrote:

On Sep 3, 2020, at 1:51 PM, Iavor Diatchki <iavor.diatchki@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@richarde.dev> wrote:

On Sep 3, 2020, at 12:10 PM, Spiwack, Arnaud <arnaud.spiwack@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@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

_______________________________________________
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