Skip to content

Improve Data.List.Base (fix #2359; deprecate use of with #2123) #2365

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
MatthewDaggitt merged 4 commits into from
Apr 22, 2024
Merged

Improve Data.List.Base (fix #2359; deprecate use of with #2123) #2365

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c4916a3
refactor towards `if_then_else_` and away from `yes`/`no`
jamesmckinna Apr 15, 2024
76afe8a
reverted chnages to `derun` proofs
jamesmckinna Apr 17, 2024
5ae64d3
undo last reversion!
jamesmckinna Apr 17, 2024
f6673bd
layout
jamesmckinna Apr 22, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
31 changes: 11 additions & 20 deletions src/Data/List/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,45 +369,37 @@ removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i

takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
takeWhile P? [] = []
takeWhile P? (x ∷ xs) with does (P? x)
... | true = x ∷ takeWhile P? xs
... | false = []
takeWhile P? (x ∷ xs) = if does (P? x) then x ∷ takeWhile P? xs else []

takeWhileᵇ : (A → Bool) → List A → List A
takeWhileᵇ p = takeWhile (T? ∘ p)

dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
dropWhile P? [] = []
dropWhile P? (x ∷ xs) with does (P? x)
... | true = dropWhile P? xs
... | false = x ∷ xs
dropWhile P? (x ∷ xs) = if does (P? x) then dropWhile P? xs else x ∷ xs

dropWhileᵇ : (A → Bool) → List A → List A
dropWhileᵇ p = dropWhile (T? ∘ p)

filter : ∀ {P : Pred A p} → Decidable P → List A → List A
filter P? [] = []
filter P? (x ∷ xs) with does (P? x)
... | false = filter P? xs
... | true = x ∷ filter P? xs
filter P? (x ∷ xs) = let xs′ = filter P? xs
in if does (P? x) then x ∷ xs′ else xs′

filterᵇ : (A → Bool) → List A → List A
filterᵇ p = filter (T? ∘ p)

partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
partition P? [] = ([] , [])
partition P? (x ∷ xs) with does (P? x) | partition P? xs
... | true | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)
partition P? [] = [] , []
partition P? (x ∷ xs) = let ys , zs = partition P? xs
in if does (P? x) then (x ∷ ys , zs) else (ys , x ∷ zs)

partitionᵇ : (A → Bool) → List A → List A × List A
partitionᵇ p = partition (T? ∘ p)

span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
span P? [] = ([] , [])
span P? ys@(x ∷ xs) with does (P? x)
... | true = Product.map (x ∷_) id (span P? xs)
... | false = ([] , ys)
span P? [] = [] , []
span P? ys@(x ∷ xs) = if does (P? x) then Product.map (x ∷_) id (span P? xs) else ([] , ys)


spanᵇ : (A → Bool) → List A → List A × List A
Expand Down Expand Up @@ -458,9 +450,8 @@ wordsByᵇ p = wordsBy (T? ∘ p)
derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A
derun R? [] = []
derun R? (x ∷ []) = x ∷ []
derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs
... | true | ys = ys
... | false | ys = x ∷ ys
derun R? (x ∷ xs@(y ∷ _)) = let ys = derun R? xs
in if does (R? x y) then ys else x ∷ ys

derunᵇ : (A → A → Bool) → List A → List A
derunᵇ r = derun (T? ∘₂ r)
Expand Down
30 changes: 15 additions & 15 deletions src/Data/List/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -943,13 +943,13 @@ module _ {P : Pred A p} (P? : Decidable P) where
filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
filter-all {[]} [] = refl
filter-all {x ∷ xs} (px ∷ pxs) with P? x
... | no ¬px = contradiction px ¬px
... | true because _ = cong (x ∷_) (filter-all pxs)
... | false because [¬px] = contradiction px (invert [¬px])
... | true because _ = cong (x ∷_) (filter-all pxs)

filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
filter-notAll (x ∷ xs) (here ¬px) with P? x
... | false because _ = s≤s (length-filter xs)
... | yes px = contradiction px ¬px
... | false because _ = s≤s (length-filter xs)
... | true because [px] = contradiction (invert [px]) ¬px
filter-notAll (x ∷ xs) (there any) with ih ← filter-notAll xs any | does (P? x)
... | false = m≤n⇒m≤1+n ih
... | true = s≤s ih
Expand All @@ -965,8 +965,8 @@ module _ {P : Pred A p} (P? : Decidable P) where
filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
filter-none {[]} [] = refl
filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
... | false because _ = filter-none ¬pxs
... | yes px = contradiction px ¬px
... | false because _ = filter-none ¬pxs
... | true because [px] = contradiction (invert [px]) ¬px

filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
filter P? xs ≡ xs
Expand All @@ -977,13 +977,13 @@ module _ {P : Pred A p} (P? : Decidable P) where

filter-accept : ∀ {x xs} → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
filter-accept {x} Px with P? x
... | true because _ = refl
... | no ¬Px = contradiction Px ¬Px
... | true because _ = refl
... | false because [¬Px] = contradiction Px (invert [¬Px])

filter-reject : ∀ {x xs} → ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
filter-reject {x} ¬Px with P? x
... | yes Px = contradiction Px ¬Px
... | false because _ = refl
... | true because [Px] = contradiction (invert [Px]) ¬Px
... | false because _ = refl

filter-idem : filter P? ∘ filter P? ≗ filter P?
filter-idem [] = refl
Expand Down Expand Up @@ -1021,13 +1021,13 @@ module _ {R : Rel A p} (R? : B.Decidable R) where

derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
derun-reject {x} {y} xs Rxy with R? x y
... | yes _ = refl
... | no ¬Rxy = contradiction Rxy ¬Rxy
... | true because _ = refl
... | false because [¬Rxy] = contradiction Rxy (invert [¬Rxy])
Copy link
Collaborator

@JacquesCarette JacquesCarette Apr 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this better? Naively the previous version 'looked' better.

Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 16, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

See #2149 but for a TL;DR justification: I have never liked the asymmetry of having case branches which use constructors which mix different synonyms, such as true because _ with no ¬p... especially because in each such case here, and for the bonus of a less eager evaluation semantics (and making sure each branch is 'equally' lazy in that aspect), such things can be replaced by an appeal to invert.

Since this PR is part of a suite aimed at removing unnecessary with, I might suggest, in the spirit, if not the letter of #2149 that we eventually do away with all with-based analysis of proofs of Dec... but this PR exhibits a half-way house which is more 'uniform' wrt both syntax and evaluation...?

Copy link
Collaborator

@JacquesCarette JacquesCarette Apr 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sure, inconsistent branches are bad - but here they were doing yes / no which are consistent. The drawback to the expansion is you have to use invert now, and didn't have to before. (I don't believe in cross-function uniformity, that seems like overkill and even counter-productive at times.)

