Typed-Untyped Interactions: A Comparative Analysis

Posted on 06 February 2023.

Dozens of languages today support gradual typing in some form or another. What lessons can the designer of a new language learn from their experiences?

As a starting point, let’s say that we want to maximize interoperability. For most types in the language, untyped code should be able to make a value that works for that type: type Number should accept untyped numbers, type List(Number) should accept untyped lists, and so on.

(This may seem like an obvious requirement for a type system that gets added on top of an untyped language. But there are good reasons to break it — see our earlier post on Static Python.)

The question now becomes: what sort of validation strategy should typed code use when an untyped value tries to cross a type boundary? For example, when a Number -> Number type receives an untyped function there are at least three viable options:

  1. Wrap the function in a proxy to make sure its behavior matches the type.
  2. Leave the function unwrapped, but put checks at its call sites.
  3. Do nothing! Trust the function.

Both the research literature and the realm of production-ready languages are full of ideas on this front. What was unclear (until now!) is how the validation strategies implicit across the landscape relate to one another.

With this paper, we introduce a toolbox of formal properties to pin down the guarantees that gradual types can provide:

  • type soundness (generalized) for local type guarantees,
  • complete monitoring for compositional type guarantees,
  • blame soundness to judge the accuracy of validation errors, and
  • blame completeness to judge the precision of validation errors.

We also use an error preorder to rank strategies by how early they can detect a type validation mismatch.

The upshot of all this is a positive characterization of the landscape. There is no clear winner because there are other factors at play, such as performance costs and the usefulness of types for debugging. What we do gain is a solid theoretical foundation to inform language designs.

It’s all in the paper.