This documentation provides a rigorous, pedagogical treatment of semantic type checking for MeTTa using MeTTaIL. It synthesizes insights from four foundational papers and two prototype implementations to answer the question:
Can MeTTaIL be used for semantic type checking?
Answer: Yes, with qualifications. MeTTaIL provides foundational capabilities for semantic type checking, but realizing the full vision requires implementing Native Type Theory (OSLF) as described in the Williams & Stay paper.
MeTTa's operational semantics (Meta-MeTTa paper, 2023) explicitly recommends OSLF for deriving "a type system for MeTTa that includes spatial and behavioral types." This documentation series explains:
| Level | Approach | Capabilities | Status |
|---|---|---|---|
| Basic | Current MeTTaIL | Sort validation, constructor checking | Done |
| Operational | Gph-enriched Lawvere | Reduction semantics, evaluation control, resources | Medium effort |
| Full | OSLF/Native Types | Behavioral predicates, bisimulation, refined binding | High effort |
These documents explain the mathematical foundations required to understand semantic type checking for MeTTa.
| Document | Description |
|---|---|
| 01-metta-operational-semantics.md | MeTTa as a state machine with rewrite rules |
| 02-native-type-theory-oslf.md | The 2-functor construction from λ-theories to type systems |
| 03-gph-enriched-lawvere.md | Simpler semantics when binding is eliminated via reflection |
| 04-rho-calculus.md | Rholang's theoretical foundation and reflection mechanism |
| 05-type-lifting.md | Deriving types from operational semantics via T(-) transformation |
| 06-inference-rules.md | Practical guide to reading and implementing inference rules |
Reading Order: Start with (01) for MeTTa background. For type derivation, read (05) and (06) next. Then either (02) for full OSLF theory or (03) for the simpler Gph-enriched approach. Document (04) explains how RHO calculus reflection bridges to Rholang.
These documents describe the existing prototypes and the path forward.
| Document | Description |
|---|---|
| 01-mettail-scala-prototype.md | Theory definitions, hypercube transformation, BNFC generation |
| 02-mettail-rust-prototype.md | Category-based checking, rewrite engine, Ascent Datalog |
| 03-rholang-integration.md | Current MeTTa-Rholang bridge via mettatron |
| 04-implementation-roadmap.md | Layered approach to full semantic type checking |
These documents describe the broader MeTTa ecosystem and implementation architectures.
| Document | Description |
|---|---|
| 01-opencog-hyperon.md | OpenCog Hyperon architecture, Atomspace, four meta-types |
| 02-hyperon-experimental.md | Official MeTTa implementation details |
| 03-mettatron.md | F1R3FLY.io's MeTTaTron compiler architecture |
| 04-mork-pathmap-integration.md | MORK and PathMap storage layer integration |
These documents describe the unified three-tier correction WFST architecture that integrates liblevenshtein with MeTTaIL for semantic type-aware correction.
| Document | Description |
|---|---|
| 01-architecture-overview.md | Three-tier WFST architecture overview |
| 02-tier1-lexical-correction.md | liblevenshtein edit distance and phonetic rules |
| 03-tier2-syntactic-validation.md | CFG validation via MORK/PathMap |
| 04-tier3-semantic-type-checking.md | MeTTaIL/MeTTaTron/Rholang semantic checking |
| 05-data-flow.md | Complete data flow through the stack |
| 06-integration-possibilities.md | Cross-language, ASR, IDE integrations |
Quick-reference materials and supporting documentation.
| Document | Description |
|---|---|
| gap-analysis.md | What's missing for full OSLF implementation |
| use-cases.md | Concrete examples of semantic type checking |
| bibliography.md | Complete reference list with annotations |
The choice between Gph-enriched Lawvere theories and full OSLF depends on one key question:
Can MeTTa's unification patterns be given a combinator representation?
The RHO calculus paper demonstrates that reflection can eliminate nominal features, suggesting the simpler Gph-theory path is viable for MeTTa's reflective capabilities.
This documentation synthesizes:
/home/dylon/Workspace/f1r3fly.io/MeTTaIL/)/home/dylon/Workspace/f1r3fly.io/mettail-rust/)/home/dylon/Workspace/f1r3fly.io/f1r3node/)/home/dylon/Workspace/f1r3fly.io/hyperon-experimental/)/home/dylon/Workspace/f1r3fly.io/MeTTa-Compiler/)/home/dylon/Workspace/f1r3fly.io/MORK/)/home/dylon/Workspace/f1r3fly.io/PathMap/)/home/dylon/Workspace/f1r3fly.io/liblevenshtein-rust/)The core mathematical construction underlying full semantic type checking:
λ-theory ──[P]──> presheaf topos ──[L]──> type system
T P(T) LP(T)
Where:
This construction is native because types arise directly from the syntax, not imposed externally.
Common type-theoretic notation used throughout these documents:
| Symbol | Name | Meaning | Example |
|---|---|---|---|
$\vdash$ | Turnstile | "derives" or "proves" | $\Gamma \vdash M : A$ means "$\Gamma$ proves M has type A" |
$\Gamma$ | Context | Type assumptions in scope | x: Int, y: Bool |
: | Type ascription | "has type" | M : A means "M has type A" |
→ | Function type | Functions from A to B | A → B |
× | Product type | Pairs of A and B | A × B |
◇ | Possibility | "possibly" (modal) | ◇A = "can become A" |
T(-) | Type lifting | Transformation function | T(A → B) = T(A) × (T(A) → T(B)) |
For detailed explanations, see 06-inference-rules.md.
Can you improve this documentation?Edit on GitHub
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |