Type Safety

Type Safety

Concept of the skill

Two-layer model: a compile-time layer where the type checker verifies internal consistency (claims about values are coherent across the codebase) and a runtime layer where values from outside the program (HTTP responses, environment variables, parsed JSON, untrusted user input) have NO type until parsed, regardless of what type annotation sits next to them. The discipline is the boundary contract between these two layers: validate at I/O boundaries (parse, never assert), then trust the type inside. Layered on top: soundness (does the system rule out ALL type errors of the kinds it tracks, or only some via escape hatches?), structural vs nominal typing (do shapes match by structure or by name?), narrowing (refine a broad type by control-flow evidence), and exhaustiveness checking (force the compiler to flag uncovered cases in a discriminated union).

Distinguishes a syntactic claim from a semantic guarantee. Without type-safety as a discipline (not just a compiler flag), JSON.parse(x) as User looks identical to a validated parse — the cast is decoration, not verification. The alternative — "the compiler said it was fine, so it's fine" — fails because gradual systems like TypeScript are unsound by design (escape hatches: any, as, function bivariance, ambient declarations) and untrusted input arrives un-typed regardless of what annotation sits next to it. Type-safety replaces the "compiler-blessed" mental model with "compile-time guarantees stop at the I/O boundary, runtime validation takes over there."

Distinct from api-design, which owns the external request/response surface shape — type-safety owns the discipline of expressing internal program correctness as types, and where the type system stops at the boundary api-design defines. Distinct from testing-strategy, which owns runtime verification of behavior — type-safety owns compile-time verification of structure, and the two cover different failure modes (a function can be type-safe and behaviorally wrong, or behaviorally correct and type-unsafe). Distinct from entity-relationship-modeling, which owns persistence and entity shape — type-safety owns the in-memory type contracts that consume that shape. Distinct from input validation libraries (Zod, Yup, io-ts), which provide the runtime parsing mechanism — type-safety is the discipline that decides where parsing must happen because the type system cannot. Type safety is to programs what a passport check is to international travel — the document (type annotation) certifies identity within the issuing country's records, but on the way through customs (the I/O boundary), the document is re-verified against the actual traveler, and any mismatch is rejected before they enter the trusted zone. The wrong mental model is that a TypeScript as cast is a form of validation. It is not. The cast is a programmer-asserted claim that compiles unchecked at runtime, and JSON.parse(x) as User produces a value typed as User with zero verification that it actually has the fields a User must have. The misconception conflates two layers — the compile-time claim (which the compiler accepts) and the runtime guarantee (which the cast does nothing to establish). The discipline is to use runtime validators (Zod, io-ts, manual parse functions) at every I/O boundary and treat as as an explicit, justified, rare escape hatch — not as the default way to silence a type error.

Coverage

The discipline of using a type system to rule out classes of runtime errors before they occur. Covers what soundness means and where TypeScript (and other gradual systems) is unsound, structural vs nominal typing, type narrowing and exhaustiveness checking, the runtime boundary problem, the difference between any and unknown, when to use type assertions (rarely) and when to validate (always at I/O boundaries), and the connection to runtime validation libraries.

Philosophy of the skill

Types are claims about values; type-checking is proof-checking. A program that compiles is a program whose claims have been internally consistent — but a program is more than its compiler. Values that arrive from outside the program (HTTP responses, environment variables, parsed JSON, untrusted user input) have no type until you parse them, no matter what type annotation sits next to them.

The discipline of type-safety is to take the compile-time guarantees seriously and to know exactly where they stop. A codebase that pretends JSON.parse(x) as User is safe has confused a syntactic claim with a semantic guarantee. A codebase that validates at the boundary and trusts the type inside has correctly aligned the two layers.

