[Agda] function parameters similar to data parameters

[Andreas Abel]

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.  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.

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.

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
>>
>
>
>
>
>
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/