Type Systems Across Languages

Core Concepts

The spectrum from static to dynamic

Type systems do not form a simple binary. They occupy a spectrum defined by when types are checked, whether they are enforced at runtime, and whether the system is formally sound.

Java sits at the fully static end: every expression has a type determined at compile time, the JVM class verifier enforces structural constraints at load time, and the compiler rejects programs that violate type rules. Types are nominal — two types are compatible only if one explicitly extends or implements the other, regardless of structural similarity.

TypeScript occupies middle ground. Types are checked at compile time, but they are erased before the JavaScript runtime sees the code. There are no runtime type guards injected at typed/untyped boundaries. This is the key distinction between gradual typing and optional typing: in optional type systems, types are erased at compile time and untyped values can propagate through annotated code without enforcement. TypeScript is an optional system, not a gradual one.

Python's type hints behave the same way: the runtime ignores them entirely. The type checker (mypy, Pyright) is a separate tool layered on top of the language.

Nominal vs structural typing

Java's type compatibility is based on declared relationships. If Dog does not explicitly implement Animal, a Dog instance cannot be passed where Animal is expected — even if Dog has every method Animal requires. The compiler only trusts what is declared.

TypeScript's type compatibility is structural: two types are compatible if their shapes match. If an object has .name: string and .speak(): void, it is compatible with any type that requires those members, regardless of declared hierarchy. This makes TypeScript natural for working with JavaScript's object-literal idioms but opens the door to unsoundness.

Flow, Facebook's alternative JavaScript type checker, takes a hybrid approach: structural typing for objects and functions, nominal typing for classes. Flow tends to prioritize soundness over completeness, distinguishing it from TypeScript's pragmatic approach.

TypeScript's intentional unsoundness

TypeScript's goal is not to have a provably correct type system. Instead, it strikes a balance between correctness and productivity.

TypeScript's type system is intentionally unsound. The TypeScript team explicitly lists soundness as a non-goal, choosing to prioritize simplicity and usability instead. This is a documented design decision rooted in the practical reality that TypeScript must handle all valid JavaScript, including patterns that resist static analysis: dynamic property access, prototype manipulation, any-typed library APIs, and covariant arrays.

TypeScript explicitly acknowledges that type annotations may not reflect actual runtime values. Accepting this is the cost of incremental adoption and broad JavaScript interoperability.

The academic alternative — systems like Typed Racket — prioritize soundness as a necessity. They insert runtime contracts at typed/untyped module boundaries to enforce type guarantees at runtime. The cost is migration friction: developers must carefully design module boundaries and reason about contract overhead. Research shows this friction slows adoption. TypeScript's bet is that looser interoperability beats formal guarantees for real-world adoption.

Java sidesteps this tension by never having been dynamically typed. Its type system does not need to accommodate untyped legacy code, which is why it can afford to be sound.

Control-flow analysis and type narrowing

