Qi

Qi is a functional programming language created by Mark Tarver and first released in April 2005. Built on top of Common Lisp, Qi set out to be a rationalization and modernization of Lisp: it kept Lisp’s macro power and symbolic flexibility while layering on the features programmers expected from contemporary functional languages — pattern matching, currying, partial application, and guards — together with an unusually powerful optional static type system expressed in the notation of sequent calculus. The result was a language that looked like Lisp but reasoned like a proof assistant.

History and Origins

Qi was the work of Mark Tarver, a logician and computer scientist who wanted to bring the rigor of formal logic to practical Lisp programming. He framed the project as part of a broader effort to modernize Lisp for the 21st century, and the first public version — Qi 6.1 — appeared in April 2005 under the GNU GPL.

From the start Qi was implemented in Common Lisp and ran on common implementations of it, so adopting Qi did not mean abandoning the mature Lisp ecosystem. Instead, Qi compiled its own constructs down through Lisp, giving programmers a higher-level, more strongly typed surface over a familiar runtime.

In November 2008 Tarver reimplemented the language and released Qi II, a substantially revised system with type-secure lazy evaluation on demand, a compiler that came in multiple “speeds” depending on how aggressively it used type information, and more programmable syntax. Where the original Qi had been GPL-licensed, Qi II moved to a pair of proprietary licenses — one for personal and educational use and another for building closed-source software. The last widely referenced release, Qi II 1.07, arrived in July 2009.

Design Philosophy

Qi’s guiding idea was that a modern Lisp should not have to choose between flexibility and formal rigor. Its design rests on a few principles:

• Logic as a first-class tool. Types in Qi are not bolted on; they are defined using sequent-calculus rules, letting the programmer describe a type theory the way a logician would describe an inference system.
• Optional, not mandatory, typing. Type checking can be switched on for safety or left off for the freewheeling style of ordinary Lisp, so the language scales from quick scripting to heavily verified code.
• Stay on Lisp. Rather than building a new runtime, Qi compiles onto Common Lisp, inheriting its performance, libraries, and decades of engineering.
• Bring functional conveniences to Lisp. Pattern matching, currying, partial application, and guards make idiomatic functional code far more concise than plain Lisp allows.

Key Features

Qi’s most distinctive contribution is its type system. Most statically typed functional languages — ML, Haskell — describe types with algebraic notation. Qi instead uses sequent-calculus notation, the formalism of proof theory, to define types and the rules that relate them. This makes the type system remarkably expressive: programmers can define their own type theories, and the checker is powerful enough that, by design, its type language is Turing-complete. That power is a double-edged sword — type checking is extraordinarily flexible but is not guaranteed to terminate for arbitrary user-defined systems.

Other notable features include:

• Pattern matching, currying, partial application, and guards for clear, compositional functional code.
• An optional static type checker that can be enabled per program, recognizing primitives such as symbols, variables, strings, booleans, numbers, and characters.
• Embedded Prolog (Qi Prolog). Qi compiled through an abstract machine to an extended Prolog with embedded function calls, integrating logic programming directly into the language.
• Qi YACC, a built-in compiler-compiler for writing parsers within Qi.
• Programmable syntax, leaning on Lisp’s macro heritage to let users extend the language’s surface forms.

A small flavor of Qi, showing a typed, pattern-matched definition:

(define factorial
  {number --> number}
  0 -> 1
  N -> (* N (factorial (- N 1))))

Here the line {number --> number} is the type signature, and the two clauses pattern-match on the argument — the 0 base case and the general N case.

Evolution

Qi evolved quickly across its short life. The original 6.1 release of 2005 established the core language; later versions added compiler optimizations for pattern matching. The Qi II reimplementation of 2008 was the major turning point, introducing lazy evaluation on demand and a tiered compiler that exploited type data, along with the shift to proprietary licensing. Adjacent tools such as Qi/Tk (2009) added type-secure GUI programming via Tcl/Tk.

The most important evolutionary step, however, pointed beyond Qi itself. Presenting his work around 2008–2009, Tarver observed that Qi could be rebuilt on a much smaller instruction set than the body of Common Lisp functions then used to implement it. Pursuing that insight led him to design a new, cleaner, and far more portable language.

Current Relevance

Qi is no longer actively developed. Its lineage continues through Shen, which Tarver released in September 2011 as Qi’s direct successor. Shen was built from the ground up on a tiny set of primitive instructions (the Kλ / “Kl” kernel) so that it could run on many host platforms — Common Lisp, and later targets such as JavaScript, Clojure, Python, and others — rather than being tied to Common Lisp alone. Shen carried forward Qi’s defining ideas: the sequent-calculus type system, pattern matching, and embedded Prolog. For most purposes, anyone interested in Qi today is pointed toward Shen, which preserves much of Qi’s character while being more portable and openly licensed.

That said, Qi remains historically interesting in its own right. It demonstrated that a small, single-author project could meaningfully extend Lisp with a type system more adventurous than those of mainstream functional languages.

Why It Matters

Qi mattered because it asked an unusual question: what if a language’s type system were as programmable as its code? By grounding typing in sequent calculus, Tarver gave Qi a type checker expressive enough to encode custom logics — a level of power rarely seen outside dedicated proof assistants — while keeping the whole thing running on ordinary Common Lisp. Combined with pattern matching, currying, guards, and embedded Prolog, Qi showed how much modern functional and logical machinery could be layered onto Lisp without leaving it. Its ideas did not fade with the language; they live on in Shen, making Qi an important and influential waypoint in the long evolution of the Lisp family.