A minimal dependently typed language whose purpose is to enumerate or
sample the inhabitants of any type under a simplicity (description
length) prior. Because types include function types, dependent pairs,
propositional equalities, and user-defined datatypes, the same machinery
that enumerates Nat -> Nat cheaply performs theorem proving when the
goal is a theorem — an inhabitant of an Id type is a proof. Data
declarations are themselves terms, so the prior extends to types: the
sampler can draw a datatype and then draw inhabitants of it.
Successor to Weft. LANGUAGE.md has the full definition and
design rationale; this file covers usage, the grammar, and examples.
📖 The Warp Book — an
interactive book-length introduction, written for programmers with no
dependent-types background: the type theory built up from typed lambda
calculus, the DL prior, the enumerator and sampler, and recipes for
synthetic datasets, with live widgets over real generator output.
(Source in docs/book/; the same page works opened locally from
docs/index.html.)
No dependencies beyond Python 3.
python3 tests.py # kernel + prelude tests
python3 generate.py --goal '(-> Nat Nat)' --enumerate 4 --use ''The kernel is Martin-Löf type theory reduced to one binder family and
one data mechanism: Pi, a predicative universe hierarchy, and mu
over constructor declarations, with a single generic eliminator.
Types are terms; there is no separate type grammar.
e ::= x
| U l universe, l = 0, 1, ...; U l : U (l+1)
| (pi (x A) B) dependent function type
| (lam (x) e) unannotated; checked against a Pi
| (e1 e2) application
| (let (x e1) e2) transparent local definition: e1 is
inferred, x is bound to e1's value
| (the T e) type ascription: e checked at T,
inferable; erased at evaluation
| (mu D) a datatype — a first-class term
| (con c e ...) constructor application
| (elim l e P cases) the generic dependent eliminator;
l is the motive's target universe
A data declaration D is a name, an index telescope, and a list of
constructors, each a telescope of fields and a vector of result indices:
D ::= name [x : A, ...] { c fields -> i ... ; ... }
field ::= (x : A) ordinary field (A any type term)
| (x : rec i ...) recursive field at the given indices
Field types may depend on earlier fields; result indices are arbitrary
terms over the fields. That is the entire data mechanism. Everything
else — Unit, Empty, Bool, Nat, Sigma, Id (with J), List, Vec, Fin — is
library code in prelude.py.
Three structural properties hold by construction, with no checkers in the trusted base:
- Strict positivity — self-reference exists only as the
recfield marker, so a non-positive declaration is unwritable. - Termination — recursion exists only through
elim, whose reducts are structurally smaller; every program is total. - Consistency discipline — universes are predicative (
U l : U (l+1), no cumulativity), so theorem goals mean something and the enumerator is a genuine proof search.
generate.py --goal '...' takes a tiny s-expression surface over the
core syntax and prelude names:
goal ::= x a prelude or bound name (Nat, add, ...)
| U0 | U1 universes
| 3 integer literals elaborate to Nat
| true | false | tt
| zero | refl | nil constructor sugar
| (suc e)
| (-> A B ... R) right-nested non-dependent arrows
| (pi (x A) B) dependent function type
| (lam (x y ...) e) curried lambda
| (let (x e1) e2) transparent definition
| (con c e ...) constructor of any type in scope
| (f a b ...) application
| (data Name [((i T) ...)] (c field ... [-> idx ...]) ...)
field ::= (x T) ordinary field
| (x rec idx ...) recursive field at the given indices
In a data form the optional first group is the index telescope, and a
constructor's terms after -> are its result indices. Declarations are
terms, so they can appear anywhere in a goal — but datatypes are
generative (a datatype is its declaration's identity, so two
textually identical declarations are distinct types). If the same type
must appear twice, bind the declaration once with let and reuse the
variable. For example, length-indexed vectors of Nats:
(let (V (data VN ((n Nat))
(nil -> 0)
(cons (k Nat) (x Nat) (xs rec k) -> (suc k))))
(-> (V 1) (V 1)))
Enumeration is exhaustive in description-length order. --use ''
exposes nothing from the prelude, so everything is built from scratch;
for Nat -> ... goals the tool also tabulates the function on small
inputs:
$ python3 generate.py --goal '(-> Nat Nat)' --enumerate 4 --use ''
#000 [DL 2] (lam (x0) x0)
0 1 2 3 4 5 6 7
#001 [DL 2] (lam (x0) 0)
0 0 0 0 0 0 0 0
#002 [DL 3] (lam (x0) (suc x0))
1 2 3 4 5 6 7 8
#003 [DL 3] (lam (x0) 1)
1 1 1 1 1 1 1 1
A Sigma goal asks for a dependent pair; the least inhabitant of "a number equal to 2" is found immediately:
$ python3 generate.py --goal '(Sig Nat (lam (n) (Id Nat n 2)))' --enumerate 1 --use ''
#000 [DL 5] (pair 2 refl)
When the goal is a theorem, enumeration is proof search. Symmetry of equality is discovered as the textbook J-proof from the bare goal, with no hints:
$ python3 generate.py --goal '(pi (a Nat) (pi (b Nat) (-> (Id Nat a b) (Id Nat b a))))' \
--enumerate 1 --use ''
#000 [DL 7] (lam (x0 x1 x2) (elim x2 (lam (i3.0 x3.s) (Id Nat i3.0 x0)) (refl => refl)))
forall k. add k 0 = k requires induction; the enumerator finds a
proof (with a nested induction and a J-rewrite of the induction
hypothesis it discovered itself) in under a second:
$ python3 generate.py --goal '(pi (k Nat) (Id Nat (add k 0) k))' \
--enumerate 1 --use 'Nat' --max-size 26
#000 [DL 17] (lam (x0) (elim x0 (lam (x1.s) (Id Nat (elim x1.s ...) x1.s)) ...))
Eliminations carry real dependent motives. Motive candidates come from goal abstraction — replacing occurrences of the scrutinee and its indices in the goal by fresh motive variables — and, at larger budgets, from free-form enumeration at the motive type.
data forms are ordinary terms, so a goal can introduce its own types:
$ python3 generate.py --goal '(-> (data Color (red) (green) (blue)) Bool)' \
--enumerate 3 --use 'Bool'
#000 [DL 2] (lam (x0) true)
#001 [DL 2] (lam (x0) false)
#002 [DL 7] (lam (x0) (elim x0 (lam (x1.s) Bool) (blue => true) (green => true) (red => true)))
--samples draws from a geometric DL prior (rejection on ill-typedness
and fuel exhaustion, so the realized distribution is the MDL prior
conditioned on typeability). A universe goal samples types — fresh
data declarations included — and --inhabit K then samples K
inhabitants of each:
$ python3 generate.py --goal 'U0' --samples 3 --inhabit 2 --seed 11 --use 'Nat,Bool'
#000 [12 nodes] (-> (data T1 (c0 (a0 Nat) (a1 Nat)) (c1 (a0 Nat) (r1 rec))) Nat)
inhabitant: (lam (x0) 1)
inhabitant: (lam (x0) 0)
#001 [11 nodes] (data T2 (c0) (c1 (r0 rec) (a1 Bool)) (c2 (a0 Nat) (a1 Bool)))
inhabitant: (c2 0 true)
inhabitant: (c1 (c1 c0 true) false)
#002 [5 nodes] (data T3 (c0 (a0 Bool)) (c1))
inhabitant: c1
inhabitant: (c0 false)
--forward inverts the direction. Instead of searching for
inhabitants of a given goal, it grows a table of (term, type) pairs
by moves that only combine entries already known well-typed —
application, constructor application, binder discharge under a
hypothesis, elimination — and reads each result type off the
construction. Work is proportional to pairs produced rather than to a
search that may fail, so every Id-typed pair is a theorem arriving
with its proof attached; --theorems filters to exactly those, and
--goal (optional here) filters to one type. Pairs are priced by
joint DL (1 + |type| + |term|, the everything-pair measure) and
capped by --forward-max:
$ python3 generate.py --forward 30 --use 'Nat,add,Id' --forward-max 14 --theorems
#000 [DL 9] refl : (Id Nat 0 0)
#001 [DL 11] refl : (Id Nat 1 1)
#002 [DL 13] refl : (Id Nat (add 0 0) 0)
#003 [DL 13] refl : (Id Nat 0 (add 0 0))
#004 [DL 13] refl : (Id Nat 2 2)
--forward-samples runs a random walk on the same moves — near
rejection-free, since a move lands unless it duplicates or busts the
cap, which suits dataset generation better than enumeration's
exhaustive order. The backward modes remain the query side of the
pair: a chosen goal, searched. Forward covers only what its moves
construct (notably, redex spellings and single-use lets never arise),
and binder bodies come from hypothesis sub-tables bounded by
--forward-depth.
For observable goals (Nat -> ... -> data), --dedup keys enumeration
on the observed input/output grid instead of the program text —
enumerate data points, not programs. Boolean-valued grids render as
#/., so a Nat -> Nat -> Bool goal enumerates binary images,
simplest first. With leq exposed, image #000 is leq itself, drawn
as its own triangle:
$ python3 generate.py --goal '(-> Nat Nat Bool)' --enumerate 4 --dedup --use 'Bool,leq'
#000 [DL 1] leq
########
.#######
..######
...#####
....####
.....###
......##
.......#
#001 [DL 3] (lam (x0 x1) true)
########
########
...
#002 [DL 3] (lam (x0 x1) false)
........
........
...
#003 [DL 5] (lam (x0) (leq (suc x0)))
.#######
..######
...#####
....####
.....###
......##
.......#
........
--postulate NAME=TYPE adds an axiom — a constant with a type and no
computation rule. This turns the enumerator into a free-algebra term
generator over the postulated signature (and lets you add classical
axioms per run; note that postulated equalities break canonicity for
goals that use them):
python3 generate.py --goal '(-> F F)' --samples 5 \
--postulate 'F=U0' --postulate 'fadd=(-> F F F)' --use ''| Flag | Meaning |
|---|---|
--goal EXPR |
the type to inhabit (required); any type, including U0 |
--enumerate N |
first N inhabitants in description-length order |
--samples N |
N random inhabitants under the DL prior |
--inhabit K |
with a universe goal: also sample K inhabitants of each sampled type |
--use NAMES |
comma-separated prelude names exposed to the generator (default add,mul,Nat,Bool; '' for nothing) |
--postulate NAME=TYPE |
add an axiom (repeatable); auto-exposed |
--max-size N |
DL budget for enumeration (default 11) |
--min-budget / --max-budget / --tau |
sampling budget distribution |
--window N |
tabulation width for observable goals (default 8) |
--dedup |
deduplicate enumeration by observed grid |
--seed N |
RNG seed for sampling |
Prelude names available to --use: Unit, Empty, Bool, Nat,
Sig, Id, List, Vec, Fin (types) and exfalso, not, add,
mul, leq, fst, sym, trans, cong, append (functions).
The prior counts one node per construct, including inside data
declarations, so type definitions and terms are priced with the same
ruler. There is no literal loophole: numerals are constructor trees
(unary Nat literally costs n), and cheaper numeral representations are
datatypes the user can define. Sharing enters the prior through let —
a repeated subterm can be bound once and referenced by a one-node
variable, moving the measure from tree size toward program (DAG) size.
The generator only emits let in maximal-sharing form (inferable bound
value, used at least twice), so it never produces a spelling that plain
enumeration already covers.
kernel.py— terms, NbE evaluation, conversion, bidirectional checking, the generic eliminator, description length, printing.prelude.py— the library: finite types, Nat arithmetic, Sigma, Id (with sym/trans/cong), List, Vec (with append), Fin.generate.py— the type-directed enumerator and sampler; any type is a goal, including universes.tests.py— kernel and prelude tests.LANGUAGE.md— the language definition and design rationale (why this kernel and not Cedille/W-types/CIC, why predicativity, why generative datatypes, the deferred extensions).