Modeling asynchronous transactions with types — Part 1

Scenario 1

Imagine that you're in writing a function that caches assets on S3. The function should:

1. Write an asset to a given key/bucket.
2. Store the asset's location in a Postgres table.

Now, imagine that you accidentally write:

await writeLocationToPgres(assetId, bucket, key);
await uploadToS3(bucket, key);

When things go well, there is no problem, but if something goes wrong during the write to S3, your asset cache will be out-of-sync with S3. That means that no logic will kick in to retry the upload, which means that downstream services like webpages and video renderers will not display the asset.

This sort of bug happens all the time and is the reason that videos have chunks lobbed off and profile pictures disappear even though "I'm sure I uploaded it."

Scenario 2

You work for a price comparison tool and you're contractually obliged to present quotes from 3 vendors. You write:

quote1 = await getQuote1();
quote2 = await getQuote2();
async sendWinningQuote([quote1, quote2]);

This will work for a while until Vendor #3 realizes they are getting no business from your site, at which point there are lawsuits, angry consumers, and a degradation of trust in a service. This sort of thing also happens all the time.

Asynchronous transactions are hard!

In both cases, a company got bit by an asynchronous transaction. In one, the developer wrote something in the wrong order, and in the other, s/he left something out.

At Meeshkan, like in most companies, our team spends time investigating at which point of a pipeline asynchronous transactions failed. It is really hard, and there is no silver bullet to ensure the correct execution, relaunching, and potential rollback of complex asynchronous transactions.

What I'd like to show in this series of articles is one strategy to reduce the number of botched asynchronous transactions. To start, I'll revisit the two examples above, showing how both errors are prevented in my IDE (VSCode) by a type-checker (in this case, PureScript).

Scenario 1 revisited

Check out the following program in PureScript where I write to the db after I write to s3. It compiles just fine.

If, however, I invert the order, we get a red-squiggly.

Plus an error message that tells us exactly what went wrong.

Scenario 2 revisited

Check out the following program in PureScript where I get quotes from three vendors and only display information after I receive all 3 quotes.

If I change the order of the quotes, it still compiles just fine, as all three are present.

However, if I leave one out, the compiler lets me know with a red squiggle.

It also lets me know exactly what I left out.

What's to come

In the next article in this series (that will come out tomorrow), I will show how to build this sort of system from the ground up.

The first article will look at how rows can create "lanes" in indexed monads to allow for indeterminate order of execution where order doesn't matter (ie from our vendor-quote example above) while enforcing certain before-after relationships where order does matter.

The second article will show how these relationships can be consolidated into a type-level transition machine so that they are not defined ad hoc.

The third article will show how these relationships can be built into an ADT that is used to construct an indexed free monad, guaranteeing that they are the only possible outcomes in a given monadic context.

Comments

[Asad Saeeduddin]

Nice post! In the following snippet:

quote1 = async getQuote1();
quote2 = async getQuote2();
async sendWinningQuote([quote1, quote2]);

Did you perhaps mean:

await getQuote1()
// etc.

?

[Mike Solomon]

yup, thanks!