[Agda] using irrelevant field

[Andreas Abel]

Well, the story is: "Once irrelevant, always irrelevant".  It is like 
with the IO monad in Haskell: once you are in IO, you cannot get out in 
a safe way.

There is an exception:  You can turn an irrelevant contradiction into a 
relevant one:

   -- Empty type
   data \bot : Set where

   makeRelevantEmpty : .\bot -> \bot
   makeRelevantEmpty ()

(You can directly match on irrelevant empty types.)

With proof-irrelevant equality (UIP), probably also Alan Jeffrey's trick

   postulate
      makeRelevantEq : {A : Set}{a b : A} ->
        .(a \equiv b) -> a \equiv b

is sound.

To (2): You could edit a standard library with irrelevance.


P.S.:

   > suc≢0 : ∀ {n} → suc n ≢ 0
   > suc≢0 {suc n} ()
   > suc≢0 {0}     ()

needs no matching on n, it can be simplified to

   suc≢0 : ∀ {n} → suc n ≢ 0
   suc≢0 ()


On 18.03.2014 16:22, Sergei Meshveliani wrote:
> This is about "converting an irrelevant value to relevant".
>
> On Tue, 2014-03-18 at 14:37 +0100, Andreas Abel wrote:
>> The example is rejected since the proof x/=0 is irrelevant in
>> (subEl x x/=0), but f expects it to be relevant.
>>
>> The fix 2. is correct.
>>
>> The other way to fix it is of course to just drop the second argument to
>> f, since it is unused anyway.
>>
>> Probably your example is too simplistic, you want to do something more
>> advanced with irrelevance!?
>
>
> Yes.
>
> (1) Most function _condition_ arguments in any mathematical library need
> to be irrelevant.
>
> (2) It is desirable
>     a) to include irrelevant things to the language standard,
>     b) to use irrelevant things in Standard library.
>
> (3) My DoCon-A library currently uses irrelevant things, but not
> everywhere, so far (I fear of possible complications).
>
> The approach (3) causes that sometimes I need to convert a thing to
> relevant.
> Here is a contrived example:
>
> --------------------------------------------------------------------
> open import Relation.Binary.PropositionalEquality using (_≡_; _≢_)
> open import Data.Product using (_,_; Σ)
> open import Data.Nat     using (ℕ; suc)
>
> record Nonzero : Set where  constructor subEl
>                              field  elem   : ℕ
>                                     .proof : elem ≢ 0
> Nonzero' : Set
> Nonzero' = Σ ℕ (\x → x ≢ 0)  -- relevant version
>
> suc≢0 : ∀ {n} → suc n ≢ 0
> suc≢0 {suc n} ()
> suc≢0 {0}     ()
>
> nz' : Nonzero'               -- example of using Nonzero'
> nz' = (1 , suc≢0)
>
> toRelevant : Nonzero → Nonzero'
> toRelevant (subEl x x≢0) =  (x , x≢0)
> --------------------------------------------------------------------
>
> It is not type-checked.
>
> So far, I agree `relevant' and `irrelevant' parts this way:
> in the intersection I change a relevant argument in a signature to
> irrelevant. And repeat this by transitivity until the checker is
> satisfied.
> (In this approach, Nonzero' needs to be removed).
>
> Is there possible another way to agree the `relevant' and `irrelevant'
> parts?
> In particular, what to do with the above example?
>
> Thanks,
>
> ------
> Sergei
>
>
>
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/