Promise Land: Proving Correctness with Strongly Typed Javascript-Style Promises
Issue Date
2022-01-01Author
Elliott, Andrei Darien
Publisher
University of Kansas
Format
35 pages
Type
Thesis
Degree Level
M.S.
Discipline
Electrical Engineering & Computer Science
Rights
Copyright held by the author.
Metadata
Show full item recordAbstract
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.
Collections
- Theses [3972]
Items in KU ScholarWorks are protected by copyright, with all rights reserved, unless otherwise indicated.
We want to hear from you! Please share your stories about how Open Access to this item benefits YOU.