kirancodes.me
To Proof Maintenance & Beyond!

Parallel type-checking with haskell using saturating LVars and stream generators

Ryan R. Newton, Ömer S. Agacan, Peter P. Fogg, Sam Tobin-Hochstadt

Abstract

Given the sophistication of recent type systems, unification-based type-checking and inference can be a time-consuming phase of compilation---especially when union types are combined with subtyping. It is natural to consider improving performance through parallelism, but these algorithms are challenging to parallelize due to complicated control structure and difficulties representing data in a way that is both efficient and supports concurrency. We provide techniques that address these problems based on the LVish approach to deterministic-by-default parallel programming. We extend LVish with Saturating LVars, the first LVars implemented to release memory during the object's lifetime. Our design allows us to achieve a parallel speedup on worst-case (exponential) inputs of Hindley-Milner inference, and on the Typed Racket type-checking algorithm, which yields up an 8.46× parallel speedup on 14 cores for type-checking examples drawn from the Racket repository.

Related papers