A language of
universal extension.

Every program is a Kan extension

Not a slogan — a claim the compiler will show you. A Kan program is a presentation: each definition is a generator, and the program's meaning is its initial model — a left Kan extension of the generators along their inclusion. Every definition is a fiber of that one construction: folds and matches are the rich fibers (genuine (co)limits and Kan extensions); a literal is the trivial fiber. Nothing is left out, and nothing is forced.

kan explain renders each definition as its fiber:

$ kan explain program.kan
Color    an inductive type {red | green | blue} — the initial algebra of its
         constructor functor (a colimit); its recursor is the unique mediating map
seven    a value — a generator with a defining equation; its universal completion
         is trivial (the terminal fiber)
parity   a fold over Color — the left Kan extension of its cases along the
         constructors ↪ Color
sumTo    a fold over ℕ (a catamorphism) — the left Kan extension of its zero/suc
         cases along {zero, suc} ↪ ℕ
Monoid   a signature — a dependent record type (a presented theory); its values
         are its models

The trivial fiber (seven) and the rich ones (sumTo, parity) are fibers of a single left Kan extension — the philosophy, rendered on your own code. This is what distinguishes Kan: not that it can express universal constructions, but that every program already is one.

And it's not just a picture — it's a theorem, checked in Kan. In examples/universal.kan the recursor fold is proved (by induction, not by refl) to be the unique map extending a ℕ-algebra — the universal property of the left Kan extension along {zero, suc} ↪ ℕ — and ordinary recursive add is shown to be exactly that fold. A real recursive function, exhibited with a machine-checked proof as a Kan extension. (Uniqueness is stated pointwise — the honest notion in a type theory without function extensionality.)

And it is becoming operational: a hole ? is a partial diagram the compiler completes. In check-mode it fills ? with the unique universal completion when the goal is contractible — Unit → unit, Σ → a pair, Π → a lambda, Id A a a → refl — so ? : (A:U) -> A -> Unit becomes λA a. unit; and when the goal has many inhabitants (Nat, Bool) it refuses and reports the goal ⊢ ? : T rather than guess. The compiler fills the horn — soundly, exactly when the completion is universal.

The idea

Most languages ask you to describe every step. Kan begins from what you actually know — some objects, some maps, some constraints — and treats the gaps as opportunities for universal construction.

Every paradigm has one computational act. The lambda calculus has application; logic programming has inference. Kan’s is extension: given a partial diagram, find the canonical object or morphism that completes it. Named for Daniel Kan — whose Kan extension and Kan complex both say the same thing: a partial diagram has a canonical filler.

Because that single primitive is the universal completion of a partial diagram, the deep constructions of category theory stop being separate theories and become one act at different shapes: a limit or colimit is a fill, a sheaf is the fill that glues compatible local sections into a unique global one, and a fibration is the fill that lifts a partial diagram along a map.

The seed

One sort, one relation, one operation. Cells (objects, morphisms, … as dimensions of one thing), their faces (which let a diagram be partial), and fill — complete a horn. Everything else is derived, and the modality dial decides how strong a completion to demand.

Pattern matching, total by construction

You write functions with match and structural recursion. A function is accepted only when the recursion is on a smaller piece of its input — so if it compiles, it terminates. Totality isn't a promise here, it's enforced. Both plain and accumulator-style recursion work (the argument may shrink or change); non-structural recursion is rejected.

-- addition, by pattern matching and structural recursion
def add : Nat -> Nat -> Nat = lambda m n: match m { | zero => n | suc k => suc (add k n) }

-- a generic map over lists
def map : (A : U) -> (B : U) -> (A -> B) -> List A -> List B
  = lambda A B f xs: match (xs : List A) { | nil => nil B | cons y ys => cons B (f y) (map A B f ys) }

A type is a theorem — and it compiles to native code

Kan is dependently typed: you state a program's property as a type, and the checker proves it. You prove things with the same match you compute with — the recursive call is the induction hypothesis. Here, a proof that add n 0 = n for every n; the proof is simply that it type-checks:

