[Agda] Printing named arguments [Re: Case split creates too many {_}]

[Apostolis Xekoukoulotakis]

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> 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
>
> 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
>>>>>> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170410/5bcb4410/attachment-0001.html>