Types as tests that would take forever

The design of disp's type system, explained from the bottom up. A type is a program that answers one question about two trees. Checking a claim honestly means running that program over every tree there is, which never finishes. Every checker disp ships is a shortcut, and every shortcut comes with a reason it agrees with the honest run. Every code block on this page is a test line or definition from one of three files the harness runs on every npm test: lib/tests/refuter.test.disp (the honest checker, 12 tests), lib/tests/confirmer.test.disp (the shortcuts, 182 tests) and lib/tests/types_doc.test.disp (this page's own snippets, 31 tests). The one block that is not a program is marked as such.

1. A type claim is a claim about infinitely many trees

Everything in disp is a tree: a number, a program, a type. Today a type is a program that says yes or no to one tree, and checking a value means applying the type to it. That works perfectly for data: Nat 3 runs a shape check and answers yes.

It stops working the moment the claim is about a function. succ : Nat -> Nat says: for every tree that is a Nat, succ of it is a Nat. No single run visits every Nat. The honest way to check it is to list every tree in order of size, keep the Nats, and run succ on each. disp already has that list, Trees, and IDEAS.disp already has the honest checker:

Arrow :: {Dom : Tree -> Bool, Cod : Tree -> Bool, fuel : Nat, fn : Tree} -> Bool :=> {
  let members := Trees.as_items.bounded(fuel).s_filter(Dom)
  let outputs := members.s_map({arg} => fn arg)
  outputs.s_all(Cod)
}

Run it and two things are visible at once. It can find a bad input and stop: that is a real refutation, with a witness anyone can re-run. And when it finds nothing it has not proved anything, because the budget ran out before the list did. The same claim flips with the fuel:

test Arrow Bool Bool 1 t = true      // one probe, no counterexample yet
test BoolFn t = false                // BoolFn := Arrow Bool Bool 25; the leaf is not a Bool function

So there are three answers, not two, and the third one is not a failure. Refuted means here is an input the claim fails on. Proved means the checker holds a short argument that the list would never turn up a bad input. Open means neither, within the budget, and it always says why.

The rest of this page is about what the short argument is, and what a type has to be for the argument to make sense.

2. The one question a type answers

Here is the change of view that makes everything else fall out. A type is not a program that says yes or no to one tree. It is a program that answers one question about two trees:

Do these two count as the same, as far as this type cares?

A tree belongs to a type when the type says it is the same as itself. That is the whole definition of membership; there is no second notion. For a data type the two-argument program is just the old one-argument program run on both sides, plus identity:

rel_of :: {recognize : Tree -> Bool} -> Tree -> Tree -> Bool :=> {x, y} => ((recognize x) && (recognize y)) && (x == y)
NatRel := rel_of NatR
test NatRel 2 2 = true
test NatRel 2 3 = false
test NatRel (t t) (t t) = false      // a stem is not the same as itself at Nat: it is not a Nat

member :: {rel : Tree -> Tree -> Bool, v : Tree} -> Bool :=> rel v v
test member NatRel 2 = true
test member NatRel (t t) = false

Notice the last NatRel line. The relation is deliberately not reflexive. If it only compared the trees, every tree would be the same as itself and the stem would belong to Nat. The recognizer conjunct on both arguments is what keeps non-members out, and it is what makes membership the diagonal of the relation rather than something separate. In mathematics this object has a name, a partial equivalence relation: symmetric, transitive, reflexive only on its own carrier.

For data types nothing about your code changes. You still write a recognizer, and the relation is derived from it. Where the relation carries more than the recognizer is in exactly two places, quotients and function types, and those are the next two sections.

3. Function types: sameness is judged at a type

Two functions are the same at A -> B when, fed any two inputs that A calls the same, they return outputs that B calls the same. Written out, and this is the one block on the page that is a specification rather than a program, because the "for all" ranges over an infinite list:

// not a program: the arrow relation, as a specification
f ~[A -> B] g   iff   for all a, a' with a ~[A] a':   (f a) ~[B] (g a')

Three things follow immediately, and each one used to be a separate feature.

• Function extensionality is not an axiom and not a theorem. It is this definition. Two functions that agree on every input are the same function at that type, because that is what "the same" means at that type.
• Membership is respect. A function belongs to A -> B when it is the same as itself, which unfolds to: it maps inputs A calls the same to outputs B calls the same. At a data domain that is just "maps members to members". At a quotient domain it is strictly more, as section 4 shows.
• Sameness is always judged at a type. The identity function and a function that rebuilds its argument are the same at Nat -> Nat and different at Tree -> Tree, because at Tree sameness is bit for bit and a stem is rebuilt into a fork.

id := {n} => n
shift := {n} => if (is_zero n) { zero } else { succ (nat_pred n) }
test eq_arrow NatR id shift = "Proved"        // every Nat comes back as itself
test eq_arrow TreeR id shift = refuted (t t)  // a stem does not
test id (t t) = t t
test shift (t t) = t t t

That last pair of lines is the whole reason this design can coexist with an inspecting substrate. The functions really are different trees, and at the type of trees that difference is visible. At the type of numbers it is not, and the checker says so.

4. Quotients: the same trees, a coarser question

A quotient keeps a type's members and changes what "the same" means. The simplest way to declare one is a normalizer, a function that picks a canonical representative:

rec parity :: {n : Tree} -> Tree :=> if (is_zero n) { zero } else if (is_zero (nat_pred n)) { succ zero } else { parity (nat_pred (nat_pred n)) }
ParityRel := {x, y} => ((NatR x) && (NatR y)) && (parity x == parity y)
test ParityRel 2 0 = true
test ParityRel 2 1 = false
test ParityRel (t t) (t t) = false

A quotient can only coarsen: two trees the carrier already calls the same stay the same, and some others join them. That one sentence turned out to matter more than it looks. An earlier draft let a quotient over a function type refine sameness back to bit-for-bit identity, and that reopened the transport paradox through the equality of types. So the rule is: at Quotient A nf, x and y are the same when nf x and nf y are the same at A. Quotienting by the identity normalizer gives you A back.

Now the payoff of section 3's pair-of-inputs definition. A function from the quotient belongs only if it cannot tell identified inputs apart:

is_even_step := {ie, n} => if (is_zero n) { true } else if (is_zero (nat_pred n)) { false } else { ie (nat_pred (nat_pred n)) }
id_step := {_self, n} => n
test respects_nf is_even_step parity Bool = "Proved"      // is_even : Parity -> Bool
test respects_nf id_step parity NatR = refuted (pair 0 2)  // id : Parity -> Nat cannot tell 0 from 2

Nothing here is a separate "respect obligation" bolted onto the type. It is membership, computed from the definition of sameness at an arrow whose domain is a quotient. The checker discharges it by the same induction it uses for everything else, with the recursive call assumed on the normalized sub-input; section 6 explains that machinery.

5. The honest checker, precisely: the refuter

The refuter is the type's relation run over the domain's list of related pairs instead of over a placeholder. It is IDEAS.disp's Arrow generalized from members to pairs, and it is the ground truth every shortcut is measured against.

// Related pairs of a domain, smallest first. For a data type the pairs are the diagonal;
// for a quotient they are (a, nf a). Both are bounded, so they finish spent, never exhausted.
diag_pairs :: {recognize : Tree -> Bool, fuel : Nat} -> Items (Pair Tree Tree) :=>
	Trees.as_items.bounded(fuel).s_filter(recognize).s_map({a} => pair a a)
quot_pairs :: {recognize : Tree -> Bool, nf : Tree -> Tree, fuel : Nat} -> Items (Pair Tree Tree) :=>
	Trees.as_items.bounded(fuel).s_filter(recognize).s_map({a} => pair a (nf a))

refuted :: {witness : Pair Tree Tree} -> Verdict :=> pair "Refuted" witness
open_after :: {probes : Nat} -> Verdict :=> pair "Open" probes

// refute: walk the related pairs; the first pair the function does not carry to a
// related pair is a concrete witness. The ending says the rest: an exhausted
// stream was the domain's own generator (Proved), a spent one was a budget (Open).
refute :: {pairs : Bounded (Items (Pair Tree Tree)), cod_rel : Tree -> Tree -> Bool, fn : Tree, probes : Nat} -> Verdict :=> c_fold ({recurse, step, checked} => {
	let p := step.step_draw.yielded_item
	if (step.is_finished) { if (step.finished_result.is_spent) { open_after checked } else { "Proved" } }
	else if (not step.step_draw.is_yield) { recurse step.step_rest checked }
	else if (cod_rel (fn p.fst) (fn p.snd)) { recurse step.step_rest (succ checked) }
	else { refuted p }
}) pairs probes

test refute (diag_pairs NatR 40) NatRel succ zero = open_after 3
test refute (diag_pairs NatR 40) NatRel ({n} => pair n n) zero = refuted (pair 1 1)
test refute (quot_pairs NatR parity 40) NatRel ({n} => n) zero = refuted (pair 2 0)
bool_pairs := s_from_list [pair true true, pair false false]
test refute bool_pairs BoolRel not zero = "Proved"

What it can say, exactly:

Two limits are permanent. It cannot refute divergence: an input on which the function never answers exhausts its per-run budget and is Open, not a witness. And at a function-typed domain there is no exact list of members at all, so the refuter there can only draw on functions already certified, and can never Prove by exhaustion.

The refuter also has a second job: whenever a shortcut believes it has found a counterexample symbolically, the refuter re-runs it concretely before anything is reported. A symbolic "these differ" is only ever a suggestion.

6. The shortcut: one run on a placeholder

Instead of running succ on every number, run it once on a symbol, a placeholder that means "some Nat, I will not say which". If the run finishes without ever needing the symbol's shape, it is a template: substitute any real number and you get that number's real run. One run stands for all of them.

The checker's value domain makes this concrete. A partly known value is either a known tree, a symbol, a stuck application (a neutral term nobody can run), or a partly known shape:

known :: {v : Tree} -> Val :=> pair "Known" v
sym :: {T : Code, name : Tree} -> Val :=> pair "Sym" (pair T name)
in_sym_at :: {T : Code, root : Nat, path : List Tree} -> Val :=> sym T (pair "In" (pair root path))
app_val :: {head : Val, arg : Val} -> Val :=> pair "App" (pair head arg)
half_stem :: {a : Val} -> Val :=> pair "HalfStem" a
half_fork :: {a : Val, b : Val} -> Val :=> pair "HalfFork" (pair a b)

Two details of the symbol carry most of the design. It has a name, a root and a path of destructor steps, so two occurrences of the same unknown compare equal and different unknowns do not; that is what makes pair n n refutable and what makes "f n equals g n" expressible at all. And it has a sort: a symbol that came from splitting an input is an In symbol, and only those may ever be used to justify recursion.

The evaluator interprets the substrate's rules over these values. Only one rule looks inside its argument, and that is the only place a symbol can be needed. A run therefore ends in one of three ways:

answered :: {v : Val} -> Res :=> pair "Answered" v
need :: {s : Val} -> Res :=> pair "Need" s
stuck :: Res := "Stuck"
stuck_on :: {reason : Tree} -> Res :=> pair "Stuck" reason

Need means a case split can resolve it: the run wanted to know whether the symbol is zero or a successor. Stuck means nothing can, and it carries a reason: fuel, a symbol of a type with no cases, a missing licence. This distinction is the difference between an Open the user can act on and an Open they cannot.

Splitting on demand

When the run needs a symbol's shape, the search substitutes each constructor case with fresh sub-symbols and runs each case. The cases come from the type's declaration, and the table is optional:

table :: {R : Code, child : Tree -> Val} -> Option (List Val) :=>
	if (R == NatR) { some [known t, half_fork (known t) (child "pred")] }
	else if (R == TreeR) { some [known t, half_stem (child "child"), half_fork (child "left") (child "right")] }
	else if (R == Bool) { some [known t, known (t t)] }
	else if (R == FalseR) { some [] }
	else { none }

The difference between some [] and none is not pedantry. An empty case list means a declared empty type, and a claim over an empty domain is vacuously Proved. No case list at all, which is what a function type or an undeclared recognizer has, means the search must not split and the verdict is Open with a reason. A first probe conflated the two and Proved {'{'}f{'}'} => tree_eq f id at a function-typed domain, which is precisely the transport paradox this whole design exists to refuse.

rec search_r :: {check : Val -> Res, input : Val, depth : Nat} -> Verdict :=> {
	let r := check input
	if (r == "Yes") { "Proved" }
	else if (input.is_known) { if (r == "No") { refuted input.snd } else { open_on (explain r) } }
	else if (is_zero depth) { open_on "split depth exhausted" }
	else {
		let target := split_target r input
		if (target == "None") { open_on (explain r) }
		else {
			let alts := table target.sym_type ({step} => in_sym_at target.sym_type target.sym_root (cons step target.sym_path))
			combine (alts.snd.map({alt} => search_r check (subst target alt input) (nat_pred depth)))
		}
	}
}

Read it top down. A Yes on a symbolic input covers every instance of its symbols. A No on a known input is its own witness. Otherwise split the symbol the run needed, and combine: any refuted case refutes, all Proved cases prove, anything else is Open with the first reason.

Recursion: the call may assume the claim, on a smaller piece

When the program calls itself, the symbolic run reaches a call it cannot unfold forever. The checker lets that call answer "whatever the claim promises", but only when the argument is a strict sub-symbol of the input it started from. Recursion on a strictly smaller piece must bottom out, and that is the only termination argument the checker knows.

apply_ih_at :: {Dom : Code, Cod : Code, root : List Tree, partner : Val -> Val, x : Val} -> Res :=> {
	let license := {c} =>
		if (((c.is_in_sym) && (c.sym_type == Dom)) && ((c.sym_root == 0) && (is_strict_ext c.sym_path root))) { answered (rec_sym Cod c.sym_path) }
		else { stuck }
	let direct := license (canon x)
	if (direct.is_answered) { direct }
	else {
		let peeled := match_val (partner (var_sym "a")) x []
		if ((peeled.is_answered) && (not peeled.answer.is_nil)) { license (canon peeled.answer.head.snd) } else { stuck }
	}
}

Four checks in that licence, each closing a real hole: the argument must be an input-derived symbol, of the domain's type, from the root being inducted on, and strictly below it in the destructor order. Miss the last one and a step function whose recursion never descends is Proved; miss the first and a symbol minted from a function's output counts as smaller than the input. Both were live bugs in earlier probes.

dbl_step := {dbl2, n} => if (is_zero n) { zero } else { succ (succ (dbl2 (nat_pred n))) }
bad_step := {bad2, n} => if (is_zero n) { zero } else { succ (bad2 n) }   // fix bad_step 1 loops forever
test check_by_structure succ = "Proved"
test check_by_structure ({n} => pair n n) = refuted 1
test check_by_induction dbl_step = "Proved"
test check_by_induction bad_step = "Open"
test check_by_induction two_base_step = "Proved"   // course-of-values: the licence folds succ (sub-symbol) back to the symbol

So the short argument behind a Proved is always one of three: the run never looked at the symbol; the run looked, the cases were split, and every case closed; the program recursed, and every recursive call was on a strictly smaller input-derived piece. The certificate names which.

Which part is the specification

The symbolic evaluator in confirmer.test.disp is the reference: a readable disp program, non-performant on purpose, whose behaviour is the meaning of every verdict on this page. It is not a second evaluator for its own sake. The intended fast path is the same one the project already uses for everything else: a native mode of the host evaluator that treats a symbol as an opaque node it refuses to open, validated against the reference by differential testing, or a specialized rewrite of the reference in an .opt.disp overlay. The reference runs a concrete dbl 3 about a thousand times slower than the native evaluator, so the fast path is what turns this design into a tool; the reference is what says the tool is right.

The hook is on the rule, not on the text

A fair test of the model: a function whose text contains no inspection, but which builds a case-analysis at runtime and applies it to its input. If the checker's guard were on the syntax, this would slip through.

runtime_triage := {n} => (t (t zero succ) id) n
runtime_id := {n} => (t (t zero ({_} => zero)) ({_l, r} => succ r)) n
test runtime_triage 1 = t t
test run runtime_triage (in_sym NatR []) = need (in_sym NatR [])
test check_by_structure runtime_triage = refuted 1
test check_by_structure runtime_id = "Proved"

The run reports that it needed the symbol's shape, because the built triage is applied to the symbol and the triage rule is where the evaluator looks. The first function then turns out not to be a member at all: it sends the number one to the stem t t, and the search finds that by splitting and re-running the case concretely. The second, a Nat identity written the same way, is Proved after the split. Under the v1 confirmer in CHECK.disp, which cannot split, both come back Open: never Proved, never a false verdict.

7. Streams: the same trick facing the other way

A stream is a stepper and a state; a step finishes with an ending, or runs on with an item (a yield) or without one (a skip). Two streams are the same when every item and every step agree, forever. The honest check is prefix comparison and never ends; the shortcut is one symbolic step. Run each stepper on a symbolic state, compare the items, and check that the next states are again a pair the relation covers. The assumption "these states are related" may only be used on the next states, after both sides have taken a step; using it on the current states would prove any two streams equal.

naturals := nats.as_items
nats_add := s_new ({n} => running (emit (yield n) (add 1 n))) zero
by_two := s_new ({n} => running (emit (yield n) (succ (succ n)))) zero
nats_pair := s_new ({p} => running (emit (yield p.fst) (pair (succ p.fst) t))) (pair zero t)
pair_states := {x} => pair x (half_fork x (known t))
test stream_eq NatR same_states naturals nats_add = "Proved"
test stream_eq NatR same_states naturals by_two = refuted (pair [known 0, known 1, known 2, known 3] [known 0, known 2, known 4, known 6])
test stream_eq NatR pair_states naturals nats_pair = "Proved"

The third line relates two streams with different state spaces through a user-supplied relation between states; the coinductive hypothesis is discharged by matching the next states against that pattern.

Two notions of the same, and why the finer one is the type's

What section 7 checks is strong bisimulation: a skip is a step, and a skip must meet a skip. A stream that skips before every item is therefore not the same as one that does not (slow versus naturals is refuted in the probe). That is deliberate. The library's bounded spends budget on skips, so under any looser sameness it would carry equal streams to unequal prefixes and fail to belong to its own type.

The optimizer still needs a sameness to appeal to when it removes a skip, and it gets one without a new mechanism: a quotient. The weak stream type is Items V quotiented by the skip-removal normalizer, exactly as Parity was Nat quotiented by parity. A function belongs to an arrow out of the weak type only if it cannot count skips, which bounded cannot claim and a consumer that only reads items can. The normalizer is partial on a stream that skips forever, so forming the quotient carries a productivity obligation, a certificate that skips are finitely many between items, parallel to the termination obligation on functions. Skip removal is then licensed as a rewrite at the weak type and scored as a measured improvement, and a context that counts skips is simply not a member of the weak arrow, so the rewrite does not fire there.

8. Tree is the type of code

disp's substrate lets any program take any tree apart, including a function. That is the reflection the whole project is built on, and it is also why no untyped notion of "same behaviour" survives: a program that compares trees bit for bit tells any two different trees apart. The design does not fight this. It gives the ability a type.

At Tree sameness is bit for bit and every tree belongs, so inspecting functions are perfectly good members there:

test check_arrow TreeR Bool is_leaf = "Proved"
test check_arrow TreeR Bool ({x} => tree_eq x t) = "Proved"

At Nat -> Nat sameness is extensional, so a symbol of that type is a value the checker will not let anyone look inside, and will not let anyone embed at a position whose sameness is finer than its own. That second half is the subtle one. It is not enough to refuse the function that compares f with the identity. Wrapping f in a stem, pairing it with zero, or returning it unchanged at type Tree would let bit-for-bit sameness leak back in through the codomain, and an earlier probe accepted all three. The rule that closes every spelling: a value carrying a symbol of a coarser type is never "the same as itself" at a finer position. Where a certified pair of same-but-different functions is stored, the checker grounds the symbol on it and refutes concretely.

NatFn := ArrowC NatR NatR
sniff := {f} => tree_eq f id
wrap := {f} => t f
test check_arrow NatFn Bool sniff = refuted (pair id shift)
test check_arrow NatFn TreeR wrap = refuted (pair id shift)
test check_arrow NatFn NatR ({f} => f 0) = "Proved"           // applying a function symbol is fine
test check_arrow NatFn TreeR ({f} => f id) = refuted (pair id shift)   // applying it outside its domain is not

This is why function extensionality at Nat -> Nat is consistent with bit-for-bit comparison at Tree. The two never meet, because there is no member of (Nat -> Nat) -> Tree other than the constant functions and the ones that go through an application first. The old kernel tried to police this with an unforgeable hypothesis token and a provenance ledger, and it leaked through a reader that could tell a hypothesis from a value. Here there is nothing to leak: a symbol only ever exists inside the checker's own value domain, and every piece of the candidate program the evaluator touches is re-wrapped as a known tree.

9. The contract: every shortcut agrees with the honest run

Put together, the checkers form a ladder. Each rung is a procedure plus the claim that its verdict never disagrees with the refuter, and a note on how far that claim is proved.

Why one run stands for all

Call a value partly known when some of its leaves are symbols, and call an instantiation the tree you get by substituting a member for every symbol. The evaluator fires the substrate's rules on partly known values, and each rule examines a fixed part of its operands: applying a leaf or a stem reads nothing; applying a fork reads the shape of its left branch to choose between the constant rule, the sharing rule, and the case rule; and only the case rule reads the shape of the argument. Whenever the part a rule needs is known, the same rule fires with the same result for every instantiation, because substitution reaches under a known node without changing its shape; that is one line per rule. Whenever the part is a symbol, nothing fires: the evaluator answers Need or Stuck. Two more one-line cases: the case-analysis whose three arms are all leaves rebuilds any argument, so it may pass a symbol through, and a fully known shape collapses back into the tree it denotes. By induction on the sequence of firings, if the symbolic run answers a value, then for every instantiation the real run reaches that value's instantiation. The real run may take more steps, and it is at least as willing to finish, since the host discards an unused argument the symbolic evaluator would have evaluated.

Two things sit outside this sketch. A symbol or a neutral term in function position makes a neutral term rather than firing; instantiating one means applying the instantiated head, and the lemma extends exactly when that application terminates, which is what the head's stored membership certifies. And the induction licence is a separate argument, ordinary strong induction on the size of the input piece, whose one genuinely open claim is that a single symbol per input establishes respect when the domain's sameness is coarser than identity. That is the fundamental lemma of logical relations for the judge, and it is tested rather than proved.

The contract is not just stated; it runs. Every probe file ends with the honest checker running against its own verdicts:

agrees :: {verdict : Verdict, enumerated : Bool} -> Bool :=>
	if (verdict == "Proved") { enumerated } else if (verdict == "Open") { true } else { not enumerated }
test agrees (check_by_structure succ) (Arrow NatR NatR 40 succ) = true
sweep := candidates.map({fn} => pair (check_by_structure fn) (Arrow NatR NatR 40 fn))
test sweep.all({p} => agrees p.fst p.snd) = true      // 40 candidate trees: 8 Proved, 32 Refuted, 0 Open

Two rules keep the verdicts honest at the edges. A symbolic "No" is never reported as Refuted until the offending case has been instantiated by its smallest members and re-run for real, so an uninhabited case can never refute. And a recognizer that loops on some input makes membership Open there, never a verdict either way:

rec LoopR :: {v : Tree} -> Bool :=> if (is_zero v) { true } else { LoopR v }
test check_arrow LoopR NatR id = "Open"

10. What the optimizer gets

The optimizer's job is to replace a program by a different, faster one that is the same at the type the specification names. Under this design that is one certificate of section 6's equality rung, plus one membership check: the surrounding context must belong to the arrow from the type where the two programs are the same to the type of the whole. A context that inspects its hole does not belong to that arrow, so the rewrite is refused there, and a context that only applies its hole does.

Every verdict is stored as replayable data: which symbol, which cases, which recursive calls were licensed, and for a refutation the concrete pair. Replay never searches; it re-runs the named steps and checks the licences. Refuted witnesses are kept as a regression battery every later candidate must pass. Cost is judged by measured native steps, not by the symbolic run's step count, because the two are not proportional; the symbolic count only gives the asymptotic direction. Correctness gates, cost ranks. The stream case shows the two channels apart: removing a skip is not an equality at Items V, it is an equality at the weak quotient and an improvement at the strong type, and the rewrite fires only inside contexts that belong to the arrow out of the weak type.

11. What stays Open on purpose, and how to read an Open

Membership at Nat -> Nat is undecidable, so some true claims stay Open forever. The design does not hide this; it names the budget or the rule that stopped the run.

Two things are conjectures rather than theorems, stated as such and tested: that one symbol per binder suffices, meaning membership judged at the codomain implies respect for the domain's relation; and that the enumeration lists every tree exactly once. The run lemma of section 9 is a theorem, and it is property-tested anyway: instantiate the symbols of a symbolic answer at random and compare with the real run. Each conjecture has a one-line falsifier of the same shape.

Two ceilings are stated rather than hidden. Equality of types is structural on their codes: two types with the same members but different declarations are different types, and moving a program between representations is a pair of certified translations, never a type equation. And laws quantified over all types are neither Proved nor Refuted, because a function that cases on its type argument is a legitimate member of the polymorphic type, so the usual free theorems do not hold outside a sub-universe of certified non-inspecting code.

12. Glossary

Companion files, all run by npm test: lib/tests/refuter.test.disp (the honest checker, 12 tests), lib/tests/confirmer.test.disp (the shortcuts, 182 tests), lib/tests/types_doc.test.disp (this page's snippets, 31 tests). CHECK.disp and CHECK.html are the v1 confirmer this design grew out of.