Type Systems and Programming Styles

A type system classifies values and expressions and imposes rules on how they may be used.

8.1 What is a type system?

A type system classifies values and expressions and imposes rules on how they may be used. It can catch certain errors before execution or constrain behavior at runtime.

8.2 Static and dynamic typing

Static typing: many type checks occur before the program runs.

Dynamic typing: type checks are performed during execution.

Type inference: the system derives types from expressions without requiring every type to be written explicitly.

Gradual typing: a program can combine statically checked and dynamically checked portions, depending on language and tooling.

Checked with the TypeScript compiler (tsc --strict) after uncommenting the assignment: Python example:

Output (CPython 3.13.1, with print(count, type(count).__name__) appended):

Python type annotations help tools but are not generally enforced by the standard runtime. Type checking behavior depends on the language and tooling.

let count: number = 3;
// count = "three"; // Type error in TypeScript (TS2322)

b.ts(2,1): error TS2322: Type 'string' is not assignable to type 'number'.

count: int = 3
count = "three"  # Python normally permits this at runtime.

three str

8.3 Nominal and structural typing

Nominal typing: compatibility is based on declared type identity or explicit relationships.

Structural typing: compatibility depends on the members or shape a value provides.

TypeScript uses structural typing in many situations:

Output (Node.js 24.18, with console.log(distanceFromOrigin({ x: 3, y: 4 }))):

type Point = { x: number; y: number };

function distanceFromOrigin(point: Point): number {
  return Math.sqrt(point.x ** 2 + point.y ** 2);
}

distanceFromOrigin({ x: 3, y: 4 }); // 5

8.4 Static types do not prove correctness

A type checker may show that a value has the expected shape, but it does not necessarily prove that:

A user is authorized A number is in a valid business range A remote service is available A value came from a trusted source A transaction is atomic A cryptographic protocol is correct

Use types with runtime validation, tests, and explicit invariants.

8.5 Algebraic data types

Product type: a value containing multiple components, such as a record or tuple.

Sum type: a value that is one of several alternatives.

Option/Maybe: a value may be present or absent.

Result/Either: a computation can return a success value or an error.

Recursive type: a type defined in terms of itself, such as a tree.

These types help represent domain states explicitly instead of relying on ambiguous sentinel values.

8.6 Refinement and dependent types

A refinement type restricts a base type with a predicate, conceptually such as “integer greater than zero.” A dependent type can express types that depend on values. Support and expressive power vary by language and system.

Conceptual notation:

This is mathematical-style pseudonotation, not valid syntax in most mainstream languages. In ordinary languages, enforce the condition through constructors, validation, smart types, or runtime checks.

PositiveInteger = { n: Integer | n > 0 }

8.7 Type classes, traits, interfaces, and protocols

These mechanisms describe shared behavior:

Interfaces and protocols specify required operations.

Traits can provide behavior and constraints.

Type classes describe capabilities associated with types in languages such as Haskell.

Generic bounds constrain which types can be used in a generic algorithm.

Do not confuse shared method names with identical behavior. Contracts include semantics and invariants.

8.8 Subtyping and variance

Covariance: a generic type preserves a subtype relationship in a particular position.

Contravariance: reverses that relationship.

Invariance: neither direction is allowed.

Variance rules prevent unsafe substitutions, especially with mutable containers and function types. Exact rules differ by language.

Exercise

Model an API response with explicit success and failure types. Compare a null-based design, an exception-based design, and a Result-style design.

Quiz

? Why does `let count: number = 3; count = "three";` fail in TypeScript but `count: int = 3; count = "three"` run in Python?
+ TypeScript checks types before running; Python's annotations are not enforced by the standard runtime. :: A real tsc run reported TS2322; a real CPython run printed `three str`.
- Python has no types. :: Python is dynamically typed; values still have types.
- TypeScript is a compiled language and Python is not. :: Compilation is not the point — static checking is.
- Both should fail. :: Python does not enforce annotations at runtime.

? Which statements about structural typing are correct? (select all that apply)
+ Compatibility depends on the members a value provides. :: That is the definition.
+ `{ x: 3, y: 4 }` is accepted where `Point` is expected without declaring it a Point. :: The real run printed 5.
- Two types with different names are never compatible. :: That describes nominal typing.
- It means types are checked only at runtime. :: TypeScript checks structure before running.

? What can a static type checker NOT prove on its own?
+ That a user is authorised to perform an action. :: Authorization is a runtime business rule.
- That a value has the 
…