New Maybe Unary definition

[guilhermehas]

I created this definition because it is a new kind of relation different from the other definitions we already have. It is the same as Data.Sum.Relation.Unary.All when used with the unit type.

[Taneb]

Do you have a specific use-case in mind for this definition?

[guilhermehas]

Yes, I needed this data structure in my linear algebra library:

VecPivotPos : (xs : Vector F n) (p : Fin n ⁺) → Set (ℓ₁ ⊔ ℓ₂)
VecPivotPos xs    ⊤⁺ = Lift ℓ₂ (AllZeros xs)
VecPivotPos xs [ p ] = Lookup≢0 xs p

[jamesmckinna]

Can this be defined directly by pattern matching, via Data.Maybe.Base.maybe?

[guilhermehas]

Can this be defined directly by pattern matching, via Data.Maybe.Base.maybe?

Yes, it can.

[jamesmckinna]

Can this be defined directly by pattern matching, via Data.Maybe.Base.maybe?

Yes, it can.

As a followup, then, some more questions (REVISED in the light of my looking again at Unary relations on Maybe):

• what's the added value in this definition?
• [DELETED]

But, given that case analysis on Maybe, either actually, or proxied via the constructors you introduce here, would drive everything (?) when using this definition, I'm still sceptical about the added value, even pragmatically. But others may disagree.

[MatthewDaggitt]

I agree with @jamesmckinna. My personal feeling is that this relation isn't sufficiently "natural" to be added to the library...

[guilhermehas]

I agree with @jamesmckinna. My personal feeling is that this relation isn't sufficiently "natural" to be added to the library...

I think that this definition is more natural than Data.Maybe.Relation.Unary.All, because it is what we got in Data.Sum.Relation.Unary.All if we substitute B to Unit.

In addition, I agree with @jamesmckinna about the problem that every time that we create a new data structure, we have to prove everything from scratch. While when we use maybe to create the type, we have a lot of theorem for free.

[MatthewDaggitt]

I think that this definition is more natural than Data.Maybe.Relation.Unary.All, because it is what we got in Data.Sum.Relation.Unary.All if we substitute B to Unit.

I'm afraid that just because we can substitute something into an existing definition to get a relation, doesn't make that relation natural.

Yes, I needed this data structure in my linear algebra library:

Looking at the problem, I'm not very convinced by the proposed use case either. I think your code would be expressed much more neatly using a sum type that either returns a proof that all entries are zero, or alternatively a Fin that points to a non-zero entry.

Thank you for the proposal, but I think in this particular case we're not going to accept this unless a more convincing use case appears. Feel free to reopen the issue if you come across one!