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

[Andreas Abel]

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/