Typed Racket: Sound Gradual Typing with Occurrence Typing and Typed/Untyped Boundaries

The Problem: Static Types Without a Full Rewrite

Racket programmers often want static type checking for core algorithms but need the flexibility of untyped code for I/O, scripting, and third‑party libraries. Typed Racket solves this with a gradual typing system: you write modules in #lang typed/racket, get static checking and JIT‑optimized code, and interoperate soundly with untyped #lang racket modules through explicit boundaries that enforce contracts at runtime.

Useful Takeaway

Put performance‑critical, algorithmic code in Typed Racket modules. Keep I/O, configuration, and untyped library glue in plain Racket. Connect them with require/typed boundaries that specify precise function signatures. This gives you static guarantees where they matter most, without rewriting your whole codebase.

How It Works: Module‑Level Language Choice

Each file begins with a language declaration. A typed module:

#lang typed/racket

(define (safe-div [x : Real] [y : Real]) : Real
  (if (zero? y)
      0
      (/ x y)))

The : Real annotations on parameters and the result are mandatory for top‑level bindings. The type checker runs at module expansion time (via raco make or racket) and rejects ill‑typed programs before they run.

Occurrence Typing: Refinement Without Casts

Inside a typed module, predicates refine types in each branch. After (integer? x), the then branch sees x : Integer; the else branch sees x : (U Integer String) (a union). No explicit casts are needed.

#lang typed/racket

(define (describe [v : (U Integer String)]) : String
  (if (integer? v)
      (format "int: ~a" v)        ; v is Integer here
      (format "str: ~a" v)))      ; v is String here

This works for user‑defined predicates too, provided they are defined in typed code and their return type is a predicate type like (-> Any Boolean : Integer).

Crossing the Boundary: require/typed

An untyped module io.rkt exports a function that reads a number from a port:

#lang racket

(define (read-number [p : input-port?])
  (let ([line (read-line p)])
    (string->number line)))

A typed consumer declares the expected signature and gets a contracted wrapper:

#lang typed/racket

(require/typed "io.rkt"
  [read-number (-> Input-Port (U Number #f))])

(define (process [p : Input-Port]) : Number
  (match (read-number p)
    [(? number? n) n]
    [_ 0]))

At runtime, every call to read-number checks that the argument is an input port and that the result is either a number or #f. If the untyped code returns a string, the contract raises a contract-violation error at the boundary—preserving soundness.

Parametric Polymorphism

Type variables are introduced with All (written ∀ in Unicode). The identity function:

#lang typed/racket

(define (id [x : A]) : A x)  ; A is implicitly universally quantified

At each call site, A is instantiated to the argument's type. This works for higher‑order functions too:

(define (map-id [f : (All (A) (-> A A))] [lst : (Listof A)]) : (Listof A)
  (map f lst))

Note: higher‑order polymorphic contracts at typed/untyped boundaries can cause exponential checking overhead. Prefer first‑order boundaries (functions consuming/producing base types) where possible.

Struct Types Are Nominal

Two structs with identical fields are distinct types unless they share a supertype:

#lang typed/racket

(struct: point ([x : Real] [y : Real]))
(struct: vec   ([x : Real] [y : Real]))

; (point 1 2) and (vec 1 2) are NOT interchangeable
; even though they have the same fields.

Use #:super to create a common supertype when structural compatibility is intended.

Common Mistakes and Limits

Mutable Fields Break Occurrence Typing

If a struct field is #:mutable, the type checker cannot assume its value stays the same between a predicate check and its use:

#lang typed/racket

(struct: box ([val : (U Integer String) #:mutable]))

(define (bad [b : box]) : Integer
  (if (integer? (box-val b))
      (box-val b)          ; ERROR: type may have changed
      0))

Workaround: read the field into a local immutable binding first.

Recursive Bindings Need Explicit Annotations

The type checker cannot infer types for mutually recursive bindings unless at least one binding in the group has an explicit annotation:

#lang typed/racket

; This fails without annotations:
(define (even? n) (if (zero? n) #t (odd? (sub1 n))))
(define (odd? n)  (if (zero? n) #f (even? (sub1 n))))

; Fix: annotate one:
(define (even? [n : Integer]) : Boolean
  (if (zero? n) #t (odd? (sub1 n))))
(define (odd? [n : Integer]) : Boolean
  (if (zero? n) #f (even? (sub1 n))))

Missing Typed Bindings for Libraries

Many Racket libraries lack typed exports. Writing accurate require/typed signatures for complex untyped APIs is error‑prone. Start by typing only the functions you actually call, using broad but safe types like (-> Any Any) initially, then refine as needed.

Performance Profile

Typed Racket compiles to optimized machine code via the JIT. Crossing a typed/untyped boundary incurs contract‑check overhead proportional to the size of the values being checked (e.g., traversing a large list). Benchmark to decide whether a boundary belongs in a hot loop.

Verification Checklist

1. Basic type check: Create test.rkt with the safe-div example above. Run racket test.rkt (no special permissions). It should execute without type errors.
2. Static rejection: Add (safe-div 1 "two") to the file. Run raco make test.rkt. The type checker must report a type mismatch before runtime.
3. Boundary overhead measurement: Write a typed function called 1,000,000 times from an untyped module via require/typed. Compare runtime with a fully typed version using racket -t benchmark.rkt. Expect measurable overhead for non‑trivial value checking.
4. Documentation currency: Check docs.racket-lang.org/typed_racket/ for any changes to occurrence typing rules or contract semantics.

Practical Pattern: Typed Core, Untyped Shell

Layer	Language	Typical Content
Core algorithms	#lang typed/racket	Data transformations, parsers, analyzers, numeric kernels
I/O & scripting	#lang racket	File handling, CLI parsing, network requests, config loading
Boundaries	require/typed	Explicit signatures on every cross‑layer function

Use #lang typed/racket/base for a smaller dependency footprint when you don't need the full typed/racket library re‑exports.