Gradual Typing

Every programmer faces the same tension: static typing catches bugs before the program even runs, but annotating every variable slows you down; dynamic typing lets you move fast, but errors only surface at runtime — sometimes days after they were introduced.

Gradual typing, introduced by Jeremy Siek and Walid Taha in 2006, dissolves that tension. In a gradually typed language you can annotate some variables and leave others with the dynamic type $\star$ (sometimes written ? or Any). The type checker ignores $\star$ in static analysis; at runtime, every crossing of a typed/untyped boundary becomes an explicit cast that checks the contract on the spot.

The key insight is the blame theorem: when a cast fails, the language runtime can always point its finger at exactly the piece of code that broke the contract — the typed side, the untyped side, or neither. You get the safety of static typing where you want it and the flexibility of dynamic typing where you need it, with no silent errors in between.

Languages like TypeScript, Python (with mypy/pyright), Racket, and Dart all embody different points on this spectrum. Gradual typing is the formal foundation underneath them all.

The demo below simulates a cast boundary between a statically typed function and a dynamically typed caller. The typed function expects an integer; choose what value to pass and watch what happens.

<!-- {{c_html_intro}} -->
<div class="scene">
  <div class="zone typed-zone">
    <div class="zone-label">{{label_typed}}</div>
    <div class="zone-desc">{{desc_typed}}</div>
    <div class="annotation">double(x: <span class="ann">Int</span>) → <span class="ann">Int</span></div>
  </div>
  <div class="boundary" title="{{boundary_title}}">
    <div class="boundary-arrow">→</div>
    <div class="boundary-label">{{label_boundary}}</div>
  </div>
  <div class="zone untyped-zone">
    <div class="zone-label">{{label_untyped}}</div>
    <div class="zone-desc">{{desc_untyped}}</div>
    <div class="value-picker">
      <span>{{label_send}}:</span>
      <button class="val-btn" data-val="42" data-type="int">42 (Int)</button>
      <button class="val-btn" data-val="hello" data-type="str">"hello" (Str)</button>
      <button class="val-btn" data-val="3.14" data-type="float">3.14 (Float)</button>
      <button class="val-btn" data-val="null" data-type="null">null</button>
    </div>
  </div>
</div>

<div class="cast-box" id="castBox">
  <div class="cast-title">{{cast_title}}</div>
  <div class="cast-row"><span class="cast-key">{{label_value_sent}}</span><span id="sentVal" class="cast-val">—</span></div>
  <div class="cast-row"><span class="cast-key">{{label_expected}}</span><span class="cast-val"><span class="ann">Int</span></span></div>
  <div class="cast-row"><span class="cast-key">{{label_result}}</span><span id="castResult" class="cast-val">—</span></div>
</div>

<div class="blame-box" id="blameBox" style="display:none">
  <div id="blameIcon" class="blame-icon"></div>
  <div id="blameText" class="blame-text"></div>
</div>

<div class="output-box" id="outputBox" style="display:none">
  <div class="output-label">{{label_output}}</div>
  <div id="outputVal" class="output-val"></div>
</div>

<button id="resetBtn" class="reset-btn">{{btn_reset}}</button>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 14px; }

