Surprising interaction between @-patterns and nested patterns
Consider the following: let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` () () but then combining the patterns into an @-pattern, which really feels like it shouldn't change semantics: let x1@((_, _), _) = (undefined, ()) in x1 `seq` () -> undefined Does this strike anyone else as odd? The reason for this behaviour is that let x@p = rhs in body is translated to case rhs of ~(x@p) -> body according to section 3.12 of The Report[1] which is then translated to (\x -> body) (case rhs of x@p -> x) if p binds no variables, according to section 3.17.3 of The Report[2], and then to (\x -> body) (case rhs of p -> (\x -> x) rhs) which is equivalent to (\x -> body) (case rhs of p -> rhs) Putting it all together let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` () desugars as (\x0 -> x0 `seq` ()) (let v = (undefined, ()) in case v of ((_, _), _) -> v) which evaluates as let v = (undefined, ()) in case v of ((_, _), _) -> () This seems very odd to me. Why should combining two non-diverging patterns into an @-pattern cause divergence? Specifically, the translation from let x@p = rhs in body to case rhs of ~(x@p) -> body seems highly dubious. It comes from the more general rule translating let p = rhs in body to case rhs of ~p in body but it seems to interact badly with @-patterns. It seems like the rule for @-patterns should be something like let x@p = rhs in body translates to case rhs of ~(x@(~p)) in body Then the original expression containing x1 would not diverge. Does anyone else have a view on this matter? Tom [1] https://www.haskell.org/onlinereport/exps.html#sect3.12 [2] https://www.haskell.org/onlinereport/exps.html#sect3.17.3
I don't have an opinion; or maybe I do, my hunch is that any alternative would be differently but equally tricky. But the x0 example is equivalent to simply: let x0 = (undefined, ()) in x0 `seq` () which may be surprisingly unsurprising because I see that it has almost nothing to do with the x1 example. In order to make "pattern = x0" actually relevant, you may want: let { x0 = (undefined, ()) ; ((_, _), y) = x0 } in y `seq` () -> undefined The semantic explanation involves the same considerations as those of the x1 example. And you can hold the same opinion, for or against. On 2023-01-02 18:00, Tom Ellis wrote:
Consider the following:
let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` () ()
but then combining the patterns into an @-pattern, which really feels like it shouldn't change semantics:
let x1@((_, _), _) = (undefined, ()) in x1 `seq` () -> undefined
Does this strike anyone else as odd? The reason for this behaviour is that
let x@p = rhs in body
is translated to
case rhs of ~(x@p) -> body
according to section 3.12 of The Report[1] which is then translated to
(\x -> body) (case rhs of x@p -> x)
if p binds no variables, according to section 3.17.3 of The Report[2], and then to
(\x -> body) (case rhs of p -> (\x -> x) rhs)
which is equivalent to
(\x -> body) (case rhs of p -> rhs)
Putting it all together
let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` ()
desugars as
(\x0 -> x0 `seq` ()) (let v = (undefined, ()) in case v of ((_, _), _) -> v)
which evaluates as
let v = (undefined, ()) in case v of ((_, _), _) -> ()
This seems very odd to me. Why should combining two non-diverging patterns into an @-pattern cause divergence? Specifically, the translation from
let x@p = rhs in body
to
case rhs of ~(x@p) -> body
seems highly dubious. It comes from the more general rule translating
let p = rhs in body
to
case rhs of ~p in body
but it seems to interact badly with @-patterns. It seems like the rule for @-patterns should be something like
let x@p = rhs in body
translates to
case rhs of ~(x@(~p)) in body
Then the original expression containing x1 would not diverge.
Does anyone else have a view on this matter?
Tom
[1] https://www.haskell.org/onlinereport/exps.html#sect3.12
[2] https://www.haskell.org/onlinereport/exps.html#sect3.17.3 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
My opinion, for several years, has been that the Haskell designers erred in making outermost patterns lazy by default in let and where, and at the top level. I believe they should have gone with something much simpler: 1. Patterns are strict by default. 2. Variables are lazy by default. 3. Patterns at the top level must be marked lazy. 4. (With bang patterns) Variables at the top level may not be marked strict. That would harmonize the way patterns are handled in let and where with the way they're handled in function arguments and case expressions, as well as removing the outermost-pattern special case which makes the *strictness* of inner patterns surprising. Unfortunately, I don't think there's much chance of any of these changing in Haskell. On Mon, Jan 2, 2023, 6:00 PM Tom Ellis < tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:
Consider the following:
let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` () ()
but then combining the patterns into an @-pattern, which really feels like it shouldn't change semantics:
let x1@((_, _), _) = (undefined, ()) in x1 `seq` () -> undefined
Does this strike anyone else as odd? The reason for this behaviour is that
let x@p = rhs in body
is translated to
case rhs of ~(x@p) -> body
according to section 3.12 of The Report[1] which is then translated to
(\x -> body) (case rhs of x@p -> x)
if p binds no variables, according to section 3.17.3 of The Report[2], and then to
(\x -> body) (case rhs of p -> (\x -> x) rhs)
which is equivalent to
(\x -> body) (case rhs of p -> rhs)
Putting it all together
let x0 = (undefined, ()) ; ((_, _), _) = x0 in x0 `seq` ()
desugars as
(\x0 -> x0 `seq` ()) (let v = (undefined, ()) in case v of ((_, _), _) -> v)
which evaluates as
let v = (undefined, ()) in case v of ((_, _), _) -> ()
This seems very odd to me. Why should combining two non-diverging patterns into an @-pattern cause divergence? Specifically, the translation from
let x@p = rhs in body
to
case rhs of ~(x@p) -> body
seems highly dubious. It comes from the more general rule translating
let p = rhs in body
to
case rhs of ~p in body
but it seems to interact badly with @-patterns. It seems like the rule for @-patterns should be something like
let x@p = rhs in body
translates to
case rhs of ~(x@(~p)) in body
Then the original expression containing x1 would not diverge.
Does anyone else have a view on this matter?
Tom
[1] https://www.haskell.org/onlinereport/exps.html#sect3.12
[2] https://www.haskell.org/onlinereport/exps.html#sect3.17.3 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
On Mon, 2 Jan 2023, David Feuer wrote:
My opinion, for several years, has been that the Haskell designers erred in making outermost patterns lazy by default in let and where, and at the top level. I believe they should have gone with something much simpler: 1. Patterns are strict by default. 2. Variables are lazy by default. 3. Patterns at the top level must be marked lazy. 4. (With bang patterns) Variables at the top level may not be marked strict.
That would harmonize the way patterns are handled in let and where with the way they're handled in function arguments and case expressions, as well as removing the outermost-pattern special case which makes the *strictness* of inner patterns surprising.
me too
Unfortunately, I don't think there's much chance of any of these changing in Haskell.
Could start as a nice GHC extension like Strict Haskell.
On Tue, Jan 03, 2023 at 08:22:08AM +0100, Henning Thielemann wrote:
On Mon, 2 Jan 2023, David Feuer wrote:
My opinion, for several years, has been that the Haskell designers erred in making outermost patterns lazy by default in let and where, and at the top level. I believe they should have gone with something much simpler: 1. Patterns are strict by default. 2. Variables are lazy by default. 3. Patterns at the top level must be marked lazy. 4. (With bang patterns) Variables at the top level may not be marked strict.
That would harmonize the way patterns are handled in let and where with the way they're handled in function arguments and case expressions, as well as removing the outermost-pattern special case which makes the *strictness* of inner patterns surprising.
me too
I am inclined to agree. But are there any nasty corner cases involving recursive bindings?
Unfortunately, I don't think there's much chance of any of these changing in Haskell.
Could start as a nice GHC extension like Strict Haskell.
I agree, but an easier sell if there aren't nasty corner cases. Tom
There are certainly cases where lazy pattern matches are important. But IMO they're always *a bit weird*, and deserve that ~ syntactic marker letting people know that *something a bit weird is happening*. On Thu, Jan 5, 2023, 6:18 AM Tom Ellis < tom-lists-haskell-cafe-2017@jaguarpaw.co.uk> wrote:
On Tue, Jan 03, 2023 at 08:22:08AM +0100, Henning Thielemann wrote:
On Mon, 2 Jan 2023, David Feuer wrote:
My opinion, for several years, has been that the Haskell designers erred in making outermost patterns lazy by default in let and where, and at the top level. I believe they should have gone with something much simpler: 1. Patterns are strict by default. 2. Variables are lazy by default. 3. Patterns at the top level must be marked lazy. 4. (With bang patterns) Variables at the top level may not be marked strict.
That would harmonize the way patterns are handled in let and where with the way they're handled in function arguments and case expressions, as well as removing the outermost-pattern special case which makes the *strictness* of inner patterns surprising.
me too
I am inclined to agree. But are there any nasty corner cases involving recursive bindings?
Unfortunately, I don't think there's much chance of any of these changing in Haskell.
Could start as a nice GHC extension like Strict Haskell.
I agree, but an easier sell if there aren't nasty corner cases.
Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
participants (4)
-
Albert Y. C. Lai -
David Feuer -
Henning Thielemann -
Tom Ellis