In gradual systems like TypeScript, the discipline includes treating escape hatches (any, as, // @ts-ignore) as exceptional, justified, and rare — not as the default response to a type error.

Soundness — What the System Actually Promises

Practical TypeScript stance: Enable strict mode (strict: true), enable noUncheckedIndexedAccess, enable noImplicitAny. These flags close the most common leakage points. Without them, the system's guarantees are substantially weaker than developers assume.

Narrowing

Narrowing is the type checker's mechanism for refining a broad type based on control-flow evidence. Use it instead of casts.

function process(x: string | number | null) {
  if (x === null) return;            // narrows to string | number
  if (typeof x === 'string') {        // narrows to string
    return x.toUpperCase();
  }
  // here x is narrowed to number
  return x.toFixed(2);
}

Discriminated unions are the strongest pattern:

type Result =
  | { ok: true; value: User }
  | { ok: false; error: string };

function handle(r: Result) {
  if (r.ok) return r.value;  // narrows; `r.error` is not accessible here
  return r.error;            // narrowed to the error branch
}

Exhaustiveness Checking

Force the compiler to verify that all cases of a union are handled. The pattern uses an unreachable never branch.

type Method = 'GET' | 'POST' | 'PUT' | 'DELETE';

function describe(m: Method): string {
  switch (m) {
    case 'GET':    return 'safe';
    case 'POST':   return 'mutation';
    case 'PUT':    return 'idempotent replacement';
    case 'DELETE': return 'idempotent removal';
    default: {
      const _exhaustive: never = m;  // compile error if a case is missing
      throw new Error(`unhandled: ${_exhaustive}`);
    }
  }
}

When a new variant is added to Method, the never assignment fails to type-check — the compiler points at every missing branch. This converts a runtime "unhandled case" bug into a compile-time error.

The Runtime Boundary

Type information stops at the runtime boundary. Values crossing in must be parsed; values crossing out are serialized.

The pattern: validate at the boundary; trust the type inside.

import { z } from 'zod';

const UserSchema = z.object({
  id: z.string(),
  email: z.string().email(),
  createdAt: z.coerce.date(),
});

type User = z.infer<typeof UserSchema>;

async function fetchUser(id: string): Promise<User> {
  const raw = await fetch(`/api/users/${id}`).then(r => r.json());
  return UserSchema.parse(raw);  // throws on validation failure
}
// Inside the rest of the program, User is trusted.

any vs unknown vs never

Rule: prefer unknown over any always. The cost is one narrowing step; the benefit is type-safety preserved.

Verification

After applying this skill, verify:

• TypeScript strict mode is enabled ("strict": true in tsconfig).
• noUncheckedIndexedAccess is enabled; array/object access produces T | undefined.
• No any appears in committed code without an inline comment explaining why unknown is insufficient.
• No as Type cast appears without an inline comment explaining why narrowing is insufficient.
• Every I/O boundary parses with a runtime validator (Zod, io-ts, valibot, etc.) before the value is treated as typed.
• Discriminated unions have an exhaustiveness check at every consumer site.
• Public API boundaries (exported functions, route handlers, library entry points) have explicit return types — not just inferred.
• // @ts-ignore and // @ts-expect-error are accompanied by a justification and a tracking comment.

Do NOT Use When

Key Sources

• Pierce, B. C. (2002). Types and Programming Languages. MIT Press. The canonical textbook. Chapters 1-3 cover untyped lambda calculus, simple types, and the soundness/progress/preservation framework that underpins every type system.
• Siek, J. G., & Taha, W. (2006). "Gradual Typing for Functional Languages." Scheme and Functional Programming 2006. The original gradual typing paper.
• Siek, J. G., & Vachharajani, M. (2008). "Gradual typing with unification-based inference." Proceedings of the 2008 symposium on Dynamic languages. Formalizes the soundness vs ergonomics trade-off in gradual systems.
• Microsoft. TypeScript Handbook. The reference for TypeScript's type system, including the documented unsoundness in Type Compatibility and Narrowing chapters.
• Anders Hejlsberg et al. TypeScript Design Goals. Explicit acknowledgement that TypeScript trades soundness for ergonomics: "non-goals: apply a sound or 'provably correct' type system."
• Curry, H. B., & Feys, R. (1958). Combinatory Logic, Volume I. Original work on the Curry-Howard correspondence — types as propositions, programs as proofs.