feat: upstream ListM from mathlib4

[kim-em]

This migrates ListM upstream from Mathlib, renaming it to MLList (for "monadic lazy list", returning to the mathlib3 name), and making some adjustments so more operations are lazy.

[fgdorais]

Can be merged as-is (mathlib down-port).

Just a nitpick: shouldn't it be listMAPI instead of listMApi? This is not important and so I'm accepting this "incorrect" spelling.

[digama0]

the naming convention from core is ListM.Spec

[fgdorais]

the naming convention from core is ListM.Spec

Sounds a lot better to me! @semorrison ?

[digama0]

@semorrison I made a bunch of modifications here. Most notably, some of the function arguments have gained a Unit -> because we want to run them lazily (e.g. in append), and also the new Thunk type is added as a constructor so that you can have haskell style "evaluated and the result is remembered so you don't have to evaluate it again next time". It is used to prevent deep recursion or infinite recursion in pure functions here, rather than building up a long cons chain immediately.

[fgdorais]

Since @digama0 has baked-in laziness, maybe we should consider renaming this LazyListT and specialize to the new type LazyList when m:=Id?

One reason is that the specialization to m:=Id is actually interesting and it deserves a cool name! LazyListM would also work but I think that we're moving away from that after the OptionM/Option debacle.

Another reason is that I would expect ListM to reduce to something essentially equivalent to List when m:=Id. But now we have something substantially different from List when m:=Id.

In my mind, ListT m α should implement what may be informally described by m (α × m (α × ...)) (in the same sense that List α can be informally described by α × (α × (α × ...))). The monad m could be used to implement some laziness but that is not necessarily the goal since List is strict. Therefore, I think we are now looking at a fundamentally new type.

PS: Why this was called ListM instead of ListT. Is that a historical accident?

[digama0]

PS: Why this was called ListM instead of ListT. Is that a historical accident?

MList might be a better name, it means essentially "monadic (lazy) list". In lean 3 it was called mllist. ListM looks a bit more similar to others but it's probably a false cognate since it's not a monad (or rather, it is but that's not the focus of the type).

The reason for baking in the laziness is because you can end up with a completely different order of operations when using do notation than what you would expect, when the monad is something "strict" like Id, Option or Except. This is basically the same reason that andThen, orElse etc have a Unit -> thunk around their second argument, there were actual bug reports about this where things would get lifted out of the bottom half of a do block and executed unconditionally, leading to extremely difficult to interpret behavior after optimizations.

[fgdorais]

I see. The M is because this is a "list type that works well within monadic code" not that it is a monad transformer. In that case, putting the M at the end is confusing. I think it's good to have Lazy in there since that's a key feature. MLazyList sounds nice?

[kim-em]

Sorry, I haven't looked at this in a while. I am slightly in favour of MList over MLazyList, as I think the lazyness is subordinate to the monadicness.

However the much bigger chore that remains is to building mathlib against Mario's changes and see if everything still works. I will try to make this a priority.

[kim-em]

Downstream I used consOption (called just cons in the Mathlib version, with cons' being the cons in this PR) all the time. So having it disappear is a bit of a surprise.

EDIT: looking at the code, I actually never need it! Nice. :-)

[kim-em]

Remaining tasks here:

• wait for [Merged by Bors] - chore: bump Std (adapt to migration of ListM) mathlib4#6413 to build to ensure everything works
• finish bikeshedding. :-) I like MList the most, so will implement that change now, but am happy to take further instruction on this!

[digama0]

I'm basically happy with the current state of things. @semorrison, what do you think about the name MLList, returning to the old lean 3 name?