The Laffer Curve of Types: Rethinking Expressiveness and Effectiveness in Migratory Typing

In a provocative essay, Matthias Felleisen, a prominent figure in programming language research and co-creator of Typed Racket, reframes type system design as an optimization problem akin to the Laffer Curve in economics. Originally published in April 2019 and updated through May, with contributions from collaborators like Robby Findler, Shriram Krishnamurthi, and Ben Greenman, the piece critiques the traditional focus on soundness and expressiveness. Instead, Felleisen advocates for a nuanced view prioritizing developer productivity and measurable effectiveness (source).

From Logic to Engineering

Felleisen notes that most researchers view types as theorems and type systems as proof checkers—a perspective rooted in logic. Over two decades of work on migratory typing, however, has led him to see type systems as interfaces between languages and humans. Migratory typing enables gradual adoption of static types in dynamically typed codebases, contrasting with 'gradual typing,' which Felleisen dismisses as inferior marketing despite its popularity.

The core analogy draws from the Laffer Curve, which posits that tax revenue peaks at an optimal rate—too low yields nothing, too high discourages work. Felleisen maps this to type systems:

Dynamic typing (0% 'tax') catches no errors at compile time.
An 'extremist' type system (100% 'tax') rejects all programs, rendering nothing executable.

Empirical evidence places effective systems like Java and Haskell between these extremes, with diminishing returns beyond a point. Refinement or dependent types might catch nearly all errors but impose such burdens that fewer programs run, lowering overall effectiveness.

Conceptual Laffer Curve for type expressiveness vs. effectiveness, adapted from Felleisen's essay.

Migratory Typing in Practice: Typed Racket

Migratory typing starts from existing dynamically typed code, where developers already employ 'type-like reasoning.' Typed Racket exemplifies this by requiring minimal changes to migrate modules. Consider this factorial example:

Untyped Racket:

#lang racket
(module+ test (require rackunit))
;; Natural -> Natural ; the factorial function
(module+ test (check-equal? (! 3) 6))
(define (! n)
  (if (= n 0)
      1
      (* n (! (- n 1)))))

Typed Racket:

#lang typed/racket
(module+ test (require typed/rackunit))
(: ! (Natural -> Natural)) ; the factorial function
(module+ test (check-equal? (! 3) 6))
(define (! n)
  (if (= n 0)
      1
      (* n (! (- n 1)))))

Only the language declaration and comment-to-annotation conversion change. Typed Racket's set-based numeric types (e.g., Natural) and induction-checking enable this without rewrites, though precision like Natural over Integer can demand extra code elsewhere.

Granularity, Dynamic, and Trade-offs

Felleisen categorizes migratory systems by granularity:

Micro systems often include Dynamic as a fallback, easing adoption but potentially weakening checks. Felleisen conjectures micro + Dynamic sees more uptake but less error prevention.

Soundness and completeness add layers: Typed Racket's 'wrapper' approach (per Ben Greenman, ICFP 2018; Max New, POPL 2019) offers a spectrum, where unsound systems like TypeScript risk subtle bugs at typed-untyped boundaries.

Open Challenges: Performance, Debugging, Benefits

Performance remains a hurdle; early Typed Racket suffered slowdowns despite optimizations. Felleisen urges quantitative evaluation, now standard in the field.

Debugging benefits from larger typed regions and soundness, as Dynamic obscures origins. Yet, unproven benefits like maintenance gains lack rigorous studies. The essay calls for empirical methods—user studies, corpus analysis—to map the 'Laffer Curve' precisely, criticizing the field for chasing publishable proofs over developer impact.

Felleisen's vision positions migratory typing as a bridge for real-world adoption, urging researchers to prioritize evidence-based design. As dynamically typed languages dominate, optimizing this curve could transform how developers scale and maintain codebases, proving types' value beyond academia.