-- for ALL n, add n zero = n  —  a theorem, proved by induction with match
def add_n_zero : (n : Nat) -> Id Nat (add n zero) n
  = lambda n: match n { | zero  => refl
                | suc k => ap Nat Nat (lambda x: suc x) (add k zero) k (add_n_zero k) }

$ kan build nat.kan -o nat && ./nat
5
7

If it type-checks, the theorem holds — then it compiles to a native binary.

Unbounded integers — exact, and fast

Numbers in Kan are arbitrary precision, like Python's int. Nat is the inductive type you do proofs over; Integer is the machine-backed one you compute with. A Nat counter drives an Integer accumulator, so fac 50 is exact and instant — and identical from kan run, the OCaml backend, and the C backend.

-- a 65-digit factorial, by native big-integer multiplication
def fac : Nat -> Integer
  = lambda n: match n { | zero => 1z | suc k => imul (fromNat (suc k)) (fac k) }

eval fac 50

$ kan run integer.kan
30414093201713378043612608166064768844377641568960512000000000000

Exact rationals — divide-by-zero is a type error →   Exact reals →

And a step further: a rational whose den > 0 and lowest-terms invariants are proof fields the checker verifies — so ÷0 can’t be written, and every value is provably reduced. Built on a verified gcd. Beyond the rationals, constructive reals compute √2, π, e to any precision — exact on demand, still no divide-by-zero.

Category theory, in the language

The vision — programs are diagrams, computation is universal completion — is not just prose. A SmallCategory is a dependent record whose laws are fields, so a value of type SmallCategory is one the checker has verified. Functors, natural transformations, the opposite category, composition — all lawful. And the construction the language is named for is a definition you can check:

-- std/kan.kan — the Kan extension, stated as a universal property
def LeftKanExt : (A : SmallCategory) -> (B : SmallCategory) -> (D : SmallCategory)
                 -> Functor A B -> Functor A D -> U
  = lambda A B D p F:
      (L : Functor B D)
    * (unit : NatTrans A D F (compFunctor A B D p L))
    * ((G : Functor B D) -> NatTrans A D F (compFunctor A B D p G) -> NatTrans B D L G)

The extension along the identity is constructed — so the statement is inhabited, not empty.

Kan extensions, in Kan — the worked examples →

A short, checked tour: extending along the identity (both variances), the universal property computing, and Mac Lane’s “all concepts are Kan extensions” stated in the language.

Status

dependently typed · compiles to native · category theory  Kan is an early research language — real and running, with the categorical layer now inside it.

• ✓ Dependent types — Π, Σ, identity types, a universe hierarchy
• ✓ Pattern matching & structural recursion — total by construction (compiles ⇒ terminates)
• ✓ User inductive types (with parameters, e.g. List A) and induction — real proofs
• ✓ Unbounded Integer — arbitrary precision, exact fac 50
• ✓ Two native backends — OCaml and C, verified to agree
• ✓ Category theory, lawful — SmallCategory, Functor, NatTrans, and Kan extensions, laws checked
• ◦ Next: indexed families (Vec, Fin), record syntax, implicit arguments

Try it

# install — macOS / Linux, no OCaml required
curl -fsSL https://raw.githubusercontent.com/jackmitchelwidman/kan/main/install.sh | sh

git clone https://github.com/jackmitchelwidman/kan && cd kan   # grab the examples + stdlib
kan run   examples/tutorial.kan          # a runnable tour of the language, start here
kan run   examples/integer.kan           # unbounded arithmetic — exact fac 50
kan check examples/categories.kan        # category theory, lawful
kan build examples/tutorial.kan -o tut && ./tut   # compile to native (add -c for the C backend)

run and check are built into the binary — no toolchain to install. On Windows, use the PowerShell installer; full instructions in Getting Started. Every file in examples/ is a .kan program; the tutorial is the place to begin. Design doc: README · the example gallery, a hands-on tour, and the type-system notes are in /docs.