2026-06-06 — Dan Billings

Documentation that compiles: Free Monads and mdoc as provable specs

Dan Billings — 2026-06-06

Documentation is usually a lie. It describes what the code used to do, or what the author hoped it would do. The moment you copy-paste an example into a REPL, it breaks.

There is a better way. With Scala 3, mdoc, and a Free Monad architecture, documentation can be a living, compiled specification. If the docs don't compile, the build fails.

The mdoc guarantee

mdoc is an sbt plugin that treats Markdown files as Scala code. When you run sbt mdoc, it compiles every code block, executes it, and bakes the output (or compile errors) directly into the generated HTML.

This creates a hard constraint: stale documentation is impossible. If you rename an enum, change a type signature, or tighten an Iron refinement, mdoc will fail. You are forced to update the docs before you can ship the code.

Free Monads: the perfect partner for executable docs

Free Monads separate the definition of a Domain Specific Language (DSL) from its execution. In ansible-scala, we define a typed InfraProgram DSL using Scala 3 enums and refined types.

def setupWebServer: InfraProgram[Unit] =
  install(Packages.Apt.Nginx) >>
  ensureDir("/var/www/html", "0755") >>
  writeContent("<h1>Hello</h1>", "/var/www/html/index.html")

Because this is a Free Monad, it doesn't actually do anything when evaluated. It just builds an abstract syntax tree (AST). The actual work is deferred to an interpreter.

Interpreters as documentation engines

This separation is where executable documentation shines. We don't need to deploy to real infrastructure to prove our docs work. We can compile the documentation against a ConsoleInterpreter or YamlInterpreter that prints the generated commands or YAML to stdout.

// The docs compile this against a dummy interpreter
val result = setupWebServer.foldMap(yamlInterpreter)
println(result) 
// -> - name: Install nginx
//    apt: { name: nginx, state: present }
//    ...

The reader sees the exact YAML that would be generated. The compiler proves the DSL is well-formed. And because it's compiled code, the type system enforces that Nginx is a valid package and /var/www/html is a valid path.

Proving constraints with mdoc:fail

The real power comes when you document what shouldn't work. mdoc has a :fail directive that expects a compile error and captures it in the output.

val invalidPort: Port = 70000

In the generated docs, this renders as:

Error: Cannot prove GreaterEqual[1](70000)

The reader doesn't just read that "port numbers are validated." They see the compiler rejecting an invalid port. It's proof of concept built into the text.

The specification loop

When you combine these three elements, you get a self-validating specification:

  1. DSL Definition: You define your domain (packages, files, services) using pure typed models. No raw strings, no integers — only PackageRef, FilePath, and Port.
  2. Executable Docs: You write mdoc examples that import the DSL and construct programs. These compile against a TestInterpreter.
  3. Interpreter Flexibility: You swap interpreters to target different platforms. The macInterpreter generates brew commands, the ubuntuInterpreter generates apt commands, but the documentation remains the same.

If the docs compile, the specification is sound. If the docs run, the DSL is usable. And because the docs are compiled Scala, the compiler catches every edge case before it ever reaches production.

See also: Type-Safe Home Cluster — the architecture behind this DSL.

Documentation stops being a chore and becomes a first-class citizen of your architecture. It's the Jupyter notebook for systems programming: interactive, executable, and mathematically provable.

← All writings · Home