Gradual Typing, Higher-Order Casts, and Blame

A language that mixes typed and untyped code must decide what happens at the boundary. Checking nothing gives up the guarantees the typed fragment was supposed to provide. Checking everything rejects programs that are correct in practice. Gradual typing takes a third route: it inserts a runtime check at each boundary, gives that check a direction and a label, and when the check fails it reports which side of the boundary was at fault. The mechanism is called a cast, and the discipline that makes the failure report meaningful is called blame.

The consistency relation

The type system adds a single type, written ? or ★, that is consistent with every type. The relation is not subtyping; it is symmetric, and it holds when the two types are equal or when either one of them is the dynamic type.

Consistency is deliberately not transitive: Int ~ ? and ? ~ String hold, but Int ~ String does not. This non-transitivity is the whole design. If consistency were a congruence closed under transitivity, the dynamic type would be a top and the system would collapse into a subtype system in which Int is a subtype of String through ?.

Typing rules use consistency in place of equality wherever a value crosses a boundary: an argument of type τ may be passed to a parameter of type σ when τ ~ σ. When the two are equal, the application is statically checked and no runtime work is inserted. When one is ?, the compiler inserts a cast.

Casts are checks with a direction

A cast from τ to σ is written ⟨τ ⇒ σ⟩ and behaves differently depending on which side is dynamic. For a first-order type the runtime work is one tag comparison against σ and one branch on the result.

From dynamic to static. The cast is a check. The value’s runtime tag is compared against σ; if it matches, the value passes through unchanged. If it does not, the cast fails and blame is assigned to the producer — the untyped code that supplied a value of the wrong shape. This is the straightforward case and it is what a conventional downcast does.

From static to dynamic. The cast is a no-op in the base case. A value of type τ is already a value, and the dynamic type accepts anything. Nothing needs to be checked because the typed code has already been verified against τ. But the value may later flow back out of the dynamic fragment at a different type, and the check that happens then must blame the right party. The mechanism that arranges this is the wrapper.

Why functions need to be wrapped

A first-order cast checks a tag once. A function cast cannot, because the function’s body will be called later with arguments supplied by the other side of the boundary. The check must therefore be deferred and distributed, and a cast on a function of n parameters installs one wrapper per parameter position plus one for the result.

Consider casting a function of type Int → Int to ? → ?. A naive implementation treats the cast as an identity and returns the function unchanged. The untyped caller then applies it to a string, the typed function’s body performs integer arithmetic on a string, and the failure occurs inside the typed code — which is then blamed, even though the fault is the caller’s.

The correct cast wraps the function:

def cast_function(fn, src, dst, blame):
    # src and dst are the function types on each side of the boundary.
    # `blame` labels the code that supplied the value being cast, here the function.
    def wrapped(arg):
        # The caller supplies a src-domain value and the function needs a dst-domain
        # value: the cast runs dst.dom <~ src.dom, so a failure implicates the caller.
        arg = cast(arg, src.dom, dst.dom, blame.negate())
        result = fn(arg)
        # The function produced a dst-range value where a src-range value is expected:
        # the cast runs dst.rng <~ src.rng, so a failure implicates the function.
        return cast(result, dst.rng, src.rng, blame)
    return wrapped

Each cast is written with the expected type on the left and the supplied type on the right, so cast(v, τ, σ, l) checks a value of static type σ against τ and blames l if the value does not belong to τ. The argument is cast against the domain the function expects, dst.dom, with the label negated because the obligation now falls on the caller rather than on the function. The result is cast against the range the caller expects, src.rng, with the original label, because the function is responsible for producing it. That is the contravariant half of the story: the arrow reverses its argument’s polarity, and the label reverses with it.

The same construction recurses. Casting (Int → Int) → Int to (? → ?) → ? must wrap the outer function, and the wrapper’s argument is itself a function that must be wrapped before being passed inward. A cast on a higher-order type therefore installs a tree of wrappers whose shape follows the type: one level per arrow, with a fresh wrapper for each function value that crosses the boundary. The wrapper tree is built when the cast is performed, so the construction is paid once per cast; the per-call cost is then the tag checks and indirect calls the wrappers perform for each argument that crosses them.

Blame, and the theorem behind it

Every cast carries a blame label naming the source location that introduced the boundary. When a cast fails, the error report names the label and the negation applied along the path. The path is a sequence of negations, so the label at failure is either the original or its dual, and the report can say which side violated its obligation.

