Muro

A spec never becomes evidence. Evidence never becomes a run.

An explicit affine dependent type theory. Elixir parses, checks, and emits .muro. Only run terms become running code. Users do not need Agda.

The language book is manual/. That is what muro-lang.dev will render. It is not ExDoc. Elixir API docs, when added, stay on @moduledoc / mix docs. Agda in agda/Muro/ is a third layer: the rules of the calculus, not a certificate that a .muro file is correct.

Install

muro on Hex is published by the murolang organization. Releases are listed in CHANGELOG.md.

def deps do
  [
    {:muro, "~> 0.2"}
  ]
end

A clone is for changing the kernel. A .muro file is checked with mix muro.check from a project that depends on the package.

One-shot (humans and agents)

Two jobs. Do not mix them.

Agents: read manual/for-agents.md. Copy syntax from examples/, not from memory.

Skeleton:

-- comments start with --
def plus : run Π (n : Nat) → Π (m : Nat) → Nat :=
  λ (n : Nat) → λ (m : Nat) →
    match n motive (λ _ → Nat)
      | 0 => m
      | suc np => suc(plus np m)

mix muro.check examples/your_file.muro

A definition is in the book the moment Parser.parse/1 returns it. The checker sees the whole book (forward references are allowed). Emit keeps only run.

Manual

Index: manual/index.md. Machine-readable list: manual/manifest.yml.

Build

mise install
mix deps.get
mix test
mix muro.check
mix muro.check examples/half_ok.muro

Agda 2.8+ and standard library 2.3 (optional unless you change the kernel):

git clone --depth 1 --branch v2.3 https://github.com/agda/agda-stdlib.git vendor/agda-stdlib
make agda

Muro.Lexer.tokenize/1 is the highlighter. It walks a fragment with the parser's lexical rules and returns {kind, start, stop} byte spans. A snippet that Parser.parse/1 rejects still yields spans, and joining the slices gives the source back. Muro.MakeupLexer maps those spans onto Makeup tags (language "muro", extension .muro) and is registered when the application starts. HTML and colors stay with the caller.

Muro.Check.check_sig/1 returns :ok on the book. CI runs the Elixir job and make agda on every push and pull request. make agda checks the theorem modules (Muro.Judgement, Muro.Wall, Muro.Consistency) under --safe; conversion in ⊢ is a relation, Muro.Consistency proves that no closed normal evidence term has type Empty, Empty-evid itself is not proved, and data / ν / Tensor are still outside ⊢. Type is one impredicative sort; kinds (Π (x : A) → Type) are well-formed but are not terms of type Type, in Agda and in Elixir alike.

Names