Add `delete` to `Data.List.Base`?

[mechvel]

Consider

delete : (p? : Decidable P) → List A → List A
                                             -- delete the first x such that P x

What standard library has for this?

[gallais]

I don't think so. You could use Any's _─_ together with Any's any.

[mechvel]

Any._-_ is good. But the above delete is not given Any P xs, so that delete p? xs sometimes returns xs. May be delete is worth adding, I do not know.

[MatthewDaggitt]

@mechvel as always feel free to open a PR.

[jamesmckinna]

Cf. #989 All.decide was added in https://github.com/agda/agda-stdlib/pull/1595 so you could in v2.1 define

module _ (P? : Decidable P) where

  private
    helper : ∀ xs → All (∁ P) xs ⊎ Any P xs
    helper = All.decide (Sum.swap ∘ (Dec.toSum ∘ P?))

  delete : List _ → List _
  delete xs with helper xs
  ... | inj₁ _ = xs
  ... | inj₂ p = xs Any.─ p

But it's not clear (to me, at least) which, if any, of helper or delete belongs in the library, by contrast with All.decide? Suggest closing this issue?

[mechvel]

Personally I do not know. Currently I use my home-made functions

delP :  {xs : List A} → Any P xs → List A
delP {_ ∷ xs} (here _)        =  xs
delP {x ∷ xs} (there anyP-xs) =  x ∷ (delP anyP-xs)

delBy : (P? : Decidable P) → List A → List A
                                -- Delete the first x in xs such that P x, or return  xs  if there is not such x.
delBy _  []        =  []
delBy P? (x ∷ xs)  with P? x
... | yes _ =  xs
... | no _  =  x ∷ (delBy P? xs)

If the standard library announces an adequate replacement for them, then I would use the standard functions. I also have several proofs for these functions:

delBy-preserves∈ :  (P? : Decidable P) → ∀ {x xs} → ¬ P x → x ∈ xs → x ∈ (delBy P? xs)

delBy-preserves-All :  (P? : Decidable P) → ∀ {β} (Q : Pred A β) {xs : List A} → All Q xs →
                                       All Q (delBy P? xs)
  
length-delBy-for-any :  (P? : Decidable P) → ∀ {xs} → Any P xs → length (delBy P? xs) ≡ pred (length xs)

and some others.

[jamesmckinna]

... Currently I use my home-made functions

delP :  {xs : List A} → Any P xs → List A
delP {_ ∷ xs} (here _)        =  xs
delP {x ∷ xs} (there anyP-xs) =  x ∷ (delP anyP-xs)

You should find (and be able to prove ;-)) that this is extensionally equivalent to Any._─_ as previously suggested, so it's not obvious to me that you gain anything from this (slightly more direct) definition, which is the fusion of the two functions removeAt and index defining the library version...

[mechvel]

You should find (and be able to prove ;-)) that this is extensionally equivalent to Any.─ as previously suggested, so it's not obvious to me that you gain anything from this slightly more direct) definition, which is the fusion of the two functions removeAt and index defining the library version...

First, this delP was used under lib-2.0, and I have now an impression that Any._─_ will appear after lib-2.1-rc1. Second, it is sometimes difficult to understand standard functions, it takes effort. So, my application contains several functions that can be replaced with standard ones.

functions removeAt and index defining the library version...

Is this index that returns a number in Fin ? Indexing members of a list with numbers? Generally I have an impression that indexing a list with numbers needs to be avoided. At least my large application avoids it, avoids index , avoids Fin , and feels all right. Also suppose that I apply the fusion of the two functions removeAt and index to replace my delP. As to me, the thing will not look more clear than the home-made implementation for delBy, delP. I doubt.

[mechvel]

Sorry, index can mean in stdlib something different from a number. It may be a proof (i : x ∈ xs) for membership to a list.

[MatthewDaggitt]

I would be happy to have delBy added to Data.List.Base under the name deleteFirst.

As @jamesmckinna says, delP already exists.

@jamesmckinna I'm not so keen on your version of delete as it appears to traverse the list twice?

[mechvel]

Let the team decide. Anyway, double reversing (if any) will be bad here. Because deleteFirst will be run by interpreter or in executable, and it is easy to avoid double reversing.

[jamesmckinna]

Agree with @MatthewDaggitt that

• the proposed delete should better be named deleteFirst
• the specimen implementation I offered is clearly excessive (written while I was thinking about #989 and trying to exploit helper there), while @mechvel 's delBy is a 'clean' definition, but I would prefer the following #2359 -style:

deleteFirst : (P? : Decidable P) → List A → List A
                                -- Delete the first x in xs such that P x, or return  xs  if there is not such x.
deleteFirst _  []        =  []
deleteFirst P? (x ∷ xs)  with does (P? x)
... | true =  xs
... | false  =  x ∷ (deleteFirst P? xs)

[mechvel]

Following jamesmckinna, I consider replacing my delP with Data.List.Relation.Unary.Any ._─_ :

_─_ : {P : Pred A p} → ∀ xs → Any P xs → List A
xs ─ x∈xs = removeAt xs (index x∈xs)

But I see now that index indeed finds a Number index in (Fin ...) . So, _─_ first finds the number index for x , and then applies removeAt xs (index x∈xs) . Do I understand correct that for xs = [0 .. n] = upTo n and n∈xs : n ∈ xs the call xs ─ n∈xs takes 2*n steps to evaluate? If so, then it is better to change the implementation of _─_ to the sample of

delP {_ ∷ xs} (here _)        =  xs
delP {x ∷ xs} (there anyP-xs) =  x ∷ (delP anyP-xs)

Because the latter takes n steps in the above example, and the function _─_ is not only for proofs, but also for interpreted evaluation and for running in executable. ?