The property that makes this meaningful is stated by the blame theorem, proved by Wadler and Findler and extended by Ahmed, Findler, Siek, and Wadler to the polymorphic case with type sealing: if a program with typed and untyped components fails with a blame error, the blamed component is the one whose type was violated, and the failure is not attributable to the boundary machinery itself. In the simply typed case the theorem says that a cast failure is always the fault of the side that made a claim its value did not satisfy.

Two corollaries follow, and both are checkable properties of an implementation.

Complete monitoring. Every value that crosses the boundary, in either direction, must pass through a cast that witnesses the crossing, and every part of a higher-order value must keep that witness for as long as it can be reached. An implementation that lets a value slip across without a wrapper — by caching a result, by reusing a closure, by optimizing away a cast the compiler believes is redundant — breaks the guarantee, because the eventual failure is then attributed to whichever side happens to be executing. This is why gradual systems are careful about where casts can be eliminated: eliminating a cast is only sound if the wrapper’s effect is provably unobservable, which for a function cast means the wrapper must not have been needed to catch a violation.

Blame preservation. The label attached to a cast must survive composition. When two casts compose, the label of the composite must be derived from the labels of the parts in a way that preserves which side is responsible. Systems that collapse adjacent casts as an optimization must compose the labels rather than discard them.

The dynamic type is not Any

A language with a top type and a bottom type can express Int <: Any, and a value of type Any can be used wherever any type is expected only through a downcast that the programmer writes explicitly. The gradual type ? differs in three ways, and the differences matter for soundness.

Any is a supertype, so the subtype relation is transitive through it. ? is consistent with everything but is not a supertype, so no transitive collapse occurs. This is why a gradual language can have both a dynamic type and a top type without the two being the same thing, and it is why the variance rules of structural subtyping and variance do not apply to ? in either direction.

Any permits any operation; a value of type Any can be applied, projected, or added, and the language’s dynamic semantics decides what happens. ? also permits any operation, and the difference is where the check lives rather than whether one happens: a value of type ? was itself produced by a cast that witnessed its crossing, so a program that applies it to an argument runs the wrapper installed by that cast, which checks the argument and blames the caller if it does not fit. The check is attached to the value, not to the use site.

A downcast from Any is unchecked in the sense that the programmer asserts the type; a cast from ? carries a label and produces a blame error rather than an assertion failure. The label is what makes the failure attributable.

Where gradual typing breaks down

The polymorphic case. Adding type parameters to a gradual language is harder than it looks. A value of type ∀α. α → α cast to ? and back must keep the parametricity the type promises: if the untyped side supplies a value of some type it invented, the function must not be able to treat that value as an Int and then hand back something that is not of the original type. The cast therefore has to rename the quantified variable at the boundary, accept any type name the untyped side supplies in its place, and refuse to accept the same name twice for two different types. The technique is type sealing: the cast allocates a fresh seal for the instantiation and wraps the value so that only that seal can unseal it, which is the mechanism Ahmed, Findler, Siek, and Wadler use to state the blame theorem for the polymorphic case. Implementations that omit the sealing accept programs that violate parametricity, and the blame theorem is not available for them.

The same quantification is what makes let-polymorphism and the value restriction necessary in a language with mutable state, and a gradual system that admits both must reconcile the two.

Effects at the boundary. A cast on a function that performs effects must decide whether the effects are checked too. If the typed fragment’s effect row is part of its type, the wrapper should check that the function performs no effect outside its declared row. Enforcing that at run time requires a representation of the row as a value to test against, which most gradual systems do not maintain. The practical consequence is that effect guarantees are weaker than value guarantees at a boundary — a documented limitation rather than a defect, but one that is easy to overlook when a signature’s row is read as a promise about behaviour.

Performance of wrapper trees. As noted, a higher-order cast installs wrappers that follow the type’s structure, and each call through them pays an indirection plus a tag check per wrapped argument. A boundary crossing inside a hot loop pays that cost per iteration. Implementations mitigate it where the type is first-order, since there the cast degenerates to a single check, and where the cast is loop-invariant, since then the wrapper construction and the wrappers themselves can be hoisted out of the loop. Neither mitigation applies when the type is genuinely higher-order and the function is called with fresh arguments each time.

Migration in both directions. A gradual language must support removing types as well as adding them. Removing a type from a signature turns a static check into one or more boundary casts, so a program that used to be rejected statically may now be accepted and fail at run time; the failure model genuinely changes, and the change is not local to the edited signature because every caller that still trusts the old type now crosses a boundary instead of being checked. The engineering discipline is to treat the removal as a change in the program’s failure model, not as a local edit, because the failure moves from the compiler to a call site that may be far away.