A language of
universal extension.

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.