[Agda] question on irrelevant argument

[Andreas Abel]

On 20.01.2014 11:53, Sergei Meshveliani wrote:
> 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,

You are never forced to use _ instead of a variable name on the l.h.s.

> because the checker does not allow its usage as
>
>              foo ... nz = ... (nz ...)

On the r.h.s. nz can only used in irrelevant positions, i.e., in 
irrelevant arguments to some functions.

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

If you use _ instead of a variable name on the lhs, the variable is not 
in scope but still available to the unifier.  So Agda might sometimes 
use it to fill in a missing irrelevant argument.

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

\bot-elem-irr is such a function with irrelevant argument.

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