[Agda] Q: Matching Fin, Bug?

[Christoph Herrmann]

Hi James,

I must admit, I have read about this long before already in a manual,
that the match is only on the topmost constructor and then
traverses down, so it is in fact the zero that is not possible
any more in the case Fin 0.

Sorry, but I have just forgot about it ... and I have completely
ignored that we have in fact a nested pattern match here,
because mentally I view numbers as individual elements.

Best wishes




On 1 Oct 2009, at 20:58, James McKinna wrote:

> Christoph,
>
> as Conor and Liang-Ting have already said, but not explained, it is in
> general *not* possible to infer that a pattern match covering is total
> in the presence of empty types [Conor, myself and Healf Goguen have a
> paper about this...
>    http://www.strictlypositive.org/concon.ps.gz
> ]
> so the user (and the typechecker) need to supply evidence that  
> indeed a
> given match is not possible. What is strange is that that evidence is
> always canonical --- hence the () syntax for it (we used to write
> "bomb!", or rather, the latex symbol for a bomb) --- but you *do* need
> to supply it. Once the checker knows that (you think) the type is  
> empty,
> it is easy for them to solve
> a) the inhabitation problem for the result type, given an element of  
> the
> empty type
> b) the underlying unification problem, with the hint that it is not
> solvable...
>
> ... hope this helps,
>
> James.
>
>
> Christoph Herrmann wrote:
>> Hi,
>>
>> maybe I'm doing something wrong or there is a bug, but in the
>> following program
>> Agda complains about incomplete pattern matching:
>> ---
>> module T where
>>
>> open import Data.Fin
>>
>> f : Fin 3 → Fin 3
>> f zero = suc zero
>> f (suc zero) = suc (suc zero)
>> f (suc (suc zero)) = zero
>> ---
>>
>> Best Wishes

--
  Dr. Christoph Herrmann
  University of St Andrews, Scotland/UK
  phone: office: +44 1334 461629, home: +44 1334 478648
  email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
  URL:   http://www.cs.st-andrews.ac.uk/~ch

  The University of St Andrews is a charity registered in Scotland: No  
SC013532