[Agda] function application in index positions

[Andreas Abel]

On 05.02.2013 12:09, Peter Divianszky wrote:
> On 02/04/2013 06:17 PM, Andreas Abel wrote:
>> On 01.02.2013 21:32, Peter Divianszky wrote:
>>
>>> data Even : ℕ → Set where
>>>    double : ∀ n → Even (n + n)
>>
>> I think non-pattern indices like this one should be forbidden in the
>> first place.  Instead you should have to write
>>
>>    data Even (m : N) : Set where
>>      double : forall n -> (n + n == m) -> Even m
>
>  From a practical viewpoint, isn't the first data definition is more
> compact having exactly the same semantics?

Yes, but the second definition requires the user to place the equality n 
+ n == m.  If we were to introduce the first def. as sugar for the 
second def., it would not be clear where to place the equality proof. 
It seems better that the user writes this himself.

>>> Is this documented / should I open a ticket?
>>
>> I think the current liberty leads people to believe the type checker
>> could handle arbitrary indices, which is not true and leads to error
>> messages which are harder to understand than an outright
>>
>>    "double's type is illegal because the unification problem
>>
>>       n + n == expression
>>
>>     is not solvable in general"
>
> A better error message would help a lot!

Well, but currently def. 1 is not illegal, the price has only to be paid 
when one wants to use it.

Cheers,
Andreas


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