Promise Land: Proving Correctness with Strongly Typed Javascript-Style Promises

Elliott, Andrei Darien

Publication

Promise Land: Proving Correctness with Strongly Typed Javascript-Style Promises

Elliott, Andrei Darien

Abstract

Code that can run asynchronously is important in a wide variety of situations, from user interfacesto communication over networks, to the use of concurrency for performance gains. One widely- used method of specifying asynchronous control flow is the Promise model as used in Javascript. Promises are powerful, but can be confusing and hard to debug. This problem is exacerbated by Javascript’s permissive type system, where erroneous code is likely to fail silently, with values being implicitly coerced into unexpected types at runtime. The work presented here implements Javascript-style Promises in Haskell, translating the model to a strongly typed framework where we can use the type system to rule out some classes of bugs. Common errors — such as failure to call one of the callbacks of an executor, which would, in Javascript, leave the Promise in an eternally-pending deadlock state — can be detected for free by the type system at compile time and corrected without even needing to run the code. Along the way, we demonstrate that Promises form a monad, providing a monad instance that allows code using Promises to be written using Haskell’s do notation.