a better scanr, via Data.List.NonEmpty

[jamesmckinna]

Avoids the with-based definition in favour of a simpler definition using (pattern-matching ;-)) let, with no dead-code branch... cf. also #1937 , #2123

[gallais]

Shouldn't the scanr in NonEmpty consume a NonEmpty list?
I think the improved scanr should probably go in Data.List.

[jamesmckinna]

@gallais wrote:

Shouldn't the scanr in NonEmpty consume a NonEmpty list?

I don't think so, although perhaps you could argue either way. I think the main point is that scanr transforms lists into non-empty lists. So maybe scanr⁺ should take a non-empty list, but then you would get (still) get a redundant repetition of f x y ∷ _ in both the top-level clause, and the local defn of the corresponding go function... I think? DRY!?

I think the improved scanr should probably go in Data.List.

That's more plausible, but then where does its defining property scanr-defn belong? Also there? I'd be fine with that, but it seems to go against ambient convention? I'll make that as a final change at the end, for comparison's sake. DONE.

All that said (and done): scanr⁺/go could now even also move to Data.List, as a local defn in scanr... and now does.

[jamesmckinna]

Thanks @JacquesCarette for the feedback. Any suggestions as to how to "find the way out of the bottle"?

UPDATED: hopefully the latest revisions are now more inline with your review comments!

[MatthewDaggitt]

This is screaming to me that we're doing something wrong here with the dependencies. Can we discuss this evening at the stdlib implementor's meeting?

[jamesmckinna]

Well, this is the motor for this PR: AFAICT, the Data.List.Base defn of scanr arises in the (historical) form it takes precisely to ensure that it can exist in Data.List.Base, without any of the other analysis of its typing.

But, as other commenters elsewhere note, the 'official' library definition has terrible properties (or better: terrible proofs of its properties...) because of its 'wrinkly' definition, arising from its combination of with and dead-code.

The other operations considered in #2267 / #2269 are OK, but scanr seems 'special'.

This PR represents my attempt at the least-invasive restructuring of Data.List.Base able to avoid the wrinkles...

[jamesmckinna]

So I think we've (now) agreed to find a better home for this (and #2269 ) under Data.List.Something, and not in Data.List. Suggestions welcome!

[jamesmckinna]

Aaargh: Data.List.Kleene.*!

[JacquesCarette]

So I think that the stuff in #2269 doesn't really need to move? At least, I don't immediately see the need. So that leaves just scanr?

Or do tails and inits belong so strongly with scanr that they really ought to move at the same time?

[jamesmckinna]

So I think that the stuff in #2269 doesn't really need to move? At least, I don't immediately see the need. So that leaves just scanr?

Or do tails and inits belong so strongly with scanr that they really ought to move at the same time?

Well, good question...

• scanr and tails belong together: Data.List.Properties.scanr-defn
• scanl and inits belong together, ditto.

So, I could imagine that #2269 is 'redundant'/'invalid', but for the fact that taken all together, the four functions belong with one another. It's a judgment call (and one which Data.List.Kleene regularises by being able to define them all together via the mutuality of the datatype definitions...), so not really sure what the right thing to do is.

[jamesmckinna]

An alternative, but for the cost of a horrible allocation overhead (because we can't write functions putting multiple return values on the stack!) against a benefit of being observably NonEmpty without going via List.NonEmpty, might be to use an auxiliary intermediate Product (which is what NonEmpty reifies as as type):

scanr : (A → B → B) → B → List A → List B
scanr {A = A} {B = B} f e xs = let h , t = go xs in h ∷ t
  where
  go : List A → B × List B
  go [] = e , []
  go (x ∷ xs) with y , ys ← go xs = f x y , y ∷ ys

[JacquesCarette]

That version of scanr would be a massive pain to prove anything about. Not only does it use a non-public helper function (whose properties are crucial), it also uses with (so another depth of helper function). This feels like a Haskell version of scanr, not an Agda version, if you get my drift.

[Taneb]

I'd really like to see this merged, but putting the implementation in Data.List really isn't great (as we've discussed before) - would a new module Data.List.Scans be an option? Along with the definitions discussed in #2269 and #2267

[jamesmckinna]

Thanks @Taneb ! Sorry my recent preoccupations have meant this PR got ignored/abandoned for a while. If there were general assent towards Data.List.Scans, perhaps that is (would be) the way to go. It feels weird to have to factor them out as 'special', though!? But the definitions indeed expose... anomalies...

[JacquesCarette]

I'm a huge believer in "follow the elegant path". Not always (there's lots of room for solid engineering and usability to disrupt some elegant paths), but whenever realistic. I sometimes say it as "follow the math", but by this I usually mean "the simple definitions, without unexplained / unexplainable detours". Those anomalies are a signal, and they're the kinds of signals that I love to pursue. scanr has hit that quite strongly!

[jamesmckinna]

If we agree to move this to Data.List.Scans, is there a way to merge the two sets of commits from here and #2269 into a single one? I realise I am out my depth here!

[jamesmckinna]

Now see #2395