Advanced Type Systems: Dependent Types, Linear Types, and Effect Systems for Compile-Time Correctness Guarantees

Abstract

A type checker is the most widely deployed program verifier in the world, run by millions of engineers who may never call it that. Most use only its weakest form, which catches little more than adding a number to a string. A richer tradition in programming-language research pushes the type system far further, until it can prove properties that today are checked, if at all, by tests and review. This paper surveys three of the most consequential of these advanced disciplines. Linear and affine types track the use of resources, guaranteeing that a file handle, a lock, or a block of memory is consumed exactly once, which eliminates leaks and use-after-free at compile time and underlies the ownership model that has recently reached mainstream systems languages. Effect systems make a function's side effects, its input and output, its exceptions, its access to state, part of its type, so the compiler can enforce that effects are handled and that pure code stays pure. Dependent types, the most powerful of the three, allow types to depend on values, collapsing the distinction between programs and proofs and making it possible to state and verify full functional correctness within the language itself. We explain the core idea behind each, trace how ideas once confined to proof assistants are entering production languages, and assess the cost, chiefly in type-checking complexity and programmer effort, that has kept the most powerful systems from widespread adoption.