Type systems: System F, dependent, linear

Once you have the simply-typed lambda calculus (STLC) and Hindley-Milner, there's a whole landscape of richer type systems above. Each extends the core with a new ability — quantifying over types, letting types depend on values, tracking resource usage — and each pays a price in inference, decidability, or implementation complexity. This is a map of the territory.

The lambda cube

Henk Barendregt's λ-cube organizes typed λ-calculi along three axes:

The corners are named: STLC (no axes), System F (polymorphism), Fω (polymorphism + operators), λΠ (dependent), Calculus of Constructions (all three) — the basis of Coq.

System F (a.k.a. polymorphic λ-calculus)

System F adds type abstraction (Λ) and type application:

id  =  Λα. λ(x : α). x          ;; "for any type α, λx.x at type α → α"
id [Int] 5                       ;; instantiate α := Int, then apply

That's the term-level explanation for HM's "let-generalization": HM implicitly inserts Λ at let-bindings and the type application at use sites.

Cost: type inference is undecidable in full System F. HM is the sweet-spot restriction (prenex/rank-1 polymorphism only) where inference is decidable.

Dependent types

In dependent types, terms appear inside types. The function-type arrow generalizes to Π (dependent product):

ident   : ∀a. a → a                ;; System F: type doesn't see value
replicate : Π(n : Nat). Π(a : Type). a → Vec n a
                                    ;; Vec n a depends on the value n

Now replicate 3 "x" has the static type Vec 3 String — the length is in the type. The compiler can refuse head v where v : Vec 0 a.

Languages: Agda, Idris, Lean, Coq, F* (proof assistants), and lean mainstream entries are emerging — TypeScript-style "literal types" are a restricted form of dependent typing in practice.

Cost: type-checking is sound but slow; you must often supply proofs the checker can't find. Most code becomes mixed term-and-proof.

Linear and affine types

A linear type system requires each value to be used exactly once; affine requires at most once (so dropping is OK). This tracks resources: file handles, memory, mutable state.

;; pseudocode
file ⊸ String              ;; "uses the file linearly, returns a String"

let (contents, file') = read file    ;; original file is consumed
let _                  = close file' ;; new handle is consumed
;; reusing the original `file` here is a *type error*

Linear types let you have safe in-place mutation with pure semantics (Haskell's linear-base, Rust's borrow checker is a linear-ish discipline with extra rules about lifetimes), and they support session types for protocols (see track G).

Languages: Linear Haskell, Rust (substructural via affine ownership + borrows), Clean (uniqueness types — a sibling discipline).

Refinement types

Halfway to dependent: types are predicates over an underlying type.

type Nat   = { v : Int | v >= 0 }
type Bounded = { v : Int | 0 <= v && v < 100 }

LiquidHaskell, Refinement F#, Dafny, and to some extent Idris's predicates take this route. Inference is delegated to an SMT solver (Z3) so users write the predicates and the machine checks them.

How the landscape relates

STLC
  + ∀types         → System F
  + type ops       → System Fω
  + dependent      → λΠ → Calc. of Constructions → Coq, Agda, Lean
  + classes        → Haskell (HM + Fω fragments + classes)
  + subtyping      → TypeScript, Scala (loses principal types)
  + linearity      → Linear Haskell, Rust
  + refinements    → LiquidHaskell, F*

Every "real" language is a particular slice. Knowing the slice helps you predict what the type system can and can't express.

Try the idea in Clojure (with malli or spec)

Clojure is dynamically typed, but you can simulate refinement-style and dependent-style constraints at runtime via specs:

This isn't "real" dependent typing — there's no static guarantee — but the shape of the predicate is the same one a refinement type would carry. The checker just runs at the boundary instead of at compile time.

Real-world: each slice in production

The cost-vs-benefit is always the same shape: stronger guarantees mean more code-time work, but pay off where bugs are catastrophic or expensive.

Check yourself

Exercise

Write down (in pseudo-syntax) the type of map in:

1. Simply-typed λ-calculus restricted to Int.
2. System F.
3. A dependent system tracking length: a map that preserves the length of its input vector.

What inference burden does each impose on the programmer?