[Agda] When to use implicit arguments [Re: Printing named arguments]
Andreas Abel
abela at chalmers.se
Mon Apr 10 15:29:27 CEST 2017
> A very important thing is to learn when to use implicit vs explicit
> arguments.
In my experience, Agda can usually not infer an argument you case on.
For instance,
+-assoc : ∀ m n o → (m + n) + o ≡ m + (n + o)
+-assoc zero _ _ = refl
+-assoc (suc m) n o = cong suc $ +-assoc m n o
Here, it makes sense to make n and o implicit, but not m. Agda can
reconstruct n and o usually when you use +-assoc to prove a goal (whose
type is known).
However, when you are using 'rewrite', you need to pass all arguments
... rewrite +-assoc a b c
since Agda needs to compute the equality you want to rewrite with from
the term `+-assoc a b c'. Thus, in a 'rewrite'-heavy style, one can
only omit arguments that are inferable from other arguments, not the one
inferable from the target.
Best,
Andreas
On 10.04.2017 14:26, Apostolis Xekoukoulotakis wrote:
> With Andreas commit, the behavior is to replicate the style the
> programmer used, which means that nothing will change for you.
>
> I do remember being confused by
> "{x = x}" as well when I was learning the language.
>
> I am too battling with cleaning the code so as to be readable.
> A very important thing is to learn when to use implicit vs explicit
> arguments.
> I haven't mastered that yet.
>
> I also wonder whether there is a difference in complexity between
> mathematical proofs and software development.
> As far as I know, Mathematics are characterized by elegance and simplicity.
>
> On Mon, Apr 10, 2017 at 10:00 AM, Andreas Abel <abela at chalmers.se
> <mailto:abela at chalmers.se>> wrote:
>
> Thanks, Martin,
>
> for the explanation. I can confirm that a named argument like
>
> {x = x}
>
> can cause quite some confusion to the reader. (It looks
> non-sensical unless you are familiar with the specifics of Agda syntax.)
>
> Now, if you look at the bug report
>
> https://github.com/agda/agda/issues/2537
> <https://github.com/agda/agda/issues/2537>
>
> you see that the current situation is incoherent. Agda preserves
> named arguments in the usual case, but not for with-clauses. I
> think that should be fixed.
>
> The next question is whether Agda should *introduce* named arguments
> or rather use a sequence of {_} arguments when, for instance, you
> split on a hidden argument.
>
> For your taste, Agda should not introduce named arguments ever in
> printing. Maybe a flag like
>
> --no-named-arguments
>
> could represent this style of printing terms.
>
> On 07.04.2017 16:23, Martin Escardo wrote:
>
> On 07/04/17 15:01, Andreas Abel wrote:
>
> Hi Martin,
>
> when it comes to interactive editing, we are striving for
> the commands
> to preserve/imitate the user code as much as possible.
> Thus, if the
> user has chosen named arguments, the splitter should
> preserve this
> style, instead of switching to positional arguments.
>
> Why are you fond of the current behavior?
>
>
> Because, for personal idiosyncratic reasons, I don't use named
> arguments. Writing {x = x} {y = y} doesn't look idiomatic, and is
> confusing for people who don't know Agda but who I want to be
> able to
> understand my code. I write the Agda code for myself to read,
> and not
> for simply having something accepted and blessed by the Agda
> typchecker.
> If you are never going to write {x = a}, and you write always {x
> = x},
> this seems a wrong design. And {x = x} looks very curious and
> cryptic.
> Anyway, you can safely ignore my opinion. But this is what it is.
> Additionally I think adding variables that are not used in types
> makes
> the types very unreadable.
>
> Best,
> Martin
>
>
>
> Best,
> Andreas
>
> On 07.04.2017 16:02, Martin Escardo wrote:
>
> Hi Andreas, for several reasons, I like the way things
> are regarding
> this. If there is any change, could it be achieved by a
> different
> control sequence, so as to preserve the existing
> behaviour? Thanks,
> Martin
>
> On 07/04/17 13:33, Andreas Abel wrote:
>
> Agda uses {_} to skip unsupplied hidden arguments.
> Instead it could use
> a named hidden argument for the supplied one {frll}.
>
> Could you put a reasonably small self-contained test
> case on the issue
> tracker?
>
> Thanks,
> Andreas
>
> On 07.04.2017 13:59, Apostolis Xekoukoulotakis wrote:
>
> ```
> removeCom {frll = frll} (_⊂_ {pll = pll} {ll =
> ll} {ind = ind} lf lf₁)
> (_←⊂ {lind = lind} ic) with (replLL ll ind
> (replLL pll lind frll)) |
> (drepl=>repl+ {frll = frll} ind lind)
> ... | g | r = {!!}
>
> ```
> case splitting creates this:
>
> ```
> removeCom {frll = frll} (_⊂_ {pll = pll} {ll =
> ll} {ind = ind} lf lf₁)
> (_←⊂ {lind = lind} ic) with (replLL ll ind
> (replLL pll lind frll)) |
> (drepl=>repl+ {frll = frll} ind lind)
> removeCom {_} {_} {_} {_} {_} {frll} (_⊂_ {pll}
> {_} {_} {_} {ind} lf
> lf₁) (_←⊂ {_} {_} {_} {_} {_} {_} {_} {lind} ic)
> | .(replLL _ (ind +ᵢ
> lind) frll) | refl = ?
> ```
>
> instead of :
>
> ```
> removeCom {frll = frll} (_⊂_ {pll = pll} {ll =
> ll} {ind = ind} lf lf₁)
> (_←⊂ {lind = lind} ic) with (replLL ll ind
> (replLL pll lind frll)) |
> (drepl=>repl+ {frll = frll} ind lind)
> removeCom {frll = frll} (_⊂_ {pll = pll} {ll =
> ll} {ind = ind} lf lf₁)
> (_←⊂ {lind = lind} ic) | .(replLL _ (ind +ᵢ
> lind) frll) | refl = ?
> ```
>
> I wonder if the behavior can be changed.
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
>
>
>
>
>
> --
> Andreas Abel <>< Du bist der geliebte Mensch.
>
> Department of Computer Science and Engineering
> Chalmers and Gothenburg University, Sweden
>
> andreas.abel at gu.se <mailto:andreas.abel at gu.se>
> http://www.cse.chalmers.se/~abela/ <http://www.cse.chalmers.se/~abela/>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
> <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
--
Andreas Abel <>< Du bist der geliebte Mensch.
Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden
andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/
More information about the Agda
mailing list