A major strength of TypeScript (and Python's type checkers) is flow-sensitive type narrowing: the type of a variable can differ at different points in the program based on what the control flow has established.

TypeScript's control-flow analysis (CFA) tracks execution paths through if/else branches, typeof, instanceof, truthiness checks, and equality comparisons. The same variable can have different inferred types on different branches:

function process(value: string | number) {
  if (typeof value === "string") {
    // value is narrowed to string here
    console.log(value.toUpperCase());
  } else {
    // value is narrowed to number here
    console.log(value.toFixed(2));
  }
}

TypeScript calls these patterns type guards. Discriminated unions extend this further: a union of types that each carry a unique literal discriminant field enables exhaustiveness checking via the never type — if a switch statement omits a case, the remaining value gets type never, producing a compile error. This is TypeScript's analog of Java's sealed classes and pattern matching exhaustiveness.

The theoretical foundation for this kind of narrowing is occurrence typing, formalized by Tobin-Hochstadt and Felleisen at ICFP 2010. Occurrence typing assigns types to variable occurrences (individual uses) rather than declarations, combining propositional logic with set-theoretic types (unions, intersections, negations) to refine types based on control-flow predicates. Explicit logical inference rules govern how type information is narrowed: the L-SUB rule, L-SUBNOT rule, L-BOT rule, and L-UPDATE rule together enable the system to reason about propositional satisfiability over types.

Python supports a similar pattern via isinstance(). Type checkers like mypy and Pyright narrow the type of a variable after an isinstance check, making isinstance — already idiomatic in dynamic Python — do double duty as a type guard for static analysis.

Java takes a different approach. Rather than flow-sensitive narrowing over arbitrary conditions, it uses explicit pattern matching in instanceof:

Object obj = getObject();
if (obj instanceof String s) {
    // s is already typed as String, no explicit cast needed
    System.out.println(s.toUpperCase());
}

Java's sealed classes and switch pattern matching (stable since Java 21) allow exhaustiveness checking comparable to TypeScript's discriminated unions, but through the nominal type hierarchy rather than structural shape.

Kotlin's smart casts occupy a middle position. After an is check, Kotlin automatically narrows the type within the branch. However, this only works for provably immutable variables. Mutable class properties do not benefit from smart casts because another thread could change the property between the check and the use.

Type inference: var, local inference, and Hindley-Milner

A common assumption when coming from TypeScript or Haskell is that type inference means the compiler figures out types everywhere. In Java, this is not the case.

Hindley-Milner type inference, implemented via Algorithm W, infers principal types — the most general type for any expression — through global constraint unification. This enables nearly complete omission of type annotations, as in Haskell or OCaml.

Java's var (introduced in Java 10) uses local type inference. Local type inference, as described by Pierce and Turner, infers types from information in adjacent syntax nodes, propagating constraints bidirectionally (synthesizing types upward, checking them downward) without global unification. var can only infer the type of a local variable from its initializer:

var list = new ArrayList<String>(); // inferred as ArrayList<String>
var x = someMethod();               // inferred from return type of someMethod()

You cannot use var for method parameters, return types, or fields. This is a deliberate constraint: Java's local inference is bounded and predictable. It improves readability without requiring global reasoning.

Bidirectional type checking — splitting inference into a synthesis mode (derive a type from the term) and a checking mode (verify a term against a given type) — remains decidable even for expressive type systems where full unification-based inference would be undecidable. This property underpins Java's local inference and is why bidirectional checking has become the dominant paradigm in modern language design.

TypeScript's type inference is also local in this sense — it does not perform Hindley-Milner global unification. But it propagates types across more contexts than Java's var, including generic call sites and lambda parameter types.

Null safety across languages

Null is a source of runtime errors in every language that has it. The approaches to containing null diverge significantly:

Java does not have null safety at the language level. null is assignable to any reference type. Optional<T> is a library wrapper that signals intent: a method returning Optional<String> is explicitly declaring it might return nothing. But Optional is not enforced — code can still call .get() without checking, and null can still be passed where Optional<T> is expected. It is a convention, not a contract.

TypeScript with strictNullChecks makes null safety opt-in at the project level. Introduced in TypeScript 2.0, strictNullChecks treats null and undefined as distinct types, not assignable to other types unless the union is explicit. With this flag enabled, string | null and string are different types. CFA handles narrowing: after if (value !== null), the null is excluded from value's type in that branch. The crucial caveat: this flag is off by default, reflecting TypeScript's gradualist philosophy.

Kotlin integrates null safety into the type system unconditionally. String is non-nullable; String? is nullable. The compiler enforces the distinction at every point. Smart casts handle narrowing after null checks. This is the tightest null safety of the three — without the escape hatch of any.

Compare & Contrast

Dimension	Java	TypeScript	Python (mypy)
Type discipline	Static, mandatory	Static at compile time, erased at runtime	Optional, checked by external tool
Nominal vs structural	Nominal	Structural	Structural (duck typing + hints)
Soundness	Near-sound (caveats: raw types, unchecked casts)	Intentionally unsound	Mypy aims for soundness within annotated code
Runtime enforcement	Yes (JVM verifier, runtime casts)	None (full erasure)	None (annotations are metadata only)
Flow-sensitive narrowing	Pattern matching instanceof (explicit, nominal)	CFA with type guards (implicit, structural)	isinstance() narrowing (explicit)
Type inference scope	Local only (var)	Local + call sites	Local + call sites
Null safety	Optional by convention, no enforcement	strictNullChecks opt-in	Optional[T] by convention, checked by tool
Full HM inference	No	No	No

Common Misconceptions

"TypeScript is a sound type system with some edge cases." This understates the design intent. TypeScript's team explicitly lists soundness as a non-goal. Unsoundness is not a bug backlog — it is a documented tradeoff. Bivariant function parameters, covariant arrays, and any are features of the design, not accidents to be fixed.

"Java's var is like TypeScript's type inference — it just figures things out." Java's var is bounded local inference: it works only for local variable initializers and only when the right-hand side has an unambiguous type. TypeScript and Haskell propagate type information far more broadly. Java deliberately chose the conservative form to keep inference predictable and bounded.

"Python type hints enforce types at runtime." They do not. Python's type hints are annotations — metadata accessible via typing.get_type_hints() but not evaluated or enforced by the interpreter. A true gradual type system inserts runtime checks at typed/untyped boundaries; Python does not. The type checker (mypy, Pyright) is a separate process.

"Java's Optional is equivalent to Kotlin's nullable types." Optional<T> is a library class, not a language primitive. It does not prevent null from existing in your codebase, does not prevent passing null where Optional<T> is expected, and adds an allocation. Kotlin's T? is enforced by the compiler with no overhead. They solve the same problem with very different levels of enforcement.

"Gradual typing and optional typing are the same thing." They are not. Gradual type systems insert runtime checks at typed/untyped boundaries. Optional type systems erase types before execution. TypeScript and Python are optional systems. A true gradual system like Typed Racket maintains runtime contracts at module boundaries.

Thought Experiment

You are designing a new API gateway service that will be consumed by three teams: one using Java, one using TypeScript, and one using Python with mypy. You need to define a contract for a function that returns a user profile, which may or may not exist.

In each language, how would you represent "this value might be absent"? What guarantees does each representation give to the caller? What can go wrong if the caller ignores the signal?

Now consider: if you generate client SDKs from an OpenAPI spec, how much of the null-safety contract is preserved across the boundary? What happens when TypeScript's erased types meet a Java service that throws NullPointerException? When Python's runtime-ignorant annotations meet a Go service that returns zero values?

There is no single correct answer. The exercise surfaces how much type safety is a local property of a single language runtime versus a distributed property of an API contract enforced — or not — across language boundaries.