MeTTa Programming Language Full

Atoms and Expressions

The basic elements of MeTTa are symbols (distinguished by name, optionally grounded to external data or code). Symbols compose into expressions representable as trees or, with deduplication, as metagraphs. Expressions are stored in an AtomSpace container equipped with pattern matching. There is no distinction between code and data — MeTTa programs are expressions in AtomSpace, queryable and rewritable by other programs.

Gradual Type System

MeTTa uses gradual typing: untyped symbols receive the special type ?, which is treated as functional (so expressions starting with untyped symbols are interpreted as function applications, not tuples). The arrow type (\(\to\)) describes function signatures with arbitrary arity; dependent types are supported naturally (e.g., (: Mortal (→ Human Type)) creates a dependent type indexed by Human values). Type constructors are not separate syntax — any typed symbol acts as a constructor of its type, allowing new knowledge base entries to be inserted modularly at runtime. Currying is not automatic and must be performed explicitly. Grounded types are registered via regex patterns paired with constructor functions, allowing the parser to recognize and wrap external data (e.g., floats, strings) transparently.

Type-Directed Evaluation

MeTTa's evaluation model is type-directed: expressions whose first element has an arrow type are treated as function applications (subexpressions evaluated, then the grounded function executed or equality query formed); expressions whose head has a non-arrow type are treated as tuples and evaluate to themselves. This two-rule dispatch — arrow-typed head → application, otherwise → tuple — is the core mechanism replacing traditional function-call syntax.

Pattern Matching

AtomSpace's pattern matcher extracts expressions matching a query via unification of variables (prefixed with $). Binding is asymmetric: query variable bindings are prioritized over expression variable bindings, and binding a variable to a non-variable symbol takes precedence over binding to another variable. The same variable appearing multiple times must bind to the same subexpression. Conjunctive queries use comma-joined patterns with shared variables that must be satisfied simultaneously. The pattern matcher is type-aware — type annotations are treated as expression enrichments (supplementary metadata, not structural modifications), meaning (e (: a A)) matches (e a) and the type information propagates without altering the expression structure. This enrichment model extends naturally to vector embeddings and attention values.

Equalities and Chaining

The built-in = symbol defines directed rewrite rules: (= a b) means a can be transformed to b during evaluation, but not vice versa. This directionality enables MeTTa to express causal generative models — directed paths in expression space rather than symmetric equivalences. Pattern matching against equality definitions can produce conditional matches requiring further unification, which the interpreter resolves by constructing chained equality queries. Type-level equalities (e.g., (= (TCons $a (List $a)) (List $a))) are processed the same way, enabling type computation at runtime.

Non-deterministic Evaluation

MeTTa evaluation proceeds by matching expressions against rewrite rules and replacing them with the rule body under the computed substitution. The interpreter maintains a local AtomSpace as an evaluation queue, processing one expression at a time (though concurrent evaluation of multiple targets is supported). Multiple equality matches produce multiple evaluation branches — MeTTa is inherently non-deterministic. Because equalities are not required to be unique (the same left-hand side can have multiple right-hand sides), functions can naturally express non-deterministic choice. This enables direct encoding of search problems: the Specification demonstrates a subset-sum solver using non-deterministic binary list generation and compositional evaluation. Non-total functions are permitted by default — an expression with no matching equality evaluates to itself, acting simultaneously as a type constructor and a partial function.

S-Expression Grammar and Special Atoms

The reference implementation defines a formal EBNF grammar for MeTTa syntax. Programs are sequences of atoms, optionally prefixed by ! (evaluate and return result to user; unprefixed atoms are added to the AtomSpace). The grammar distinguishes four atom kinds — Symbol (WORD tokens), Variable ($-prefixed), Grounded (WORD or STRING matched by tokenizer regex patterns), and Expression (()-delimited lists). Grounded atoms are constructed via a tokenizer — a collection of (regex, constructor) pairs that intercept matching tokens during parsing (e.g., [0-9]+ → integer parser).

Seven elementary types are built in: Type (type of types), %Undefined% (unknown type), Atom (supertype matching any atom), and four meta-types corresponding to the grammar: Symbol, Variable, Expression, Grounded. Meta-types control evaluation order — an argument typed as Atom or a meta-type is passed unevaluated to the function.

Three special result atoms have built-in semantics: Empty (branch produces no result — removed from output), NotReducible (expression cannot be reduced further — returned as-is), and Error (with structured subtypes: StackOverflow, NoReturn, IncorrectNumberOfArguments, BadArgType, BadType). The distinction between Empty and NotReducible is critical: Empty prunes a non-deterministic branch, while NotReducible preserves the expression as a valid data term.

(Provenance: repo-doc, hyperon-experimental docs — MeTTa language specification)

Evaluation Algorithm

The interpreter evaluates atoms via the metta(atom, type, space, bindings) entry point, dispatching on the atom's meta-type:

• Symbol, Grounded, or empty expression → type-cast: check the atom's declared types against the expected type via unification; return the atom if types match, or a BadType error otherwise.
• Expression → interpret_expression: extract the head's type. If it's an arrow (function) type, check argument count and types, then evaluate as a function call. If the head has no arrow type, evaluate as a tuple (each element evaluated independently).

Function evaluation uses metta_call, which either invokes a grounded function's native code or queries the AtomSpace for (= call_expr $X) equality rules and recursively evaluates the matched results. Non-determinism arises naturally: multiple equality matches produce multiple evaluation branches, each pursued independently. The interpreter filters error branches when at least one success branch exists, but returns all errors if no branch succeeds.

Pattern matching uses two-sided unification via match_atoms. Variable bindings track both value assignments (\(\text{var} \leftarrow \text{value}\)) and equality relations (\(\text{var}_1 = \text{var}_2\)). Binding merges can produce multiple results when previously bound variables are matched against new patterns, and loop bindings (circular references) are automatically filtered out.

(Provenance: repo-doc, hyperon-experimental docs — MeTTa language specification)