lwt.ml: human-friendly edition – major refactoring and commenting of the Lwt core

[aantron]

This PR heavily updates lwt.ml to make it much more legible and friendly.

What the new lwt.ml looks like...

• in the ordinary view, where you can see it in all its glory, read the friendly Reading Guide and Overview, and browse all the code,
• with internal modules folded (94 lines), where you can neatly see the high-level structure of the Lwt core, and
• with internal signatures expanded (282 lines), where you can see what belongs where.

For comparison, what the previous lwt.ml looks like: [link].

Why?

This PR is a series of gradual refactorings of lwt.ml to make it more legible, such that the final version shares almost no lines in common with the original, though the ASTs are still largely similar. There are two main purposes:

• Make it much easier to contribute to Lwt. I've seen several comments along the lines of "I wanted to contribute, but I couldn't read lwt.ml," and I couldn't read it well either. Even if someone can't read the new lwt.ml, they should feel welcomed and encouraged to ask about it.

• Have enough people actually understand the semantics of lwt.ml deeply to be able to do some combination of

  • write the manual (Write new manual #304),
  • adapt to effects,
  • adapt better to JS, and/or
  • change the semantics in various ways (e.g. Bind quirk #329).

  Ideally, enough people can read lwt.ml for the semantics to enter the community's organizational memory. This will hopefully free Lwt from some paralysis and inertia.

  I found that, while reading lwt.ml, I needed to refactor it in some places, to be able to continue reading it more and more deeply, instead of getting stuck on superficial difficulties. That eventually led to this whole PR.

Highlights of the new code

The new lwt.ml has:

• Thorough documentation, including the mentioned Reading Guide and Overview, as well as many implementation detail comments. The Overview discusses all concepts necessary to understand everything in lwt.ml.
• Sectioning with internal modules. Signatures limit the scope of helpers, and provide type-checked tables of contents. Internal modules can be folded by text editors that support code folding. Functions are reordered by category, compared to the original lwt.ml.
• Lots of renaming for clearer, self-descriptive terminology, and a switch to the "promise" language.
• General refactoring and cleanup to organize the code.
• GADTs to eliminate a large number of assert false cases. The original code had 35 assert false expressions, which correspond to a considerably larger number of cases, because many appear under or-patterns. The new code has four assert false expressions.
• Explicit annotation and documentation of promise state changes. Encoding (mutable) promise state in a GADT requires casts when state changes, and these casts explicitly document the state changes Lwt believes are possible between when Lwt gives a promise to a user, and when Lwt uses that promises again later.
• No first-class modules. These were used for encoding existential types, and have been replaced by GADTs.

It's undoubtedly possible to improve the code even further, but I'd like to commit this as a starting point for that process.

How to review

This PR is broken up into 57 commits, of which:

• The first 40 are trivial renamings, reorderings, and whitespace changes.
• The next 11, from "be explicit about public/internal casts" to "refactor nchoose, npick, nchoose_split" are non-trivial changes that require true thinking. Of these, "make promise state into a GADT" is the most involved. Many of these have detailed commit messages.
• The remaining 6 are again trivial renamings, reorderings, and whitespace changes.

It's still a lot to deal with, but hopefully this way of breaking up the history makes it somewhat possible to review the PR. It should also give lwt.ml fairly sane blame.

Each commit passes the Lwt test suite. Code coverage is 98%, though the test suite is more thorough than just achieving high coverage.

Pings and notes

I have to thank @dkim for some suggestions on improving the Overview. Thanks!

@talex5 Obviously, this affects tracing. Ultimately, I hope it makes tracing easier to maintain. We should probably also work on getting it maintained in the main Lwt repo at some point (#180).

This code should be bug-for-bug compatible with the previous code. That includes the assertion failures and segfaults we recently saw in #315 and #349. In fact, this code is likely to have worse behavior in such situations, due to having fewer assertion expressions. Preserved bugs also include #340.

Some of the stuff in the overview belongs in lwt.mli, and may get moved there when working on the manual.

I would appreciate it if anyone with access to a stress test, or any other non-trivial Lwt code, would give this rewrite a try (@mfp, @copy, @domsj?). The command to pin it should be:

opam pin add lwt https://github.com/ocsigen/lwt.git\#wat

Thanks!

[aantron]

Ok, the entire stability project turned out to be (probably) caused by the Skylake CPU bug. So, nothing is blocking work to finish off this PR. I've tried to address all the comments.

• Switched "unification" vocabulary to "proxying".
• Gave constructors to the phantom types, so they can be moved into an internal module.
• Fixed typos.
• Regarding the warning suppression (ping @avsm), I think we have to keep it. Since there is no _tags anymore, I will probably add it as an [@@@ocaml.warning] extension point inside lwt.ml in the upcoming merge commit.
• Regarding the promise state terminology, I am now thinking that the right thing to do is to fully adopt JS terminology, i.e. completing becomes resolving, resolving becomes fulfilling, etc. I'll open a separate issue about that, and that issue will also include an item to write a table containing the mapping between old terminology, new terminology, and terminology in other popular languages or systems. For this PR, I've gone through the comments and tried to make sure the current transient terminology is self-consistent. A quirk (already observed by @edwintorok) is that what resolvers do is allow completing promises. After switching to JS terminology, resolvers will resolve promises. The JS terminology issue doesn't have to result in JS terminology; debate is welcome, but whatever the final terminology is, we will make everything as consistent and obvious as possible.
• Regarding anything that is already explained in the .mli file, the .mli file will be rewritten as part of creating the new manual. I agree that several things from the comments in the new lwt.ml should, or are, explained there. However, the .mli file is currently a source of uncertainty, and I'd like to revisit lwt.ml once lwt.mli is written. I will adjust the comments then to reduce duplication, and everyone is welcome to participate in revisiting lwt.ml as well :)

This PR passes all the unit tests, and I believe it has also passed several stress tests by @smondet, @domsj, and @copy. I think we should merge it relatively soon. That will eliminate the chance of further bit rot, and dually eliminate uncertainty about working on lwt.ml/unblock several issues in it.

When merging the PR, I will incorporate the work on more accurate exception messages by @raphael-proust that has been added to master while the PR was open.

For whatever is left over, and upon new ideas, everyone is welcome to make further issues and PRs to improve lwt.ml. As it says inside:

* Please edit the code and the docs!

This code is meant to be readable, and to be edited. If you are reading
something, and think there is a much better way to express it, please go
ahead and open a pull request to the Lwt repository at

 https://github.com/ocsigen/lwt

I'll probably remove the word "much" from that. It sounds like a barrier.

So... :)

[aantron]

(macOS build failures were caused by some upstream breakage on macOS, that was fixed in master by 0e63890 on May 16, so it should be fine on merge, and I will check that before putting the merge into master).

[avsm]

nit: Overview -> overview

[aantron]

I actually wrote that deliberately, but looking back on it months later, I have to agree :) Changing...

[chambart]

You should mark those types as private to enforce it.

[aantron]

Very nice, I've done so.

This is actually enforcing even what prevented me from making the promise record type private – that the record would become immutable even inside the module Main_internal_types. private in a module is perfect for phantom types, though.

[chambart]

It is possible to avoid one indirection (and associated allocations) here.

type (_,_, _, _) kind =
    | Resolved : ('a,'a, underlying, completed) state
    | Failed   : (exn, _, underlying, completed) state
    | Pending  : ('a callbacks, 'a, underlying, pending) state
    | Proxy    : (('a, 'b, 'c) promise, 'a, proxy, 'c) state

type (_,_,_) promise = Promise : {
  mutable kind : ('value, 'a, 'u, 'c) kind;
  mutable value : 'value;
} -> ('a, 'u, 'c) promise

Of course the problem is that mutating the value requires both fields to be updated at once. You can't express that in the type system, hence you need to cheat some more with the type system to write a set function like:

val set : ('a, 'u, 'c) promise -> ('value, 'a, 'u, 'c) kind -> 'value -> unit

I'm not proud of this kind of suggestion, but in the case of Lwt the cost of traversing those pointers and allocating the state is far from negligible.

[Drup]

The problem of that proposition is that, additionally to the set trick, it requires inline records. Lwt is still compatible with ocaml 4.02, inline records come from 4.03.

[aantron]

This also reminds me of #94 (comment). We will have to keep it mind for the future.

[aantron]

It's finally in! Thanks to all reviewers (whether commenting or not!) and stress testers!

[aantron]

Hopefully, it's now open season on improving lwt.ml :)