Gradual Typing: TypeScript and Friends

Microsoft migrated 20 million lines of JavaScript to TypeScript - and found thousands of hidden bugs. Google converted 20% of its Python code to strict type hints. Airbnb reduced runtime errors by 38% after adopting TypeScript. But none of these companies halted development for the migration. How? Gradual typing - add types gradually, file by file.

• **Migrating large projects**: JS → TS without halting development (Microsoft, Google, Airbnb, Slack)
• **Python ecosystem**: FastAPI uses type hints for automatic API request validation
• **IDE superpowers**: autocomplete, go-to-definition, refactoring - all thanks to types
• **Documentation as code**: type annotations are documentation that is checked by the compiler and never goes stale

Gradual Typing - types on demand

Renovating an apartment has two approaches: move out, tear everything down to the concrete, and redo it all in six months - or renovate room by room while still living in it. **Gradual typing** is the room-by-room renovation for code.

**Gradual typing** is an approach where types are added to a program optionally. Code without types continues to work, and typed sections are checked by the compiler. There is no need to rewrite everything at once.

The key difference from ordinary static typing: the **`any`** type (or its equivalent) serves as the boundary between the typed and untyped worlds. Everything marked `any` is not checked by the compiler - it trusts the programmer.

**Migrating JS → TS**: rename `.js` to `.ts` - any JavaScript is already valid TypeScript. Add type annotations file by file, starting with the most critical modules (API boundaries, business logic).

TypeScript - the most successful gradual type system

TypeScript is not just "JavaScript with types". It is a full **structural** type system with union types, narrowing, mapped types, and conditional types. Let's examine the key mechanisms that make TypeScript an expressive tool.

**Structural typing** means TypeScript compares types by their **structure** (what fields they have), not by **name** (what the class is called). If an object has all the required fields, it qualifies - regardless of how it was created.

**`unknown` instead of `any`**: the `unknown` type is safer - it requires a check before use. Use `any` only as a temporary solution during migration, and `unknown` for external data (API responses, JSON, user input).

Python Type Hints - types without coercion

Python took the "types are optional" philosophy even further than TypeScript. In TypeScript the compiler at least checks types before generating JS. In Python, type annotations **have absolutely no effect on program execution** - they are just metadata. Checking is done by separate tools: mypy, pyright, pytype.

**The key difference from TypeScript**: in Python, type annotations are **only metadata**. The Python interpreter ignores them entirely. But frameworks like FastAPI/Pydantic read annotations via the `inspect` module and use them for runtime validation - this is a bridge between gradual typing and real safety.

**The `Any` propagation problem**: if even one function returns `Any`, it "infects" everything that interacts with it. mypy stops checking types in the call chain. Enable `--disallow-any-generics` and `--warn-return-any` for early detection.

Soundness: why TypeScript is intentionally "leaky"

The TypeScript team openly acknowledges that their type system is **unsound**. This is not a bug - it is a deliberate design decision. A sound type system guarantees that if code compiles, runtime type errors are impossible. TypeScript makes no such guarantee. But why did this turn out to be the right choice?

Why did unsound TypeScript win over sound Flow? The answer lies in the **adoption curve**. TypeScript allows gradual migration: any JS file can be renamed to .ts and it will compile. Flow required more changes, its tooling was slower, and its community grew more slowly. Pragmatism defeated academic purity.

**Rule for production code**: Never trust data crossing system boundaries - API responses, user input, files, environment variables. Validate at the boundaries with zod/io-ts/class-validator, and TypeScript's unsoundness ceases to be a problem.

Итоги

• **Gradual typing** - the philosophy of incremental type addition: code without types works, types are added as needed
• **TypeScript** - a structural type system with union types, narrowing, and expressive type inference; unsound by design
• **Python type hints** - annotations do not affect runtime; checked by external tools (mypy, pyright)
• **Soundness trade-off** - TypeScript is intentionally unsound for compatibility with JS and easy migration
• **Boundary protection** - validation of external data (zod, Pydantic) compensates for unsoundness in production

Gradual Typing in the context of language theory

Gradual typing bridges the static and dynamic worlds, creating a connection between them.

• Structural vs Nominal Typing — TypeScript uses structural typing - objects are compared by structure, not by name
• Type Inference — Hindley-Milner inference in Haskell vs local inference in TypeScript - different approaches to type inference
• Dependent Types — The next frontier: types that depend on values (Idris, Agda) - full program verification
• Runtime Validation — Zod, io-ts, Pydantic - a bridge between compile-time types and runtime safety

Вопросы для размышления

• Does the codebase use `any`? How much? Can it be replaced with concrete types or `unknown`?
• How is data from external APIs handled - trusted as-is or validated?
• Starting a new project from scratch: TypeScript strict from day one, or gradual typing?

Связанные уроки

• plt-03-static-vs-dynamic — Gradual typing bridges static and dynamic - you need to understand both ends first
• plt-04-type-inference — Type inference makes gradual typing practical by reducing the annotation burden
• plt-07-algebraic-types — Once gradual typing is mastered, richer type constructs like ADTs are the next step
• plt-02-type-systems — Foundation: what a type system is and which guarantees it provides
• comp-01-intro