• What is a type system?
• Static vs dynamic typing
• Strong vs weak typing (and why the terms are fuzzy)
• Nominal typing and subtyping
• Structural typing and duck typing
• Parametric polymorphism (generics)
• Subtyping polymorphism (OO)
• Type inference (preview)
• Soundness, completeness, progress/preservation
• Exercises

• Assigns types to expressions; rules govern typing derivations.
• Goals: correctness (catch errors), optimization, documentation, tooling.
• Formalized via judgments Γ ⊢ e : T and typing rules.

Γ ⊢ e1 : T1 → T2, Γ ⊢ e2 : T1 ⇒ Γ ⊢ e1 e2 : T2

• Static: checked at compile time; errors prevented before execution.
• Dynamic: checked at runtime; flexible but may fail later.
• Gradual typing blends static and dynamic with explicit boundaries.

• Often marketing terms; better to discuss implicit conversions and safety guarantees.
• Coercions can be explicit (safe) or implicit (risky if surprising).
• Soundness matters: avoid undefined behaviors and ill-typed operations.

• Types identified by names; subtyping declared (class/interface hierarchy).
• Variance for generics: covariant, contravariant, invariant parameters.
• Liskov Substitution Principle: substitutability constraints.

List[Cat] ⊑ List[Animal]? Depends on variance of List[T]

• Type compatibility by structure (fields/methods), not names.
• Common in TypeScript, Go interfaces, OCaml object types.
• Pros: flexibility and interoperability; cons: accidental compatibility risks.

type Point = { x: number, y: number }
function len(p: { x: number, y: number }) { /* ... */ }

• Functions/types abstract over type parameters with uniform behavior.
• Monomorphization vs reified generics; constraints/traits bound operations.
• Relation to type inference and specialization.

fn max(a: T, b: T) -> T { if a > b { a } else { b } }

• Dynamic dispatch via vtables or fat pointers; interface/trait objects.
• Subtyping vs implementation inheritance; composition over inheritance.
• Binary compatibility and ABI impact method dispatch.

• Constraint generation and solving; unification (preview of Hindley–Milner).
• Local vs global inference; annotation strategies.
• Trade-offs: usability vs predictability.

• Progress: a well-typed term is a value or can take a step.
• Preservation: types are maintained by evaluation.
• Together imply type soundness for the language core.

If Γ ⊢ e : T and e → e' then Γ ⊢ e' : T (Preservation)

1. Model nominal vs structural typing for a small OO language; demonstrate variance pitfalls.
2. Design a generic container API in two languages (e.g., Rust and Java) and compare.
3. Explore gradual typing by adding runtime checks at module boundaries.