On filter and boolFilter

[andreasabel]

In Data.List.Base, I find

filter : ∀ {P : Pred A p} → Decidable P → List A → List A
boolFilter : (A → Bool) → List A → List A

the latter being deprecated.

I am a bit puzzled by this choice. The current version of filter is simply

filter p = boolFilter (isYes \o p)

I don't question that this specialization gets its own name (as I am generally in favor of fat libraries). However:

1. In analogy to the naming conventions of Haskell and OCaml, shouldn't filter be the Bool version?

filter : (A → Bool) → List A → List A

2. The current filter function (which could be called decFilter or filterDec) requires a decidable predicate rather than a simple boolean test, but then throws away the evidence. Shouldn't it rather retain the evidence?

decFilter : (p : Decidable P) -> List A -> \Sigma (List A) (All P)

Analogous cases: partition, span, break, takeWhile, dropWhile.

Design baseline: Don't ask for data that you don't use to produce the result.

See also #263.

[MatthewDaggitt]

They were changed to use decidable predicates a while back, as the boolean versions were very difficult to state and prove properties about. Furthermore as most of the library is set up to use decidability rather than boolean functions they didn't interface well with other code.

The problem with your proposed definition in 2. is that it makes much harder to chain filter with other list functions as you then have to explicitly project out the actual list. I guess it's the tension between efficiency and making it easier to work with.

Having said that @laMudri is proposing to reimplement these functions using the new definition of Decidability in #932 which will avoid generating the proof component of the decidability result. This I think will provide the best of both worlds?

[andreasabel]

the boolean versions were very difficult to state and prove properties about.

Not sure I agree. From a high-level perspective, one should be able to inherit the results for definition 1 (Bool) from definition 2 (Dec). Given a boolean function f : A -> Bool, I can get a corresponding predicate P : A -> Set that is decidable Dec P. Thus, should be able to implement boolFilter in terms of decFilter and get the properties of boolFilter from those of decFilter without doing further induction.

However, I agree that a redesign could happen in connection with #932.

[MatthewDaggitt]

Okay revisiting several years later. Apologies for the delay @andreasabel.

I've been brought back here by the module dependency graph issue. In particular by the fact that requiring decidable predicates requires you to import .Properties modules when sometimes you don't want to. To summarise my position:

• I'm sold on the idea of having both boolean and decidable variants.
• I'm sold on implementing the boolean variants in terms of the decidable variants.
• While I understand where you're coming from, I'm not sold on changing the return type of the decidable variant to include the proof, for the reasons I previously stated above. Namely, it makes it very difficult to compose operations. As an example consider dropWhile and takeWhile from Data.List.Base. takeWhile would presumably return a pair of list and proofs whereas dropWhile would be return a simple list of elements. Thus you couldn't easily do a dropWhile after a takeWhile for example.

As for the naming I'd guess I'd prefer not to make a breaking change if possible, so how about appending a ᵇ, eg. filterᵇ?

[MatthewDaggitt]

I should add that it is going to require lifting T? from Data.Bool.Properties to Data.Bool.Base... which I'm working on talking myself round to, despite the fact that it violates my dearly held beliefs that decidability proofs should live in Properties files. After all it's hardly really a proof 😅

[JacquesCarette]

I was thinking of suggesting that we put the definition of relations and predicates in Foo.Relation (without going down the arity rabbit hole), instead of Foo.Base. That would leave .Base proof-free. And relations do seem somewhat different, at least semantically, than pure proofs of properties. [What I mean is that the inductive types that we call relations, do seem of a different nature.]

[MatthewDaggitt]

Can you give some concrete examples of what would go in Foo.Relation?

[andreasabel]

As for the naming I'd guess I'd prefer not to make a breaking change if possible, so how about appending a ᵇ, eg. filterᵇ?

That sounds fine. I am a bit removed from this issue now, so I do not have a strong opinion atm. boolFilter could also stay (unless the b-superscript notation is becoming a naming convention).
Maybe the only thing I am thinking strongly about is that the bool-variants should not disappear from the API altogether.

[JacquesCarette]

(I think I've answered a similar query on a different issue, but it's better to be thorough) What would go in Foo.Relation? The definition of data types that represent (unary, binary, ..., n-ary) relations. Perhaps some basic functions on them. Most definitely not any theorems about them.

The same way we separate data-structures and basic functions on them from their properties (and bundles). Generalized to encompass relations.

[MatthewDaggitt]

Hmm so what about basic operations over those data types? For example nearly every data type has a map operation. They couldn't all live in the same module right?

What about relations that pretty much require module parameters for their syntax to work sensibly, e.g. pointwise equality over lists?