[Agda] function parameters similar to data parameters

[Peter Divianszky]

Thanks for the investigation.

On 24/11/2012 19:31, Andreas Abel wrote:
> Well, I think that the version with omitting the telescope args,
>
>    add (x : Nat) : Nat -> Nat
>    add zero    = x
>    add (suc y) = suc (add y)
>
> is confusing because, while add is written with one argument, it has to
> be used with two arguments.

Indeed it is a bit confusing, and a bit even more confusing for mixfix 
operators. The same holds for sections but there the syntax give more 
notice that extra arguments are added.

>  The version with writing the telescope args
>
>    add (x : Nat) : Nat -> Nat
>    add x zero    = x
>    add x (suc y) = suc (add x y)
>
> does not have much advantage over just writing
>
>    add : (x : Nat) -> Nat -> Nat
>
> except that it could fix the problem with the hidden argument you
> describe.  But it would complicate the implementation, because one needs
> extra checks that the first argument of add is always the variable x.

The extra check would be a good feature, I would use telescopes 
primarily to get the extra check.

> Data types allow telescopes since there is a difference, semantically,
> between parameters and indices of the data type.  And because there is
> some magic omitting data parameters in constructors.

I see.

By the way, when I use sections with 'data' I have to use two 
indentations. To avoid this a lightweight syntax would be useful like

   _≤_ : ℕ → ℕ → ℕ
   z≤n : ∀ {n}                 → zero  ≤ n
   s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n

but I see that it would be a big change. One could not search for 'data' 
keywords but syntax colouring and semantic search could help.

I guess you also considered already the automatic addition of some 
hidden arguments like

   _≤_ : ℕ → ℕ → ℕ
   z≤n :         zero  ≤ n
   s≤s : m ≤ n → suc m ≤ suc n

which would simplify the definition too.
Syntax colouring would help to read this also. Maybe these discussions 
are relevant in connection with some improvement of the interactive 
interface.

> Instead of adding the telescope syntax for functions, I think it would
> be worth investigating how to improve the treatment of hidden arguments.
>   (Lazy instead of eager insertion...)
>
> Cheers,
> Andreas
>
> On 23.11.12 9:27 AM, Peter Divianszky wrote:
>> On 22/11/2012 11:46, Andreas Abel wrote:
>>> On 19.11.2012 09:57, Peter Divianszky wrote:
>>>> Now this is possible:
>>>>
>>>> ---------------------------------------------------
>>>> module _ {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m)) where
>>>>    ℕ-elim : ∀ n → P n
>>>>    ℕ-elim zero = z
>>>>    ℕ-elim (suc n) = s _ (ℕ-elim n)
>>>> ---------------------------------------------------
>>>>
>>>> My question is, could we write
>>>>
>>>> ---------------------------------------------------
>>>> ℕ-elim {P : ℕ → Set} (z : P zero) (s : ∀ m → P m → P (suc m))
>>>>         : ∀ n → P n
>>>> ℕ-elim zero = z
>>>> ℕ-elim (suc n) = s _ (ℕ-elim n)
>>>> ---------------------------------------------------
>>>
>>> Is this so much more succinct than the section?  I have wondered about
>>> telescopes for function definitions myself before, but how does this
>>> scale to mutual functions?
>>
>> I'm quite happy with sections, but if I go on and use them, I'll end up
>> one section per every single function at the end.
>> In that case telescopes look nicer.
>>
>> Mutual functions are not that common.
>>  From another point of view, we have the same situation with data with
>> telescopes and mutual data I think.
>> Why not treat data and function in the same way regarding telescopes?
>>
>>> We could maybe allow telescopes in mutual with
>>>
>>>    mutual tel
>>>      decls
>>>
>>> being a shorthand for
>>>
>>>    module _ tel where
>>>      mutual
>>>        decls
>>>
>>
>>
>>
>>
>>
>>
>