Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Uniformize destruct and pattern matching logic #1907

Merged
merged 2 commits into from
May 6, 2024

Conversation

yannham
Copy link
Member

@yannham yannham commented May 3, 2024

Depends on #1904

Context

When patterns were first introduced, only let-destructuring existed, and match expressions weren't a thing. Rather than manually generating code that would check that a pattern does match the destructured value, we piggy-backed on contracts instead, which was easier and provided better error messages. Up to now, this was still how destructuring worked: a contract is elaborated from the pattern and applied to the matched value, and should report any error if the value doesn't match. Then, destructuring is desugared to a series of let-bindings that assume that the destuctured value has the right shape. The generated code is thus quite simple, as it doesn't have any error handling to do.

When pattern matching landed, we kept the old destructuring infrastructure, because it was there and worked well, and had this slightly different behavior in case of non-matching patterns.

Motivation

However, this brings duplication: the compilation of match expressions does a work quite similar to destructuring, but they don't share much of the code.

What's more, we're at risk of having inconsistent semantics. Some questions aren't trivial to answer for destructuring, in particular with respect to lazyness: should let _ = x in null force x? What about let 'Foo _ = x in null, or let 'Foo 5 = x in null?

After extended discussions, we decided to give destructuring a simple semantics in term of pattern matching: let <pat> = <matched> in <body> should be strictly equivalent to <matched> |> match { <pat> => <body> }. Indeed, match has a clear semantics around forcing values in lazy languages. This also agrees with intuition, and gives a reasonable semantics for all the cases we wondered about.

This PR implements this change in practice, by getting rid of the ad-hoc desugaring of destructuring and by rewriting let-destructuring to actual pattern matching instead.

Getting rid of contracts

The contract generated from a pattern in let-destructuring had the advantage of providing better error messages in some cases. For example, instead of having the current (after this PR) "nonmatching pattern", you could have "missing field foo" or "extra field bar" for record patterns.

While we could keep the contract and still desugar to pattern matching, I still feel using a contract was kinda opportunistic at the time. It's also arguably strange to get contract errors pointing to destructuring, where there's no visible contract involved. Finally, it's quite a bit of code lying around.

In the end, I got rid of the elaborated contract for now in this PR. I believe most languages don't give better error messages when a pattern doesn't match. The user can still slap a contract on top of the matched value (that is, to do the contract elaboration and application, just manually) if a pattern doesn't match and they want more precise information.

Finally, there's no commitment required: if we later find out this was actually useful, we can revert the change and re-introduce elaborated contracts.

Deleted test

I deleted a test that was testing for patterns with multiple bound variables. I intend to forbid that altogether, see #1906.

@yannham yannham requested review from jneem and vkleen May 3, 2024 16:59
@github-actions github-actions bot temporarily deployed to pull request May 3, 2024 17:01 Inactive
Base automatically changed from feat/wildcard-pattern to master May 6, 2024 04:18
Copy link

dpulls bot commented May 6, 2024

🎉 All dependencies have been resolved !

When patterns were first introduced, only let-destructuring existed, and
match expressions weren't a thing. Rather than to manually generate code
that would check that a pattern does match the destructured value, we
piggy-backed on contracts instead, which was easier and provided better
error messages. Up to now, this was still how destructuring worked: a
contract is elaborated from the pattern and applied to the matched
value, and should report any error if the value doesn't match. Then,
destructuring is desugared to a series of let-bindings that assume that
the destucture value has the right shape. The generated code is thus
quite simple, as it doesn't have any error handling to do.

When pattern matching landed, we kept the old destructuring
infrastructure, because it was there and worked well. However, there is
duplication: the compilation of match expressions does a work quite
similar to destructuring.

What's more, we're at risk of having a diverging semantics. Some
questions aren't trivial to answer for destructuring, in particular with
respect to lazyness: should `let _ = x in null` force `x`? What about
`let 'Foo _ = x in null`, or `let 'Foo 5 = x in null`?

After some discussion, we decided to give destructuring a simple
semantics in term of pattern matching: `let <pat> = <matched> in <body>`
should be strictly equivalent to `<matched> |> match { <pat> => <body>
}`. Indeed, `match` has a clear semantics around forcing values in lazy
languages. This also agrees with intuition, or at least gives a
reasonable semantics for most cases.

This commit implements this change in practice, by getting rid of the
ad-hoc desugaring of destructuring and rewriting let-destructuring to
actual pattern matching instead.
@yannham yannham force-pushed the chore/uniformize-destruct-and-pattern-matching branch from 362476d to 922f237 Compare May 6, 2024 09:21
@github-actions github-actions bot temporarily deployed to pull request May 6, 2024 09:23 Inactive
core/src/term/pattern/compile.rs Outdated Show resolved Hide resolved
Co-authored-by: jneem <joeneeman@gmail.com>
@yannham yannham enabled auto-merge May 6, 2024 15:43
@github-actions github-actions bot temporarily deployed to pull request May 6, 2024 15:44 Inactive
@yannham yannham added this pull request to the merge queue May 6, 2024
Merged via the queue into master with commit 07cd719 May 6, 2024
5 checks passed
@yannham yannham deleted the chore/uniformize-destruct-and-pattern-matching branch May 6, 2024 16:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants