Write the rules.
Explore every outcome.

Language · 1

Atoms, particles and coherences

Photonic has one kind of data: occurrences of atoms, grouped into particles, living in coherences.

An atom is any run of characters other than ( ) [ ] . , and whitespace. True, 0, ->, $x and 人 are atoms. Atoms mean nothing by themselves; rules give them meaning.

A dot joins occurrences into a particle. A particle is unordered and counts repeats: A.B and B.A are the same particle, and A.A holds two occurrences of A.

A comma separates coherences, the independent places where particles live. A.B, C is two coherences. () is one empty coherence; an empty program has none.

A configuration is everything that exists at one moment: its coherences and the rules that are live.

Next: Rules consume and produce

Language · 2

Rules consume and produce

A rule names what it consumes in brackets, then what it produces.

A.X
[A] B

Matching is open: a pattern needs only its own occurrences, and the rest of the coherence passes to the output.

To consume the whole particle, name all of it:

A.X
[A.X] B

An event consumes one match. Two occurrences of A take two events:

A.A
[A] B

Several inputs, several outputs

Commas inside the brackets select several coherences; commas after them produce several. Every output receives the remainder of every consumed coherence.

A.X, B.Y
[A, B] (C, D)
[C, D] E

Empty inputs and outputs

A.X, B.Y
[A],
[B] ()

The lens shows how each form reads. Compare [A], [B] C with [A] [B] C:

Next: Occurrences have identity

Language · 3

Occurrences have identity

Two occurrences can carry the same atom and still be different occurrences. Photonic tracks which is which.

When one event produces several outputs, they all receive the same remainder: the same occurrence appears in each. When those coherences join again, a shared occurrence counts once.

Seed.X
[Seed] A((), ())
[A, A] ()

Occurrences written separately are independent, and they add up:

A(X, X)
[A, A] ()

Adding up is arithmetic. A natural number can be a coherence of independent Units, and addition is a join:

Add.Unit.Unit,
Add.Unit.Unit.Unit
[Add, Add] ()

Every explicit output is a new occurrence. Two branches that each produce Y produce two Ys, even from one ancestor.

Identities are anonymous. Configurations that differ only in how occurrences are named are the same configuration, and the runtime stores it once.

Next: Every future

Language · 4

Every future

When several events are possible, the runtime explores all of them. The result is a graph: configurations are nodes, events are arrows.

An event is one rule applied to one match. Different rules, and different matches of one rule, give different events.

A
[A] B
[A] C
[B, C] D

A
[A] B, C
[B, C] D

Only occurrences that coexist in one configuration can be matched together.

Cycles and endless programs

A
[A] B
[B] A

[] A

Exploration runs within budgets on configurations, coherences, occurrences, scopes, records and work. A search stopped by a budget can resume with a larger one. Until it finishes, whatever it has not found is unknown.

Next: Scopes

Language · 5

Scopes

An output group that contains rules opens a scope: a local place with its own rules.

Brew.Tea
[Brew] (Kettle [Kettle.Tea] Cup)

• A scope's own rules send their output to the enclosing scope. That is how a scope returns.
• Rules of enclosing scopes also apply inside a scope, and their output stays inside.
• A rule joins coherences only within one scope.
• A scope group starts with at most one coherence: (Kettle [Kettle.Tea] Cup) is valid, (A, B [A] C) is not.
• The scope holds what the entering rule matched exactly; a state view shows it after holds.

A scope works like a function body: it receives the remainder, runs its local rules and returns through them.

Next: Inference

Language · 6

Inference

A rule can apply to what a configuration can become. The event happens at the original configuration.

A
[A] B.C
[B] D

Abstraction through rules

Inference makes abstraction ordinary. Here two ordinary rules make True and False count as Boolean:

Not.True
[True] Boolean
[False] Boolean
[Not.Boolean] (
    [True] False,
    [False] True,
)

Inference splits a match in two. Occurrences matched as written, here Not, are exact. Occurrences reached through evidence, here True seen as Boolean, are the witness. A literal output consumes both. A scope consumes the exact part and receives the witness. Hover an event to outline what it consumes: solid for exact, dashed for witness.

And.True.False.Extra
[True] Boolean,
[False] Boolean,
[And.Boolean.Boolean] (
    [True.True] True,
    [True.False] False,
    [False.False] False,
)

Next: Rules are values

Language · 7

Rules are values

A rule in brackets inside a particle is a value. It can be produced, carried, matched, consumed and replaced.

Seed.A
[Seed] [A] B

([A] B).A
[[A] B] [A] C

Loaded rules are live occurrences too, and a rule can consume one:

[A] B
[([A] B)] C

• Executing a rule reads it; matching it consumes it.
• A rule value remembers the scope that made it. Equal code made in different scopes gives different values.
• There are no variables, wildcards or quotation. Abstraction comes from rules, as in inference.

Next: Fields and shorthand

Language · 8

Fields and shorthand

Particles are unordered, so a role needs its value attached. A one-rule value does that.

Digit.0.Carry.1 cannot say which number is the digit. ([Digit] 0).([Carry] 1) can: each role and its value form one rule value, a field.

Fields are live rules. Beside a bare P, the field ([P] True) fires and turns it into True. The theorems use this on purpose, and the library never uses a role name as a plain atom.

P.([P] True)

Shared prefixes

Parentheses in a particle distribute: A(B, C) means A.B, A.C, and (A, B).(C, D) means four coherences. They build nothing: Box(A.B) is exactly Box.A.B. In a rule's output, adjacent groups are separate outputs: [A] (B)(C) produces two coherences.

Next: Prism

Verification · 9

Prism

Prism answers one question: can this exact configuration be reached?

A target is a complete configuration: every coherence, every occurrence and every live rule. A.X [A] B reaches B.X [A] B, where the rule is still live, but never plain B.X.

A.X
[A] B

[] A

Direct paths

Large programs are checked along a direct path: one execution, followed until it reaches the target, returns to a configuration it has seen, or no rule applies. A path can prove a target reachable; it can never prove one unreachable. Programs that build linked data, and most theorems, are checked along paths.

Next: The workbench

Verification · 10

The workbench

Two views of one program. The state graph shows every configuration; the hypergraph shows how one execution moves through its coherences.

In the hypergraph each coherence is a lane that runs from the event that produced it to the event that consumes it. An event is a hyperedge: it consumes whole coherences and produces new ones, and every other lane passes it untouched. Lanes that never meet evolve independently. Select a configuration in the state graph to draw the execution that reaches it.

Every explored example in this book has a Workbench button that opens it here. For your own programs, the sandbox gives the same views a full page, keeps your draft, and makes links that carry the whole program.

Filter by pattern

Type a pattern in the filter field, or press ⌘ K or / anywhere in the book. The workbench keeps what matches and everything computed after it, and hides the rest.

A pattern matches the way a rule's input does: a coherence matches when it contains every occurrence the pattern names, whatever else it holds. In the hypergraph, each coherence of a pattern selects lanes on its own.

Next: Tests and tools

Verification · 11

Tests and tools

Bazel builds, runs and tests Photonic. It is the only tool to install; it downloads everything else.

load("//photonic:defs.bzl", "photonic_binary", "photonic_library", "photonic_test")

photonic_library(
    name = "logic",
    srcs = ["logic.particle"],
    deps = ["//library/boolean:not"],
)

photonic_binary(
    name = "example",
    srcs = ["request.wave", "value.particle"],
    deps = [":logic"],
)

photonic_test(
    name = "negation",
    source = "Invoke.Boolean.Not.True",
    targets = ["False"],
    preserve = True,
    deps = ["//library/boolean:not"],
)

A library holds only rules. A binary combines the coherences of its sources and loads each library file once. .particle and .wave share one grammar; by convention .particle holds reusable definitions and .wave runnable programs.

Command line

bazel run -c opt //command:photonic -- parse "$PWD/program/language/inference.wave"
bazel run -c opt //command:photonic -- lower "$PWD/program/language/inference.wave"
bazel run -c opt //command:photonic -- run "$PWD/program/language/inference.wave"
bazel run -c opt //command:photonic -- prism "$PWD/program/language/inference.wave" --target "$PWD/target.json"

parse prints the syntax tree, lower the program as JSON, run the explored configurations, and prism a verdict for a target in lowered JSON. lower --context copies a source's root rules into a target; --library loads a rules-only file; --path follows a direct path. bazel run starts in its runfiles directory, so pass absolute paths.

bazel test -c opt //...
bazel run -c opt //program/language:inference
bazel test -c opt //program/language:conjunction.check

This book

bazel run -c opt //toolchain/browser:serve
bazel run -c opt //book:record
bazel test -c opt //book:record.check

The server runs every example live in WebAssembly. //book:record reruns every example, lens and expression in this page and stores the results in book/record.js, which makes the book work as a local file. //book:record.check fails when that record is stale or an example contradicts its stated verdict.

Next: The standard library

Library · 12

The standard library

The standard library is written in Photonic: 69 rule files in 14 packages. Rust only loads and checks it.

Every operation is named Type.Verb, and each type belongs to one package. A request carries Function; its answer carries Return. Scalar requests run inside Invoke, which is the whole of invoke.particle:

[Invoke] (
    Function
    [Return] ()
)

Invoke opens a scope holding Function and the rest of the request. The scope's own rule [Return] () returns whatever accompanies Return. An implementation is a table:

[Function.Boolean.Not.True] Return.False
[Function.Boolean.Not.False] Return.True
[Boolean.Not.([Each] Boolean.Not)] Function.Boolean.Not

Invoke.Boolean.Not.True

Invoke.Ternary.Add.2.2

Conventions

• Each type has its own namespace: Boolean.Not, Ternary.Add, Natural.Divide. //library:test proves that no root rule can match another root rule's input, then runs checks with all fourteen packages loaded together.
• Fields carry roles: ([Left] 0).([Right] 2), ([Digit] 1).([Carry] 1).
• Answers name their variant or error: Return.Natural.Compare.Less, Return.Natural.Divide.Error.Divisor.
• A callback such as ([Each] Boolean.Not) names an operation, and each implementation owns the rule that accepts it.
• Rules can only match what is present, so every protocol ends with an explicit answer such as Return or Clean.

The library reference lists every request and answer.

Next: Linked data

Library · 13

Linked data

Unbounded values are linked: a handle coherence reaches cells elsewhere in the same scope.

A chain handle is Zero or a Head carrying a private seal and its methods. Requests sit beside the handle:

Every output of an event receives the remainder, so a rule with two outputs duplicates a handle. Programs therefore move a chain by sending it on and forgetting the other copy, then continue on Clean. This program pushes 2, 0 and 1, reverses the chain and reads back 2, 0, 1:

Push.([Digit] 2).Zero, Stage.1
[Built, Stage.1] (Push.([Digit] 0)) (Forget.Stage.2)
[Built, Clean.Stage.2] (Push.([Digit] 1)) (Forget.Stage.3)
[Built, Clean.Stage.3] (Function.Chain.Reverse) (Forget.Inspect.Start)
[Return.Chain.Reverse, Clean.Inspect.Start] (Read) (Forget.Inspect.0)
[Yield.([Digit] 2), Clean.Inspect.0] (Read) (Forget.Inspect.1)
[Yield.([Digit] 0), Clean.Inspect.1] (Read) (Forget.Inspect.2)
[Yield.([Digit] 1), Clean.Inspect.2] Done

A vector holds any value that answers Forget, including naturals, chains and other vectors, by reference. Function.Vector.Sort sorts a vector of naturals with a stable, adaptive merge sort: one pass splits the input into runs, balanced passes merge them pairwise, and alternating orientation means no merge result is ever reversed. For n items in r runs it makes at most n − 1 + n⌈log₂ r⌉ comparisons.

bazel test -c opt //program/ternary:reversal.check
bazel run -c opt //program/vector:sort

Next: Arithmetic

Library · 14

Arithmetic

A natural is a chain of base-three digits, least significant first. All of its arithmetic runs as Photonic rules.

Function.Natural.Add sits beside Operand.Left and Operand.Right and answers Return.Natural.Add. Subtraction answers a number or Error.Underflow; division answers a quotient and a remainder, or Error.Divisor; comparison answers Less, Equal or Greater and leaves both operands intact. Integers add a sign: zero is Positive, and division truncates toward zero.

The expression package parses and evaluates infix expressions with precedence, left association, parentheses and unary minus, and answers Error.Syntax, Error.Stack or Error.Divisor for bad input. Below, the host only turns your characters into a token tape. Parsing and every digit of arithmetic are Photonic rules.

The panel shows the program your expression becomes. When the book is served, step through every event of its path.

Next: Proof by execution

Proof · 15

Proof by execution

A theorem program lists every case of a claim, checks each one, and concludes Theorem only when all of them hold. Prism checks that it reaches exactly Theorem.

Case.(([P] True), ([P] False))

[Claim] Function.Boolean.Not.Once.P
[Return.Once] Function.Boolean.Not.Twice
[Return.Twice] Function.Boolean.Equal.Verdict.P

[Holds.(([P] True), ([P] False))] Theorem

The first line expands into two cases. ([P] True) is a field, so every P in its case becomes True. case.particle gives each case its own scope: a true verdict returns Holds with the case's assignment, a false one Counterexample. The last rule needs one Holds for every assignment, and consuming them leaves exactly Theorem.

Four kinds of claims

Every term is Photonic structure that rules can match: Times.([Left] X).([Right] Y), Meet.([Of] X).([Of] Y), Less.([Left] X).([Right] Y), Equation.([Side] S).([Side] T). Two Of fields form a multiset, so commutativity needs no proof.

What is proved

84 claims: 79 proofs and 5 refutations. The last three layers prove the standard library itself, so linked addition, subtraction, comparison and successor are correct at every width. The theorem guide explains how to write one.

bazel test -c opt //theorem/...

Next: Inside the runtime

System · 16

Inside the runtime

The runtime is Rust. One transition kernel applies every rule; two searches decide which rules to apply.

The kernel is language/evaluation.rs. Exhaustive search in language/runtime.rs also performs inference and records support: the events and derivations that justify each configuration. A configuration counts as reached only with support grounded in the start, so a cycle cannot justify itself. Direct paths live in language/path.rs, and Prism in language/prism.rs.

Reports are identical with one, two or four workers; the tests check it. A budget defers work instead of dropping it, so a larger budget resumes.

The occurrence contract states loading, ownership and consumption precisely, and the runtime roadmap sets the priorities for runtime work.

Next: The repository

System · 17

The repository

Bazel is the only dependency. It downloads pinned Rust, LLVM, Node and every crate, and it checks formatting and lints on every build.

The learner

//learning:learning optimizes Photonic programs. It edits rules with a planner guided by a label-free transformer, keeps every example correct under every schedule, and minimizes parallel time and program size. solve finds the cheapest small flat program for a task, even one defined only by tests, and proves it optimal by exhausting every program that could beat it.

bazel run -c opt //learning:learning -- train --duration 3600
bazel run -c opt //learning:learning -- solve --input "$PWD/input.wave" --output "$PWD/output.wave"

The learner guide describes the objective, the search and the results. Build organization and continuous verification describe the build and the Buildkite pipeline.

Next: Grammar and glossary

Reference · 18

Grammar and glossary

The whole grammar, every form and every term.

Grammar

module = { SOI ~ item* ~ EOI }
item = _{ concept | group | context | continuation | coherence | space }
group = { "(" ~ item* ~ ")" }
context = { "[" ~ item* ~ "]" }
continuation = { "." }
coherence = { "," }
space = @{ (" " | "\t" | "\r" | "\n" | "\u{000B}" | "\u{000C}")+ }
concept = @{ (!("(" | ")" | "[" | "]" | "." | "," | space) ~ ANY)+ }

This is the complete parser grammar. There are no keywords, operators or reserved words: Not, -> and unless are ordinary atoms.

Forms

Glossary

Atom

A run of characters without delimiters. It means nothing until rules use it.

Occurrence

One appearance of an atom or rule value, with its own identity.

Particle

An unordered multiset of occurrences in one coherence.

Coherence

An independent place where a particle lives.

Configuration

All coherences and live rules at one moment; a node of the graph.

Rule

Inputs in brackets and outputs after them. Also a value.

Event

One rule applied to one match; an arrow of the graph.

Remainder

What a match leaves in its coherences; every output receives it.

Scope

A local place opened by an output group with rules. Its own rules return to the enclosing scope.

Inference

Applying a rule to what a configuration can become, at the configuration itself.

Witness

The concrete occurrences an inferred match reached through evidence.

Field

A one-rule value such as ([Digit] 0) that keeps a role with its value.

Target

A complete configuration, including live rules, that Prism looks for.

Verdict

Reached, unreachable or unknown.

Direct path

One execution, followed until it reaches the target or can go no further.

Budget

A limit on exploration. Exhausting it defers work and leaves answers unknown.

Read next

• Standard library reference: every package, request and answer.
• Theorems: the proof contract, notation and layers.
• Occurrence contract: loading, ownership, consumption and exact targets.
• Documentation index: contracts, the roadmap and dated runtime records.