[Agda] question on irrelevant argument

[Sergei Meshveliani]

On Sun, 2014-01-19 at 22:49 +0100, Andreas Abel wrote:
>  > 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!
> 

I see.
In many situations I am forced to set '_' for irrelevant argument,
because the checker does not allow its usage as 

            foo ... nz = ... (nz ...)

Here '_' instead of  nz  means, probably that  
"it is used some value of the corresponding type".

This example with  ⊥-elim-irr  is the first case that breaks this
behavior.

Regards,

------
Sergei


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