intermediateTypes
What does a static type system give you?
Whether the candidate can state what a type system actually proves, versus what people hope it proves. The tell is precision about scope: a strong candidate volunteers the properties their type system does *not* model before being asked.
What a strong answer covers
- It gives you a proof, checked before the program runs, of the specific properties the type system models — usually that every operation is applied to operands of a shape it is defined for, and that every name refers to something of the type it is used as. Nothing more. A well-typed program in most mainstream languages can still divide by zero, exhaust memory, deadlock, index past the end of an array and produce entirely the wrong answer.
- It also gives you tooling. Types are what make jump-to-definition exact rather than heuristic, what make completion list the right members, what make a rename safe across a million lines, and what let a refactoring engine change a signature and be told every call site that no longer fits. In practice this is the benefit most teams feel most days.
- And it gives the compiler information: known layouts, known sizes, resolved call targets, opportunities for monomorphization and devirtualization. Dynamically typed implementations recover some of this at runtime with inline caches and speculation, and pay for it in warmup and complexity.
- The costs are real and worth naming. Annotation burden, or an inference algorithm complex enough that its error messages are famous. Programs that are correct but that the checker rejects, which pushes people toward escape hatches. Compile time. And a design pressure toward whatever the type system can express, which is not always the clearest design.
✓ Green flags
- Says what is proved, in terms of the specific properties modelled — and names something real that remains unproved.
- Separates the three benefits: guarantees, tooling, and compiler information, and does not conflate them.
- Names an escape hatch by name —
any,unsafe, an unchecked cast — and what it does to the guarantee. - Mentions soundness explicitly, and knows that some widely used type systems are deliberately unsound.
- Names a cost without prompting: annotation burden, rejected-but-correct programs, compile time.
✗ Red flags
- "It prevents bugs." It prevents a class of bug and says nothing about the rest. This answer is the single most common one and it is untestable — a candidate who says it usually cannot then name a bug that survives type checking.
- "Static typing prevents runtime errors." Null dereferences, integer overflow, array bounds and division by zero are runtime errors that most static type systems do not model at all.
- "If it compiles, it works." True only for the properties modelled, which in a mainstream language is a small fraction of what "works" means.
- "Dynamic languages have no types." They have types; the check happens at a different time, on values instead of expressions.
- "Types make it faster" offered as the primary benefit, with no mention of what the compiler does with the information or of JIT implementations that recover it dynamically.
Follow-up
Name a property this type system does not model, and describe how you would catch it instead. Then: is that type system sound, and if not, where is the hole?
Implementation challenge
What to ask them to write or trace on a whiteboard.
Write a five-line program that type-checks and is still wrong. Then extend the type system on paper — a new type, a new rule — so that it no longer type-checks, and say what correct program you just made illegal.