searching in list

[mechvel]

Searching in a list can be expressed via lib-1.2 as

search  :  ∀ {p} {P : Pred A p} → Decidable P → (xs : List A) →
                                                (∃ (\x → P x)) ⊎ (¬ Any P xs)
search P? xs  with any P? xs
...    | yes anyP-xs =   inj₁ (satisfied anyP-xs)
...    | no ¬anyP-xs =   inj₂ ¬anyP-xs 

First, is there a ready function in lib-1.2 to express this? Second, it is more desirable to have (for a setoid)

search  :  ∀ {p} {P : Pred A p} → Decidable P → (xs : List A) →
                                               (∃ (\x → x ∈ xs × P x)) ⊎ (¬ Any P xs)

Has lib-1.2 something for this?

[gallais]

∃ (\x → x ∈ xs × P x)) is essentially Any P xs as find demonstrates.

So you can get that by using any, then cast Dec to a sum using fromDec, and finally map over the first element of the sum using map₁.

[mechvel]

This latter search version is usable and more generic than find, and its implementation needs a wise additional combination of any, fromDec, map₁. So that it probably worth to add this search to the library.

[gallais]

In "Generic Level Polymorphic N-ary Functions", I have

decide : Π[ P ∪ Q ] → Π[ Any P ∪ All Q ]

It seems to also be missing from the stdlib and would also be a fine way to implement this search via fromDec, find & All¬⇒¬Any.

[jamesmckinna]

In "Generic Level Polymorphic N-ary Functions", I have

decide : Π[ P ∪ Q ] → Π[ Any P ∪ All Q ]

It seems to also be missing from the stdlib and would also be a fine way to implement this search via fromDec, find & All¬⇒¬Any.

decide was added in #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?))

  search : ∀ xs → ¬ Any P xs ⊎ ∃ (\x → x ∈ xs × P x)
  search = Sum.map All¬⇒¬Any find ∘ helper

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

[MatthewDaggitt]

I wouldn't be against helper being added to Data.List.Relation.Unary.All. I feel we should avoid using \x → x ∈ xs × P x as much as possible so not too keen on search.

[jamesmckinna]

I wouldn't be against helper being added to Data.List.Relation.Unary.All. I feel we should avoid using \x → x ∈ xs × P x as much as possible so not too keen on search.

Should we call this function (ie: helper) search instead (it's the 'essence' of search in Underwood, Gent and Caldwell "Search Algorithms in type Theory" Theoretical Computer Science 232 (2000) 55–90), and client-side post-processing (as above) can fix up the types to deliver whatever a user such as @mechvel might want instead...?

[mechvel]

Concerning the essence of the subject (which I do not recall/understand now) , let the team decide, and then I would decide how to apply this. My deal is mainly to suggest an issue.

But there is a problem of the English language. My English is not enough to understand may be half of what jamesmckinna writes. I shall be grateful to people if they put sentences somehow in a simpler way.

[jamesmckinna]

Thanks Sergei for the reminder to try to write in simpler language!

[mechvel]

I somehow exaggerated this (a new word for me). At least this latter fragment of

and client-side post-processing (as above) can fix up the types to deliver whatever a user such as @mechvel might want instead...?

remains totally enigmatic for me. ( Anyway I do not need to solve this particular sentence, because the team would make a decision, and then I would see what to do with it).

[jamesmckinna]

Apologies ;again) for having been enigmatic!

My intention was to contrast

• finding a definition which is a good 'fit' with existing definitions in the library
• which nevertheless does not make it difficult for client uses, such as yours, to be available via writing adaptor code

Excessive jargon, and writing in too much haste on my phone, got in the way this time!