[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