Gradual typing with core.typed

Clojure is dynamically typed, and that's a deliberate design choice — but sometimes you want specific functions or namespaces to be type-checked at compile time. core.typed (and its successor Typed Clojure) annotates Clojure code with optional types and runs a static checker over them. The project is research-flavored, less actively used than Malli/Spec, but the ideas are the gold standard for gradual typing in a Lisp.

Note: core.typed is a library, and the static checker runs at build/REPL time (clojure.core.typed/check-ns). Examples below show the shape; they will not run in the embedded SCI REPL.

Annotating a function

A type annotation declares the input/output types. The checker verifies the body matches; callers must pass compatible values.

(require '[clojure.core.typed :as t])

(t/ann square [t/Num -> t/Num])
(defn square [x] (* x x))

[t/Num -> t/Num] reads "takes a number, returns a number." The checker now flags any caller that passes a non-number, and any body that returns something else.

Heterogeneous types

core.typed distinguishes structural shapes:

(t/ann full-name '{:first String :last String} -> String)
(defn full-name [{:keys [first last]}]
  (str first " " last))

The map type '{:first String :last String} is structural — any map with at least these keys of these types is acceptable.

Union and intersection

Sum types are first-class. Use (U a b) for "either a or b" and (I a b) for "both a and b":

(t/ann parse-bool [(U String Boolean) -> Boolean])
(defn parse-bool [v]
  (if (boolean? v) v (= "true" v)))

Pair this with occurrence typing: inside the if, the checker knows v is Boolean; in the else branch, it knows v is String. The narrowing is automatic.

Where gradual typing earns its keep

• Library boundaries. Annotate the public surface; let the rest stay dynamic.
• Numeric and shape-heavy code. Catches "I returned a vector where the caller expected a number" mistakes that example tests miss.
• Domains with many small data shapes. Type aliases turn ad-hoc maps into named contracts.

Trade-offs and what to use instead

core.typed's checker is slow, the annotation surface is large, and the community has mostly moved on. For most modern projects:

• Spec / Malli — runtime validation, generative testing, openable maps; optional and incremental.
• Typed Clojure (typed.clj.checker) — the active research line if you do want a static checker.
• Plain :pre / :post conditions — lightweight runtime guards on individual functions.

The takeaway is conceptual: in Clojure, types are one tool among many. Schemas, generative tests, REPL exploration, and discipline at the boundary all contribute to safety. core.typed shows what fully static checking can look like in a Lisp.

Check yourself

Exercise

Sketch type annotations for two functions in a hypothetical project:

(t/ann add-tax  ,,, )
(defn add-tax [price rate] (* price (+ 1 rate)))

(t/ann lookup  ,,, )
(defn lookup [users id]
  (some (fn [u] (when (= (:id u) id) u)) users))

For lookup, your return type should reflect that the user might not be found — i.e. it should be a union with nil.