So I'm happy with many of the other changes, it's this particular one which puzzles me. (I'm not saying you're wrong, merely that I'm not understanding your justification for the changes here.) I guess I'm not seeing the eager / lazy part.

I don't want to hold up merging this, it doesn't feel like something worth arguing about, but I would like to understand.

Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't want to hold up merging this,

Thanks for saying this! But I think this is perhaps a self-inflicted wound which I should attempt to patch by reverting these changes, which don't really belong here.

...it doesn't feel like something worth arguing about, but I would like to understand.

I think that they ought to happen at some point (one reason I opened #2149 all those months ago... :-(), but here is not the place. So let's discuss separately, and hopefully be able to make progress downstream.

Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Unless I take your cue about cross-function uniformity (which I had also been going for... that's the second part of the changes, towards eliminating yes/no altogether) and only revert the proofs about derun...? But I still think I' should curb my tendency towards PR mission-creep ...

Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 17, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Er... now I'm not sure what to do. I've reverted the changes for derun, and looked again at the others, and then not reverted those (if only by reason of consistency/uniformity between branches). Not sure whether to go forward or back now!

I think that I lacked the courage of my convictions to try to defend the shift from (more) strict to less in these proofs, and indeed, in proofs the issue might be moot, but there's a running theme in the history of Decidable about the advantages of being able to work only with the ('cheaper') Boolean does, compared with having to recompute the whole ('expensive') proof... and AFAICT using the constructors yes and no forces recomputation of the proof field (because it asks the matcher to discern which of the constructors Reflects.ofⁿ Reflects.ofʸ is actually outermost around it, even though those are 'mere' proxies for the corresponding Bool...).

In all the example uses in this module, the 'positive' case is lazy (the proof field is thrown away/not bound by _), while the 'negative' case passes the proof to ... contradiction, which as observed elsewhere (eg #2243 / #2199 ), does not/cannot use its argument(s).

Now I can fully believe that I have misconstrued the role of strictness here (and indeed, perhaps a truly lazy evaluator could discern Reflects.ofⁿ / Reflects.ofʸ without having to do any other evaluation of the proof object underneath, but even that is doing too much traversal, eg via _×-dec_ etc.?), and perhaps any real distinctions can only be observed with very careful profiling, but having had my eyes opened by #1988 , I'm now ... sensitised to definitions being unnecessarily strict.

As things stand, neither in the status quo ante nor in these revised proofs, is there yet any attempt to replace these uses of with by a direct, but nevertheless dependent, elimination on b because p as a candidate proof of the Decidable property at hand, in which not only would strictness wrt the p argument be more clearly discernible, but also that such proofs could be directly by Bool elimination of b... that's properly the content of #2149 in introducing a 'true' dependent eliminator for Reflects/Decidable proofs...

... but if you're serious about replacing uses of with by direct dependent elimination (eg in terms of introducing explicit helper functions rather than having with introduce them behind-the-scenes) then eventually such issues will need to be tackled...

Sorry for such a long essay! I don't know how to distil a TL;DR for you!

Copy link
Collaborator

@JacquesCarette JacquesCarette Apr 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd say that the underlying issue was lack of understanding (of this reviewer) of the subtleties of the evaluation semantics (eager / lazy) involved, and the clear desire for things that are "pure" computations to never force the proof, since it's just going to be discarded anyways.

Part of my issue might be my shallow undertanding of all these syntax patterns and the overall effect they have.

I think the conversation has unearthed non-trivial design choices that ought to be better documented. I think your above essay has done a good job of pushing me towards 'your take' on what design is the better one.

In (unpublished, sigh) work of a long time ago, we used the words 'verdict' and 'rationale' for what is essentially 'does' and 'proof'. Maybe introducing some wrappers around Dec that are known to yield only verdicts (i.e. embody being lazy in the proof) would help? I'm only introducing these new words as a way to not fall into the rut of using old names with fuzzy semantics & thus muddying the actually interesting discussion.

Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 18, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like the 'verdict'/'rationale' separation of concerns!

As to being 'better documented', I think that Decidable and friends (esp. Reflects...) still represent a work-in-progress (with shout-outs to @laMudri for the work he did in pushing things forward in the direction of such separation), with #2149 and #2199 / #2243 being yet further glosses on that.

Eg. the factorisation of Decidable towards delegation to Reflects makes one kind of sense (provided that as far as possible, Reflects and its machinery is not/never exposed to the user!), but obscures, on the other hand, a 'direct' API of a form such as

record Decidable A : Set _ where
  constructor justified
  field
    verdict : Bool
    rationale : if verdict then A else ¬ A

(perhaps it was like this, once upon a time? cf. endless discussion about record wrapping for the sake of the typechecker, and an ambient aversion to 'computed types' such as if verdict then A else ¬ A for... green slime reasons, plus the inevitable need for with-based analysis downstream?)

As to laziness wrt the rationale field, I think that the existing machinery (at least) tries to draw out the design space, not least in the definitions of _×-dec_ etc. but I think you're right that we still don't quite have the 'right' API... and won't for a while yet!


derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
derun-accept {x} {y} xs ¬Rxy with R? x y
... | yes Rxy = contradiction Rxy ¬Rxy
... | no _ = refl
... | true because [Rxy] = contradiction (invert [Rxy]) ¬Rxy
... | false because _ = refl
Comment on lines +1029 to +1030
Copy link
Collaborator Author

@jamesmckinna jamesmckinna Apr 17, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ditto. presumably?


------------------------------------------------------------------------
-- partition
Expand All @@ -1040,7 +1040,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
... | true = cong (Product.map (x ∷_) id) ih
... | false = cong (Product.map id (x ∷_)) ih

length-partition : ∀ xs → (let (ys , zs) = partition P? xs) →
length-partition : ∀ xs → (let ys , zs = partition P? xs) →
length ys ≤ length xs × length zs ≤ length xs
length-partition [] = z≤n , z≤n
length-partition (x ∷ xs) with ih ← length-partition xs | does (P? x)
Expand Down