The Kan Programming Language

A language of
universal extension.

Programs are diagrams. Computation is extension. The compiler fills the horn.

A Kan program is a partial diagram awaiting universal completion.

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.

Composition isn’t primitive in Kan. Two composable arrows form a horn; you fill it, and the new edge is their composite.

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.

fill … Exists

Some filler must exist. This builds the categorical substrate — composition, identities.

fill … Universal

The best filler, unique up to isomorphism — a Kan extension. This does the real work: products, limits, colimits, folds.

Fold is an interpreter — and it compiles to native code

A recursive datatype is an initial algebra; a fold is the unique homomorphism out of it — a universal fill. Here an evaluator, written in Kan, compiled to a native binary:

-- expr_eval.kan
data Expr { Lit int, Add Expr Expr, Mul Expr Expr }

let e = Mul(Add(Lit(2), Lit(3)), Lit(4))     -- (2 + 3) * 4

fold eval : Expr -> int {
  Lit v   = v,
  Add a b = a + b,
  Mul a b = a * b
}

show eval(e)

$ kan build expr_eval.kan -o expr && ./expr
20

The fold lowers to a recursive C function; the binary runs the computation itself.

Status

Phase 1 complete Kan is an early research language — the core is real and runs, the type system and program-completion layers are next.

✓ One kernel — fill: composition, products, pullbacks, coproducts, folds
✓ Universal properties computed, not assumed — mediating maps, fold laws
✓ Interpreter and a native compiler (.kan → C → binary)
◦ Next: a dependent-type layer to state that a diagram commutes / a construction is universal
◦ Then: program completion by synthesis — the compiler as a categorical collaborator

Try it

# requires OCaml + dune and a C compiler
git clone https://github.com/jackmitchelwidman/kan
cd kan && dune build

kan run   examples/expr_eval.kan      # interpret
kan build examples/expr_eval.kan -o expr && ./expr   # compile & run

Design doc: README · the surface language, core calculus, and compiler are documented in /docs.