[Agda] Pattern-matching operation order

[Andreas Abel]

On Feb 24, 2010, at 2:54 AM, Dan Licata wrote:

> On Feb23, Ulf Norell wrote:
>> On Tue, Feb 23, 2010 at 6:34 PM, Andreas Abel <andreas.abel at ifi.lmu.de 
>> >wrote:
>>
>>> Thanks, Ulf, for the explanation.
>>>
>>> Is it fair to say that pattern matching works for all pattern  
>>> inductive
>>> families, but not for those where indices are computed by  
>>> (recursive)
>>> functions?
>>>
>>
>> It still works. For instance, as long as the thing you match  
>> against have a
>> type where the index is a variable there are no problems.
>
> Also, being a pattern inductive family isn't a sufficient condition:
> there are times when you can't pattern-match on an inhabitant of a
> pattern inductive family. E.g.
>
> f : {A : Set} {n : Nat} {f : Nat -> Nat} -> Vec A (f n) -> Unit
> f v = {!v!}
>
> you can't match on 'v'.

Agreed, but I would not expect that anything could be done in this  
really hopeless case (since you cannot match on f : Nat -> Nat).   
Neither would I expect miracles for

l' : {A : Set}{n : ℕ} -> Vec A (n + 0) -> ℕ
l' [] = zero  -- ERROR
l' (a ∷ v) = l' v

when + is defined by recursion on the first argument.  However, since  
you can match on n first, this goes through:

l : {A : Set}(n : ℕ) -> Vec A (n + 0) -> ℕ
l zero [] = zero
l (suc n) (a ∷ v) = l n v

Cheers,

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41