Deprecate Data.List.Relation.Unary.All.Properties.takeWhile⁻

[jamesmckinna]

This is a coda to #2520 / #2521 : the type of takeWhile⁻ is insufficiently general, and generalising it makes the proof trivially delegate to that of all-takeWhile; another instance of 'non-linear bindings considered harmful' ...

NB. UPDATED: following @MatthewDaggitt 's suggestions below, can now ignore first three items here

• not sure how to record this in CHANGELOG: under Minor improvements?
• possible deprecation of takeWhile⁻ now possible? or else of all-takeWhile?
• not breaking, but not clear whether the generalisation may lead to unsolved metas errors downstream?
• any other similar refactorings possible?

[MatthewDaggitt]

To be honest I would recommend just deprecating takeWhile⁻ entirely, rather than make this change at all.

1. It's a trivial generalisation of all-takeWhile
2. It's really not the correct name for that lemma under the style guide, as it doesn't take in an argument of the form All P (takeWhile ...),

not sure how to record this in CHANGELOG: under Minor improvements?

If we were keeping it I would explicitly say what the generalisation is under "Minor improvements". I think there's probably no need to mention the delegation of the proof, as that's not something that is going to affect users?

possible deprecation of takeWhile⁻ now possible? or else of all-takeWhile?

See above.

not breaking, but not clear whether the generalisation may lead to unsolved metas errors downstream?

I agree this could lead to unsolved metas. But irrelevant if we just deprecate it 😄

[jamesmckinna]

UPDATED: now opt for deprecation

Of these only the last point now stands further consideration:

• type of dropWhile⁻ is similarly not consistent with style-guide
• types of dropWhile⁺ and takeWhile⁺ are insufficiently general: without any relationship between P and Q, these are map properties of All P wrt the sublist/prefix/suffix relations
• if generalised appropriately, then at least the existing all-takeWhile, if not takeWhile⁺, could even be deprecated as well.

Accordingly will convert to DRAFT while I figure this out. DONE. See most recent commit.

UPDATED: I've rolled back to the original simple deprecation.

[jamesmckinna]

If there was a button "Convert PR to an issue", I'd hit it, under a title like "overhaul theory of takeWhile and dropWhile for All", because it feels as though this is really a patch on something which is actually broken (wrt our style-guide precepts, and to the 'right' level of abstraction/generalisation), and needs a more serious fix?

[jamesmckinna]

After a bit more detective work...
Data.List.Relation.Binary.Sublist.Setoid.Properties.takeWhile-⊆ : ∀ xs → takeWhile P? xs ⊆ xs
so @JacquesCarette 's comment above has extra force... should we move all the properties of *While wrt All out of All.Properties altogether? (not withstanding... ahem, the recently merged #2521 ...;-))

[MatthewDaggitt]

should we move all the properties of *While wrt All out of All.Properties altogether? (not withstanding... ahem, the recently merged #2521 ...;-))

Sorry, I'm afraid I don't quite understand why we would do this and where would we put them?

[jamesmckinna]

@MatthewDaggitt I guess I'd been thinking, after @JacquesCarette 's comment:

• these properties are consequences of a general Sublist/Subset property of All (discussion above about this), so perhaps should better be rephrased in terms of such;
• the general drift of other recent discussion (with you on [ refactor ] Possible refactoring of #2509 / #2513 ? #2517 ) has been to avoid dragging additional dependency on Sublist/Subset into the imports of All.Properties
• ...

As to where we'd put them, probably in Sublist.Properties where we already have takeWhile-⊆ and dropWhile-⊆ as consequences of the corresponding Heterogeneous versions...?

But it doesn't affect this PR, so happy to punt this discussion downstream. HTH.

[MatthewDaggitt]

As to where we'd put them, probably in Sublist.Properties where we already have takeWhile-⊆ and dropWhile-⊆ as consequences of the corresponding Heterogeneous versions...?

Personally it would be very weird for me for All properties to be found under Sublist... but yes, happy to move it to a downstream discussion

[JacquesCarette]

The changes in this PR make sense to me.

The discussion, less so. I'm having a hard time extracting exactly what is being proposed from the thread.

[jamesmckinna]

@JacquesCarette writes:

The discussion, less so. I'm having a hard time extracting exactly what is being proposed from the thread.

At present: nothing beyond what is in the current commits, which I don't plan to add to.

In future, the 'issue(s)' identified above may broadly be covered by [ DRY ]:

• should properties of *While wrt All and Any be proved directly, as now (and hence be located under Properties of Data.List.Relation.Unary.{All|Any}
• or else as consequences of a general functoriality (co- for Any, contra- for All) wrt Subset/Sublist

Discussion:

• the first alternative is (basically) the status quo ante, so nothing as such is proposed (and indeed, for this PR, nothing further is towards these downstream issues)
• the second flows from your comment about functoriality (see [ refactor ] Functoriality of Data.List.Relation.Binary.Sublist|Subset wrt All and Any #2525 for separate discussion, lifted out from here), but potentially carries the additional cost of a more complex dependency graph, or else things living in not-quite-the-right place, or refactoring to make the functoriality properties Core, so that their import can be uncoupled from the various other 'right places' where things do/might/should live.

Followup discussion to #2525 ?

[JacquesCarette]

Right - so the discussion should be moved to an issue, as this is ready to be merged, which I will do now.