spec
Types, families, signatures. Uses are forgotten. Recursion does not have to descend. Nothing here is compiled.
emit · omit
explicit affine dependent type theory
A spec never becomes evidence. Evidence never becomes a run.
Named after the wall between spec, evidence, and run. Types, erased arguments, equations, and paradoxes never execute. Only run terms become running code.
Scroll the wallmuro, n. · wall
The wall is the language.
Muro is Spanish for wall. The theory is named after the one that stands between a specification, a proof, and a program. Promotion is forbidden. Elixir parses, checks, and emits. Agda specifies the judgments. If they disagree, Agda wins.
three modes
Nothing crosses the wall.
Every definition is tagged. 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.
evidence
Theorems. Same affinity tax as run. Same descent. Still not a program. Instantiating a theorem does not consume affine resources.
emit · omit
run
Programs. Affine, descending, executable. run internal
is the same judgment, emitted as defp.
emit · Elixir def
Using a definition of mode from, while checking in mode to
| run | evidence | spec | |
|---|---|---|---|
| run | yes | yes | yes |
| evidence | no | yes | yes |
| spec | no | no | yes |
the language
Bidirectional. Explicit. No holes.
One sort, Type. Not Type : Type. No metavariables, no implicits,
no unification, no tactics. Motives are written. Binders are typed.
A run or evidence variable is used at most once, unless + on Data.
Affine by default
Π (n : Nat)
is at most one use. +
reuses only if the type WHNFs to Data.
Erased binders cannot run.
Descent
Run and evidence recursion must go through match and call on a structurally smaller variable. Spec does not check descent.
Identity
{a ≡ b : A} with refl when both sides convert. rewrite takes
an explicit motive. Equations never execute.
nu and Either
Stream is a greatest fixed point. Only a run Stream becomes an Elixir Stream. Either is built-in disjoint union. Dec is a spec, not LEM.
If Agda and Elixir disagree, Agda wins.
the example
half of eight is four.
Evenness as a spec, half as a run, the proof as evidence. Evidence is an ordinary term — match, refl, rewrite — and it is not emitted.
4 half of eight
-- a spec never becomes evidence
-- evidence never becomes a run
def IsEven : spec Π (n : Nat) → Type := …
def half : run Π (n : Nat) → Nat := …
def half_ok : evidence
Π (n : Nat) → Π (e : IsEven n) →
{plus (half n) (half n) ≡ n : Nat} := …two languages
Checker and spec.
The Elixir kernel is a mirror of the Agda decision procedure. Three representations on purpose: named FOAS at the surface, de Bruijn in the checker, PHOAS in the examples.
Elixir
Parses .muro, checks the book, emits run terms as ordinary
Elixir. Muro.Check.check_sig/1 returns :ok.
Fallback for a non-run fragment is raise "erased term".
Agda
Source of truth for ⊢. Syntax, substitution, and the checker live
in agda/Muro. Extend Agda first until the example decides,
then add the matching Elixir clause.
A spec never becomes evidence. Evidence never becomes a run.
one-shot
Write against the wall.
Write a .muro program. Check it. Do not change Agda or the Elixir
kernel unless you are changing the type theory.
$ git clone https://github.com/doctorcorral/muro.git $ cd muro $ mix test $ mix muro.check examples/half_ok.muro