Gradual Typing

Gradual typing exists for a specific and entirely practical reason: there are enormous quantities of working, valuable, untyped code, and rewriting it is not on the table. A gradual system lets types be added incrementally, file by file or function by function, with the untyped remainder continuing to work. TypeScript over JavaScript, mypy and pyright over Python, Sorbet over Ruby, Typed Racket over Racket, Hack over PHP, and Flow are all instances of the same manoeuvre.

The mechanism is the dynamic type. Give the lattice a type that is consistent with everything, annotate what you can, and leave the rest at the dynamic type; the checker then verifies what it can see and waves through what it cannot. This is not a compromise bolted on afterwards — Siek and Taha's formulation of gradual typing is precisely the study of what such a system can and cannot guarantee, and the central result is that the guarantee is *local*.

The critical question, and the one that separates these systems into two genuinely different families, is what happens at the boundary. When an untyped value flows into a typed context, does anything check it? Typed Racket says yes and inserts a contract. TypeScript says no and emits nothing. Both are called gradual typing and they give you different products.

The usual mental model of any is "a type I have not narrowed yet", which makes it sound like unknown. It is not. unknown is a top type: everything is assignable *to* it, and nothing is assignable *from* it without a check, so it is safe and inconvenient. any is assignable in both directions. That bidirectionality is what breaks transitivity, and transitivity is what every other guarantee was resting on.

The practical consequence is that a single any does not affect one expression, it affects everything downstream of that expression. JSON.parse returns any, so every field of the parsed object is any, so every value derived from those fields is any, so every function they are passed to has its parameter checks silently satisfied. Nothing is reported at any step, because at every step the checker was told the value could be anything.

This is why the useful measurement in a TypeScript codebase is not the percentage of annotated code but the reachability of any from the boundaries. The noImplicitAny flag catches the ones the checker inferred; it does nothing about explicit ones, about as casts, or about the enormous surface of any in third-party type definitions. unknown at the boundary, with a parse step to a real type, is the fix, and it is the same conclusion as [[nullability]] reaches from the other direction.

The type assertion as is the other hole and is worth naming separately, because it is not a cast — nothing is converted and nothing is checked. It is an instruction to the checker to stop disagreeing. x as User on a value that is not a user compiles perfectly, emits nothing, and produces a User-typed reference to something else.

A gradual system that actually enforces its types must check values as they cross the boundary. For a first-order value that is cheap — check the shape once. For a function it is not, because you cannot check a function's type by inspecting it; you have to wrap it in a proxy that checks each argument and each result on every call, for as long as the function lives. The same applies to objects with methods, to arrays whose element type must be maintained, and to anything higher-order. These wrappers are contracts, and they are not free.

The result is that a sound gradual system can be very fast when a program is fully typed, very fast when it is fully untyped, and dramatically slower in the middle — precisely the configuration that gradual typing exists to support. Takikawa and colleagues measured this systematically across the possible typed/untyped configurations of Typed Racket programs and found overheads reaching two orders of magnitude in some configurations, publishing the result under the title "Is Sound Gradual Typing Dead?". The answer given by the community since has been a decade of work on reducing it — transient checks, space-efficient contracts, type-directed erasure — rather than a claim that the measurement was wrong.

This is the context in which TypeScript's decision reads as engineering rather than carelessness. Enforcing types at runtime in JavaScript would mean wrapping every boundary crossing in a proxy, in a language where boundary crossings are everywhere and proxies are slow, for a guarantee that competes with the ecosystem's existing validation libraries. The team chose erasure: zero runtime cost, zero output difference, and an explicit statement that the types are a development-time tool. Every consequence in this lesson follows from that one decision, and it is defensible — as long as everyone knows it was made.

The honest summary is that you can have soundness or you can have zero runtime cost at partially-typed boundaries, and nobody has yet shown how to have both at scale. Which one you want depends on whether your boundary is inside your program (where erasure plus discipline is usually fine) or at its edge (where you need a real check, and the language is not going to provide it).

The design conclusion is not "TypeScript is unsafe". It is that the checker covers one region and the boundary of that region is where your own checks have to live. Inside the region, the types carry real information and catch real mistakes at a cost of nothing at runtime, which is an excellent trade. At the boundary — HTTP responses, JSON, localStorage, environment variables, database drivers, model output, anything from a third-party library typed by hand — the guarantee is exactly zero, and only a runtime validator restores it.

That is why the validator libraries exist and why they are shaped as they are. A schema that both validates at runtime and produces the static type, so the two cannot drift apart, is the missing half of the language's design, supplied by userland. The pattern is the same in Python (pydantic), Ruby (Sorbet's runtime checks) and TypeScript, and it is the concrete form of the parse-don't-validate argument.

The second conclusion is about any hygiene. Because any is transitive through everything it touches, its cost is proportional to how far it can reach rather than to how often it appears. One any at a widely used boundary function disables checking across a large fraction of a codebase; a hundred anys in leaf functions do far less damage. Auditing by reachability rather than by count is the difference between a useful cleanup and a busy one.

And the third is about agent and model output specifically, since it is now a common boundary: text generated by a language model is untrusted input in exactly the sense this lesson means. A declared return type on the function that parses it is a claim about the code, not about the string — see [[structured-output-parsing]] and [[typed-tool-calls]] for what has to happen at that boundary.