8000 Hidden argument puns · Issue #6325 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Hidden argument puns #6325

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
Closed
nad opened this issue Nov 14, 2022 · 7 comments
Closed

Hidden argument puns #6325

nad opened this issue Nov 14, 2022 · 7 comments
Labels
hidden arguments Insertion of hidden arguments and implicit lambdas syntax Bike-shedding of the surface syntax type: enhancement Issues and pull requests about possible improvements
Milestone
2.6.4

Comments

@nad
Copy link
Contributor
nad commented Nov 14, 2022

Recently I wrote the following code:

  {R = R} {x₁ = x₁} {x₂ = x₂} {y₁ = y₁} {y₂ = y₂}
  {xs₁ = xs₁} {e₁ = e₁} {xs₂ = xs₂} {e₂ = e₂} {e₁′ = e₁′}

I have lots of code of this highly redundant form. I could perhaps use positional matching for some of the arguments, but with generalisable variables it might not be clear in what order the arguments appear, and perhaps the order changes if Agda's unification algorithm changes.

I would like to be able to write the following instead:

  {R} {x₁} {x₂} {y₁} {y₂} {xs₁} {e₁} {xs₂} {e₂} {e₁′}

I suggest that we add a flag called something like --implicit-argument-puns (the name is based on GHC's feature NamedFieldPuns). If that flag is used, then {x} in a binding position means {x = x}.

In analogy with GHC's record wildcards one might also consider supporting something like {…}, where this would mean, roughly, "{x} for each implicit argument x that has not been explicitly bound". However, I don't want to mix scope-checking and type-checking, so I do not suggest that we should implement this.
@nad nad added type: enhancement Issues and pull requests about possible improvements syntax Bike-shedding of the surface syntax hidden arguments Insertion of hidden arguments and implicit lambdas labels Nov 14, 2022
@nad nad added this to the 2.6.4 milestone Nov 14, 2022
@andreasabel
Copy link
Member
andreasabel commented Nov 28, 2022 •
edited
Loading

With --implicit-argument-puns on, should something like f {g x} be an error? (You would have to pass that argument by name, like f {z = g x}.)

@nad
Copy link
Contributor Author
nad commented Nov 28, 2022

I only intended this change to affect left-hand side binders.

@andreasabel
Copy link
Member

I only intended this change to affect left-hand side binders.

So, should {suc x} be an error as or in a pattern?

And what if my variable name clashes with a constructor?

open import Agda.Builtin.Nat

foo : {zero : Nat} -> Nat
foo {zero} = 43

@nad
Copy link
Contributor Author
nad commented Nov 29, 2022

So, should {suc x} be an error as or in a pattern?

Do you want Agda to reject f {x y} = …? I only suggested to change the meaning of {x}, not {x y} or {(x)}.

And what if my variable name clashes with a constructor?

Good point. When you expand {x} to {x = x}, then I think the second occurrence of x should be treated as a bound variable. If there is also a constructor called x in scope, then I think Agda should warn about this.

@nad
Copy link
Contributor Author
nad commented Jan 20, 2023

I think it should also be possible to have instance argument puns, so I suggest that the flag is called --hidden-argument-puns instead.

When you expand {x} to {x = x}, then I think the second occurrence of x should be treated as a bound variable. If there is also a constructor called x in scope, then I think Agda should warn about this.

I've changed my mind. The pattern {constructor}, with constructor interpreted as a pun, does not correspond to a pattern without puns, so I think we should disallow it.

@nad nad changed the title Implicit argument puns Hidden argument puns Jan 20, 2023
nad added a commit that referenced this issue Jan 20, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
18669af
nad added a commit that referenced this issue Jan 20, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
b465d60
@nad nad mentioned this issue Jan 20, 2023
Merged
nad added a commit that referenced this issue Jan 24, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
eba3008
nad added a commit that referenced this issue Jan 24, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
b67fa15 
With input from Andreas Abel.
nad added a commit that referenced this issue Jan 24, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
602b8f0 
With input from Andreas Abel.
nad added a commit that referenced this issue Jan 25, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
ed16f98 
I modified a previous version of the commit after feedback from
Andreas Abel.
nad added a commit that referenced this issue Jan 26, 2023
@nad
[ #6325 ] Added --hidden-argument-puns.
6c7d9d0 
I modified a previous version of the commit after feedback from
Andreas Abel.
@andreasabel
Copy link
Member

@nad: Anything left to be done here for 2.6.4?

@nad
Copy link
Contributor Author
nad commented May 15, 2023

I don't think so.

@nad nad closed this as completed May 15, 2023
@andreasabel andreasabel mentioned this issue Jul 21, 2023
Closed
5 tasks
@nad nad mentioned this issue Nov 10, 2023
Open
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this issue Apr 10, 2024
@nad @JobPetrovcic
[ agda#6325 ] Added --hidden-argument-puns.
272b112 
I modified a previous version of the commit after feedback from
Andreas Abel.
andreasabel added a commit that referenced this issue Sep 11, 2024
@andreasabel
Re #6325: refactor: expandPuns is an instance of mapCPattern
39178f4
andreasabel added a commit that referenced this issue Sep 11, 2024
@andreasabel
Re #6325: Factor out expandPunsOpt
d5ea5a4
@andreasabel andreasabel mentioned this issue Sep 11, 2024
Merged
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Re agda#6325: refactor: expandPuns is an instance of mapCPattern
d184ce5
fredins pushed a commit to fredins/agda that referenced this issue Nov 24, 2024
@andreasabel @fredins
Re agda#6325: Factor out expandPunsOpt
063d769
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
hidden arguments Insertion of hidden arguments and implicit lambdas syntax Bike-shedding of the surface syntax type: enhancement Issues and pull requests about possible improvements
< 3BEA !-- '"` -->
Projects
None yet
Milestone
2.6.4
Development

No branches or pull requests
2 participants
@nad @andreasabel
0