[Agda] question on irrelevant argument

[Andreas Abel]

 > Generally, there are many situations in which I can write a type-checked
 > Agda program only by a lucky occasion.
 >
 > I tried
 >          foo2 _ zero    _  =  ⊥-elim-irr {!!}

If you use _ instead of naming your argument, you cannot refer to it 
later.  It appears as

   .nz

which does not mean "irrelevant nz" but "not in scope: nz".

Unfortunately, the second can be misread for the first...

If an argument is *irrelevant*, this does not mean that its value could 
not be bound to a variable!  Using _ is generally not a good idea, only 
if it is actually not *used*

Note: irrelevant =/= unused!

Cheers,
Andreas

On 19.01.2014 20:45, Sergei Meshveliani wrote:
> On Sun, 2014-01-19 at 15:26 +0100, Ulf Norell wrote:
>> You can define an irrelevant version of ⊥-elim which you can use in
>> foo2 and foo3:
>>
>>
>> ⊥-elim-irr : .(x : ⊥) → ∀ {a}{A : Set a} → A
>> ⊥-elim-irr ()
>>
>
> Thank you.
>
> I tried several attempts with this. Finally I discover that this one is
> type-checked:
>
>    foo2 : (m n : ℕ) → .(nz : n ≢ zero) → ℕ
>    foo2 _ (suc n) _  =  n
>    foo2 _ zero    nz =  ⊥-elim-irr (nz PE.refl)
>
> Generally, there are many situations in which I can write a type-checked
> Agda program only by a lucky occasion.
>
> Thus, I tried in this example
>
>          foo2 _ zero _ =  ⊥-elim-irr ({!!} PE.refl)
>
> under emacs, and   C-c C-a.  This does not help!
> I tried
>          foo2 _ zero    _  =  ⊥-elim-irr {!!}
>
> This occurs lucky. Here  C-c C-a  shows  "(.nz PE.refl)"  -- some hint.
>
> It is not still type checked! Then I change here  ".nz"  to  "nz" :
> "Not in scope:  nz".
>
> Then I replace there  "_ ="  with  "nz _ =".
>
> I expected that it will report that  nz  declared as irrelevant and
> cannot be used this way.
> But it is type-checked!
> -- unlike with  ⊥-elim.
>
> Regards,
>
> --------
> Sergei
>
>
>>
>>
>> On Sun, Jan 19, 2014 at 2:50 PM, Sergei Meshveliani <mechvel at botik.ru>
>> wrote:
>>          Please,
>>          how to fix  foo2, foo3  shown below?
>>
>>          ----------------------------------------------------------------
>>          open import Relation.Binary.PropositionalEquality as PE using
>>          (_≡_; _≢_)
>>          open import Data.Empty using (⊥-elim)
>>          open import Data.Nat   using (ℕ; module ℕ)
>>
>>          open ℕ
>>
>>          foo : (m n : ℕ) → n ≢ zero → ℕ             -- this works
>>          foo _ (suc n) _  =  n
>>          foo _ zero    nz =  ⊥-elim (nz PE.refl)
>>
>>
>>          foo2 : (m n : ℕ) → .(n ≢ zero) → ℕ
>>          foo2 _ (suc n) _ =  n
>>          foo2 _ zero    _ =  ⊥-elim (u PE.refl)     -- is not
>>          type-checked
>>                              where
>>                              u : zero ≢ zero
>>                              u = _
>>          {-
>>          foo3 : (m n : ℕ) → .{nz : n ≢ zero} → ℕ
>>          foo3 _ (suc n) {_} =  n
>>          foo3 _ zero    {_} =  ⊥-elim (u PE.refl)      -- is not
>>          type-checked
>>                                where
>>                                u : zero ≢ zero
>>                                u = {!!}
>>          -}
>>          ---------------------------------------------------------------------
>>
>>          The checker   (of  development Agda of January 8, 2014)
>>
>>          does not allow to skip the `zero' branch, nor to set () there,
>>          nor to apply  ⊥-elim
>>          (nz  is rejected for  u,  as well as '_').
>>
>>          Thanks,
>>
>>          ------
>>          Sergei
>>
>>          _______________________________________________
>>          Agda mailing list
>>          Agda at lists.chalmers.se
>>          https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>