The wall

In brief: every definition is tagged spec, evidence, or run. The checker will not let a spec become evidence, or evidence become a run. Affinity is taxed the same on theorems as on programs. Emit keeps only run.

This is the language, not a style guide.

Three modes

m ∈ {run, spec, evid}. The surface word is evidence. Agda writes evid. Elixir stores :evidence.

run internal is Elixir visibility only. Agda Def stores the mode, not def vs defp.

See examples/internal_ok.muro: step is run internal (emits defp); inc is run (emits def) and calls step.

Promotion is forbidden

spec      ↛  evidence
evidence  ↛  run
spec      ↛  run

Using a definition of mode from while checking in mode to:

A program may mention other programs, and may be mentioned from evidence or spec (for example a type that talks about half). A theorem may be used in evidence or mentioned from spec. A spec may only be used in spec.

There is no rule that takes a spec derivation and returns an evidence derivation. The formers that live only in spec (Nat as a type, Π, identity types, …) have no constructor in a run or evidence derivation. That is proved for the core fragment in agda/Muro/Wall.agda.

Identity has one introduction, refl, and it has no run derivation (no-run-rfl in Muro.Wall). Run code cannot build a proof, hand one to a function, or return one, so no proof reaches emitted code. Pass a proof to a run function as an erased argument, (- e : {a ≡ b : A}): it is checked in spec and not emitted. An absurd branch (matchEmpty) may still have an identity type, since it never runs.

A run definition has a run type, used or not: the codomains of its Π, each side of a product, and the body of a ν are data, Nat, Unit, Empty, machine numbers, or names that reduce to one of those. def e : run {0 ≡ 0 : Nat} is refused at its type, e type: no promotion: a run definition has a spec type. Π domains are not read there; a run variable of a spec type is refused where it is used.

What is checked in spec

Even inside a run or evidence term, some positions are spec:

• Erased Π-arguments ((- x : A)).
• The two sides of an identity {a ≡ b : A}, and the sort A.

Arguments at a call site of an evidence definition are not spec, but their uses do not count. Instantiating a theorem does not consume affine resources: inside an evidence term, the argument of an application whose head is an evidence definition is checked in evidence like any other argument, and its uses are then discarded. Before 0.3.0 the argument was checked in spec, so a spec variable could be handed to a theorem from evidence; it cannot now.

Local affine binders in an evidence λ still fail if you use them twice. Evidence pays the same affinity tax as run. It is not a free ride.

Why the wall is the language

A type is not a proof. A proof is not a program.

If a spec could become evidence, you could treat IsEven as if it were a theorem. If evidence could become run, you could compile half_ok and run the proof. Muro refuses both. Emit’s fallback for a non-run fragment is raise "erased term".

The slogan is operational:

• Spec is forgotten at emit.
• Evidence is checked, then forgotten at emit.
• Run is checked, then becomes Elixir.

Next: Terms.