Skip to content
Eigenius

ESL user guide

ESL — the Eigenius Surface Language — is the human-friendly syntax for declaring ontologies, defining typed programs, and constructing resource instances. It compiles to Eigon-JSON resources that the EigenTT kernel type-checks and evaluates.

This guide is written against the implementation in kernel/src/esl/ and the type-theory kernel in kernel/src/nbe/ and kernel/src/program/. The specification it complements is D7. Every feature described here is grounded in source — chapters link directly to the modules that implement them.

How to read this guide

The chapters are ordered for sequential reading: each builds on concepts introduced earlier. If you already know a typed functional language and a typed knowledge graph (RDF/SHACL/OWL), you can skim chapters 1–3, internalise chapter 6 (Resources, types, and the layer), and then dip into the per-construct references in chapters 4 and 5.

The single most important chapter for understanding how Eigenius differs from a standalone type-theory or a standalone knowledge graph is Chapter 6 — the bridge between the resource graph and the type system. Several patterns in chapters 4, 5, 8, and 9 only make sense once that bridge is internalised.

Chapters

  1. Introduction — what ESL is, the two-layer design (HCL-style declarations + ML-style expressions), how it compiles to Eigon-JSON, and how it relates to the kernel and the rest of Eigenius.

  2. Quick tour — six worked examples: minimal class+property+resource, a program with let and apply, sized inductive types, codata streams, component calls with config blocks, and an institution-dispatched decide predicate.

  3. Lexical structure — tokens, keywords (declaration / expression / type), identifiers and qualified names (ns:local), variables, literals, operators, the lambda forms (\ and λ), comments.

  4. Declarations — per-form reference: namespace, class, property, resource, data (inductive types with bounded binders), codata (coinductive types), program. Syntax + emitted resource shape + kernel mapping for each.

  5. Expressions — per-construct reference for the program-body sublanguage: let, Apply, Lambda, Case, Match, Construct, Project, MapExpr, ReduceExpr, CoRecord, Pair, Literal, Var, plus the formula(...) Pratt-parsed math sublanguage that lowers to chain-resident formulas:FormulaTerm values (full reference in the formula language guide). For each: syntax, kernel Exp it compiles to, type-check rule, evaluation rule, capability-mode notes.

  6. Resources, types, and the layer — the bridge chapter. How a single IRI is simultaneously a resource you can query and a type you can ascribe. Ontology-as-types resolution. The mappings table (declaration ↔ resource shape ↔ kernel term/type). When and how the kernel calls back into the layer.

  7. Type theory primer — universes, Π/Σ-types, inductive types, coinductive types, sized types, identity types, normalization-by-evaluation. Brief and pragmatic; cross-linked to chapter 6.

  8. Capability modes — Pure / Read / Check / IO and how they gate which kernel AST nodes can produce values vs. stay neutral. Covers the EigonClass resolution rule, component dispatch, and institution constraint firing.

  9. Institutions in ESL — the institution surface from a program-author perspective under D14: declarations (Institution, ExportFormat, ImportFormat, QueryClass, Comorphism), how cap:predicate(args) dispatches as Exp::NativeDecide returning a Verdict, why comorphisms aren’t expression-level, and the life-science motivating example.

  10. Error messages — common compile-time and check-time errors with the messages you’ll see, what they mean, and how to fix them.

  11. Appendix — EBNF grammar reference (linked to D7 §7 as authoritative), keyword list, source file index.

Source index

All implementation referenced in this guide lives in kernel/src/esl/, kernel/src/program/, and kernel/src/nbe/. See §12 appendix for the complete file-by-file list.

Ready to start? → 1. Introduction