[Agda] irrelevancy annotation

[mechvel at scico.botik.ru]

On 2020-12-22 01:04, Carette, Jacques wrote:
> Don't use double-negation.  Instead of Null, use an HasElement 
> data-structure.
> data HasElement : List A → Set α  where
>   has-elem : (x : A) {xs List A} -> HasElement (x ∷ xs)
> 
> Then you need to match on both the list and has-elem enough to reveal
> the actual head.


Thank you. I am going to try the approach.


> I don't know why you want this to be irrelevant though.

Because if it is defined
   head : (xs : List A) → ¬ Null xs → A

then `refl' is not a proof for  head xs nn ≡ head xs nn'.
Many functions start to depend on the witness for a list non-emptiness.
For example, I represent a polynomial in  x  mainly as a list of 
monomials,
with adding certain conditions for ordering and for the coefficients 
being nonzero.
For example,  a*x^3 + b  is represented as
                                    pol ((a , 3) :: (b , 0) :: []) _ _,
where  a, b /= 0#.
Zero polynomial contains [] in its bag.
So the degree function  deg  for a polynomial needs to be   proj₂ ∘ head 
∘ Pol.monomials.
But it is defined only for a nonzero polynomial.
So,  deg  depends on the witness for  ¬ Null monomials.
In algebra, we take it for granted that equal nonzero polynomials have 
equal degree.
Bun with Agda, one needs to explicitly prove and apply the lemma of that
deg (`head') is irrelevant on the non-emptiness witness.


> Are you sure you don't want a Vec instead of a List?  Lists are best 
> understood as
> vectors that have forgotten their length.

?
Never thought of this.
Rather I thought reversely: List looks more basic than Vector.
So, I use my home-made Vector:

   module OfVector {α} (A : Set α) (n : ℕ)
     where
     data Vector : Set α  where
                          vec : (xs : List A) → length xs ≡ n → Vector

Having a bag of (vec xs _), it is possible to use all rich Standard 
library
functionality for  xs : List A.  And conversion to List is in one step.
And there is no need to add a huge functionality for Vector that would
(I expect) actually copy the List functionality.
?

--
SM