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

Overloaded &: make non-dependent tuple whenever possible #2816

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from

Conversation

W95Psp
Copy link
Contributor

@W95Psp W95Psp commented Feb 1, 2023

Hi,

Recently in a Slack conversation about deprecating the * operator for tuples in favor of the overloaded & operator, @TWal pointed out that the & operator sometimes makes dependent tuples when it is not necessary. Quoting him:

TWal: I sometimes had legitimate use of *, for example for the pair x:a{p x} & b, F* makes it a dependent pair so the fix I found was to write x:a{p x} * b

This PR makes the & operator desugar to a non-dependent tuple whenever it is possible.
It only desugars to dependent tuples if there is actually a dependency.

@W95Psp W95Psp force-pushed the fix-dependent-tuples branch 2 times, most recently from 524d6a1 to 63a7fe6 Compare February 1, 2023 10:10
@W95Psp W95Psp force-pushed the fix-dependent-tuples branch 2 times, most recently from 122178a to d323dde Compare February 2, 2023 16:07
@W95Psp W95Psp marked this pull request as draft February 13, 2023 09:37
@mtzguido
Copy link
Member

We chatted about some options today:

  • Taking this patch, which can be a breaking change
  • Using a different symbol for non-dependent and dependent tuples (& and&>?)
  • Having the user write tuple2/dtuple2 (one of the two) to disambiguate, and keep & for the other.
  • Desugaring to dtuple2 and displaying a warning when the variable does not appear in the right type.
  • Desugaring this to dtuple2, and enclosing the left type in parentheses to make it a tuple2, (so x:a{p x} & b is dependent, but (x:a{p x}) & b is not). I tried it here and here and regressions seem minor.

@W95Psp
Copy link
Contributor Author

W95Psp commented Feb 15, 2023

Personally I'm in favor of the last point you're mentionning Guido. It's a purely syntactic thing, the rule is easy to understand and I think it is quite intuitive.
I think we should close this PR in favor of that parenthesis rule change

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.

None yet

2 participants