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.

Sign up for GitHub

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

Jump to bottom

Syntax sugar for nested Sigma types #140

Closed
fizruk opened this issue Oct 13, 2023 · 1 comment · Fixed by #183
Closed

Syntax sugar for nested Sigma types #140

fizruk opened this issue Oct 13, 2023 · 1 comment · Fixed by #183
Assignees
@geffk2
Labels
enhancement New feature or request

Comments

@fizruk
Copy link
Member

fizruk commented Oct 13, 2023

It is possible to generalise Σ to accept arbitrary parameters like in #define:

Σ (a : A), ∑ (b : B), C a b       -- current syntax (right assoc)
Σ ((a, b) : ∑ (a : A), B), C a b  -- current syntax (left assoc)
Σ (a : A) (b : B), C a b          -- generalised syntax (should be desugared to left assoc)

Originally posted by @fizruk in emilyriehl/yoneda#14 (comment)

Correspondingly, there should be syntax sugar for pair patterns:

\ (a, (b, c)) -> ...        -- explicit patterns (right assoc)
\ ((a, b), c) -> ...        -- explicit patterns (left assoc)
\ (a, b, c) -> ...          -- explicit patterns (should be desugared to left assoc)

This should be a simple change.
@fizruk fizruk added the enhancement New feature or request label Oct 13, 2023
@TashiWalde
Copy link

TashiWalde commented Oct 13, 2023 •
edited
Loading

Ideally it should be possible to fully specify the mixed associativity of a Σ-type with only a single Σ symbol.
For example I would like to be able to write any of the following if I care about the exact bracketting of my terms.

Σ (a : A , (b : B a , c : C a b)) , (d : D a b c)
Σ (a : A , b : B a) , (c : C a b , d : D a b c)

And I would probably prefer one of the following for the unbiased version (which then secretly desugars to left assoc).

Σ (a : A , b : B a , C a b)
Σ (a : A) (b : B a) (C a b)

It just seems a bit asymmetric to have one but not all commas.

One additional alternative which I also quite like is to use the × as an infix operator for dependent sums. For example:

(a : A) × B × (c : C a) × (D a c)

@geffk2 geffk2 self-assigned this Apr 18, 2024
@geffk2 geffk2 linked a pull request Apr 19, 2024 that will close this issue
Add syntax sugar for nested sigma-types #183
Merged
@geffk2 geffk2 mentioned this issue Apr 19, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@geffk2 geffk2

Labels
enhancement New feature or request
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Add syntax sugar for nested sigma-types geffk2/rzk
3 participants
@fizruk @TashiWalde @geffk2