Gradually typed programming languages permit the incremental addition of static types to untyped programs. To remain sound, languages insert run-time checks between the boundaries of typed and untyped code. Unfortunately, performance studies have shown that the overhead of these checks can be disastrously high, calling into question the pragmatics of sound gradual typing. In this paper, we show that by building on existing work on soft contract verification, we can reduce or eliminate this overhead.

Our key insight is that while untyped code cannot be trusted by a gradual type system, there is no need to consider only the worst case when optimizing a gradually typed program. Instead, we statically analyze the untyped portions of a gradually typed program to prove that almost all of the dynamic checks implied by gradual type boundaries cannot fail, and can be eliminated at compile time. Our analysis is modular, and can be applied to any portion of the program.

We evaluate this approach on a dozen existing gradually typed programs previously shown to have prohibitive performance overhead—most cases more than 2× overhead and up to 70× in the worst case—and reduce the overhead to 0 in most cases and 1.6× in the worst case.