.scene { display: flex; align-items: stretch; gap: 0; margin-bottom: 1rem; border-radius: 10px; overflow: hidden; border: 1px solid #cdd9e3; }
.zone { flex: 1; padding: .8rem; }
.typed-zone { background: #e8f5e9; }
.untyped-zone { background: #fff8e1; }
.zone-label { font-weight: 700; font-size: .85rem; margin-bottom: .25rem; }
.typed-zone .zone-label { color: #1b5e20; }
.untyped-zone .zone-label { color: #e65100; }
.zone-desc { font-size: .8rem; color: #555; margin-bottom: .5rem; }
.annotation { font-family: ui-monospace, monospace; font-size: .85rem; background: #c8e6c9; padding: .2rem .4rem; border-radius: 4px; display: inline-block; }
.ann { color: #1565c0; font-weight: 700; }

.boundary { display: flex; flex-direction: column; align-items: center; justify-content: center;
            width: 64px; flex-shrink: 0; background: #f5f5f5; border-left: 2px dashed #aaa; border-right: 2px dashed #aaa; padding: .4rem 0; }
.boundary-arrow { font-size: 1.4rem; color: #666; }
.boundary-label { font-size: .65rem; color: #888; text-align: center; margin-top: .2rem; text-transform: uppercase; letter-spacing: .04em; }

.value-picker { display: flex; flex-direction: column; gap: .35rem; margin-top: .3rem; }
.value-picker > span { font-size: .8rem; color: #555; }
.val-btn { font: 600 12px ui-monospace, monospace; padding: .3rem .6rem; border-radius: 6px; border: 1px solid #e65100; background: #fff3e0; color: #bf360c; cursor: pointer; text-align: left; transition: background .1s; }
.val-btn:hover { background: #ffe0b2; }

.cast-box { background: #f0f4f8; border: 1px solid #cdd9e3; border-radius: 8px; padding: .7rem; margin-bottom: .6rem; }
.cast-title { font-weight: 700; font-size: .8rem; color: #1d3557; margin-bottom: .4rem; text-transform: uppercase; letter-spacing: .04em; }
.cast-row { display: flex; gap: .5rem; font-size: .85rem; margin-bottom: .15rem; }
.cast-key { color: #555; min-width: 120px; }
.cast-val { font-family: ui-monospace, monospace; font-weight: 600; }

.blame-box { border-radius: 8px; padding: .7rem; margin-bottom: .6rem; display: flex; align-items: flex-start; gap: .5rem; }
.blame-box.blame-ok { background: #e8f5e9; border: 1px solid #a5d6a7; }
.blame-box.blame-dynamic { background: #fff3e0; border: 1px solid #ffcc80; }
.blame-box.blame-static { background: #fce4ec; border: 1px solid #f48fb1; }
.blame-icon { font-size: 1.4rem; flex-shrink: 0; }
.blame-text { font-size: .88rem; line-height: 1.5; }

.output-box { background: #e3f2fd; border: 1px solid #90caf9; border-radius: 8px; padding: .7rem; margin-bottom: .6rem; }
.output-label { font-weight: 700; font-size: .8rem; color: #0d47a1; margin-bottom: .25rem; text-transform: uppercase; letter-spacing: .04em; }
.output-val { font-family: ui-monospace, monospace; font-size: 1rem; font-weight: 700; color: #1565c0; }

.reset-btn { font: 600 13px system-ui, sans-serif; padding: .4rem .9rem; border: 1px solid #1d3557; background: #fff; color: #1d3557; border-radius: 8px; cursor: pointer; }
.reset-btn:hover { background: #e8eef3; }

// Code not found

Notice the pattern. When the static side receives a value that matches its annotation, the cast succeeds silently. When it receives a wrong type, the runtime raises a blame error pinned to the dynamic (untyped) side — it broke the contract. If the typed side itself had an incorrect annotation, blame would fall on it instead. That precision is the whole point: no more mysterious TypeError with no culprit.

Mixing typed and untyped code sounds simple but hides real depth.

• First-order casts are easy. Checking 42 : Int at a boundary is one comparison. Checking a string, a boolean — still trivial.
• Higher-order casts are hard. If a dynamically typed caller passes a function $f : \star$ to a context expecting $\text{Int} \to \text{Int}$, you cannot check the function type immediately — functions are checked lazily, by wrapping $f$ in a proxy that checks each argument and each result as they flow. This wrapping can nest arbitrarily, and naive implementations pay $O(n^2)$ overhead for $n$ calls through $n$ boundaries.
• The blame theorem (Wadler & Findler, 2009) states that if a cast fails, the label on the blame is always a positive position (a value flowing into a context) or a negative position (a context demanding more than it declared). Typed regions can never be blamed for errors that originated in untyped code, and vice versa.
• Soundness vs. performance. A fully sound gradually typed system (like Typed Racket) carries runtime overhead proportional to how much untyped code crosses typed boundaries. "Transient" gradual typing (used in Reticulated Python and partly in TypeScript) drops higher-order wrapping, gaining speed at the cost of weaker blame — it tells you a cast failed, but not always whose fault it was.
• The gradual guarantee (Siek et al., 2015) says adding or removing a type annotation should never change whether a program runs — only whether a type error is caught earlier or later. Achieving this precisely is still an active research problem.

Related ideas appear in program synthesis and PAC learning: in all three, you are drawing a boundary between "what the machine can verify automatically" and "what it must take on faith," and managing the interface carefully.

Gradual typing is not a theoretical curiosity — it is the engineering strategy behind some of the most widely used languages today:

• TypeScript: Microsoft's typed superset of JavaScript treats every untyped JS value as type any ($\star$). Type annotations are optional and checked statically where present; runtime checks are left to the programmer, making TypeScript "optionally typed" rather than fully gradually typed — a pragmatic trade-off.
• Python type hints (PEP 484, mypy, pyright): Python lets you annotate functions and variables; tools like mypy check them statically without changing runtime behavior. The Any type plays the role of $\star$.
• Typed Racket: the most faithful academic implementation of gradual typing, with full higher-order contracts and the blame theorem enforced at runtime. It demonstrated that soundness is achievable but costly.
• Dart: uses a sound null-safety system built on gradual principles, with a sharp boundary between nullable and non-nullable types.
• Gradual migration: in large codebases (Node.js apps, legacy Python services) gradual typing lets teams annotate module by module, running the type checker only on the annotated parts. No big-bang rewrite required.

The pattern — add a formal boundary, track blame across it, migrate incrementally — shows up far beyond programming languages: in API versioning, in contract-based software components, and anywhere two systems with different levels of formality must interoperate.

Gradual typing answers a question that haunted programming language designers for decades: can a language be both statically and dynamically typed without lying about it?

The answer is yes — but only if runtime casts enforce the boundary honestly and the blame theorem ensures that every failure has a clear culprit. The cost is real: higher-order casts add overhead, and achieving full soundness requires discipline from the runtime. The reward is equally real: teams can migrate large codebases incrementally, get type-checker feedback on the parts they care about most, and still let exploratory code run without annotations.

Next time you write any in TypeScript or reach for # type: ignore in Python, you are standing at a cast boundary. The theory of gradual typing has a precise name for what happens there — and a theorem that tells you exactly who to blame when it goes wrong.