What Is a Type System

Hindley, Milner, and Type Inference

In 1969, Roger Hindley described a type inference algorithm for combinatory logic. In 1978, Robin Milner independently developed the same system for the ML language and proved the theorem: 'well-typed programs don't go wrong' - correctly typed programs cannot raise a type error. This was the first formal guarantee of soundness. The Hindley-Milner system underlies Haskell, OCaml, F#, and Elm - and inspired TypeScript's inference. For this and other contributions, Milner received the Turing Award in 1991.

Цели урока

• Define a type as a set of values plus a set of operations
• Distinguish type safety, soundness, and completeness
• Explain why TypeScript is unsound and why that is a deliberate choice
• Understand why no language can be simultaneously sound and complete

TypeScript's type system is Turing-complete. It can compute Fibonacci numbers at compile time. This was not intended - it is a consequence of conditional types combined with recursive types yielding Turing completeness. That is precisely why TypeScript cannot guarantee type checking terminates on all programs, and Microsoft caps recursion depth by force.

• **Ariane 5 (1996)** - integer overflow on a type cast. USD 370 million. Modern Rust or Haskell would have refused to compile that code
• **TypeScript** - 10+ million projects. A deliberate choice of unsoundness for JavaScript compatibility and developer convenience
• **Rust borrow checker** - a sound system for memory safety: if it does not compile, there are no data races at runtime. Mozilla, Google, and Microsoft are adopting Rust
• **Haskell in fintech** (Standard Chartered, Mercury) - sound type system as a guarantee of correctness for financial computations
• **Agda/Coq** - dependent types as formal verification: a type is a proof of a theorem. Cryptographic protocol verification

Type = Set + Operations

On June 4, 1996, the Ariane 5 rocket exploded 37 seconds after launch. The loss: USD 370 million. The cause: **integer overflow** - a 64-bit velocity value was cast to a 16-bit integer and did not fit. Ada's type system did not prevent this cast. Not because types are powerless - because this specific operation was not forbidden. Modern Rust or Haskell would have refused to compile that code.

**A type is a set of admissible values and a set of operations** applicable to those values. Not just the word `int` or `string` in code - it is a contract. Violating the contract = error.

**Key idea:** a type is not just a label. It is a **contract**: 'here is what I can hold, here is what can be done with me'. Violating the contract = error. Ariane 5 violated a type contract - and it cost USD 370 million.

Type Safety: Protection from Nonsense

A language is called **type safe** if it does not allow operations to be applied to values of incompatible types. The degree of protection varies enormously. C lets a pointer to int be cast to char* and written to arbitrary memory - the compiler says nothing. Rust refuses to compile the analogous code.

**Type safety is not the same as static typing.** Python is type safe (it disallows adding int + str at runtime) but is dynamically typed. C is statically typed but NOT type safe (void*, arbitrary casts).

The higher the level of type safety, the more errors are caught **before** code reaches the user. The difference between checking luggage at the gate and checking it mid-flight.

Soundness: Guarantees Without Surprises

Code passed type checking. The compiler said OK. Does that guarantee no type errors at runtime? **It depends on whether the type system is sound.** TypeScript says OK - and still crashes at runtime with `TypeError: Cannot read property 'toUpperCase' of undefined`. Haskell says OK - and guarantees that cannot happen.

**Sound type system** = if a program passes type checking, **there are guaranteed to be no type errors at runtime**. Robin Milner's formulation (1978): 'Well-typed programs don't go wrong.'

**Unsound does not mean bad.** TypeScript deliberately sacrifices soundness for convenience. The team's position: 'it is better to catch 95% of errors comfortably than 100% painfully'. This is an engineering tradeoff, not a flaw.

Completeness: False Positives

A sound system guarantees: 'if it passed the check - there will be no errors'. What about the converse? Can a **correct program fail the type check**? Yes. And this is not a bug - it is a fundamental mathematical limitation.

**Complete type system** = all correct programs pass type checking. If a program works correctly, the compiler **will necessarily** accept it. In practice, **no real-world type system is complete**.

**Rice's theorem** (computability theory): for any non-trivial property of programs, it is impossible to build an analyzer that is simultaneously sound AND complete. This is a **fundamental limitation**, not an oversight by language designers.

Every language makes its own choice on this spectrum. **Haskell** and **Rust** sacrifice completeness for guarantees. **TypeScript** sacrifices soundness for JavaScript compatibility. **Python** is maximally complete (no static checking), but soundness is only enforced at runtime.

Key Ideas

• **Type** = set of values + set of allowed operations. int - numbers + arithmetic, string - text + concatenation
• **Type safety** = the language does not allow operations on incompatible types. C - no, Python/Java/Rust - yes
• **Soundness** = if the compiler said OK, there will be no type errors at runtime. Haskell/Rust - sound, TypeScript - no
• **Completeness** = all correct programs pass type checking. No real-world language is fully complete
• **Rice's theorem** makes simultaneous soundness and completeness mathematically impossible
• TypeScript deliberately sacrifices soundness for convenience - an engineering tradeoff, not a defect

Related Topics

The type system is the foundation on which many other concepts are built:

• Static vs Dynamic Typing — When type checking happens - at compile time or at runtime
• Type Inference — How the compiler determines types without explicit annotations (HM algorithm)
• Polymorphism — How a single type can take different forms - generics, subtypes, ad-hoc

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

• Which tradeoff would a new language choose - soundness (like Rust) or convenience (like TypeScript)? Why?
• Why did TypeScript become more popular than Haskell, even though Haskell has a stronger type system?
• TypeScript's type system is Turing-complete - is that good or bad? What does it mean for the type checker?

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

• plt-03-static-vs-dynamic — When type checking happens: compile time vs runtime
• plt-04-type-inference — How the compiler infers types without explicit annotations (HM)
• plt-08-generics — Polymorphism - types that take different forms
• fl-25-rice-theorem — Rice's theorem explains why soundness and completeness cannot coexist
• fl-02-chomsky — Type system expressiveness correlates with Chomsky hierarchy levels
• plt-09-dependent-types — Dependent types - the power ceiling: type checker may not terminate
• ml-01