HypergraphGo

README

HoTTGo

Homotopy Type Theory in Go

---

The Short Version

A production-quality Go library for:

• Hypergraph theory — generic vertex types, transforms, algorithms
• HoTT kernel — normalization by evaluation, bidirectional typing, identity types, cubical path types
• CLI tools — hg for hypergraphs, hottgo for type checking

---

Why This Exists

Hypergraphs generalize graphs by allowing edges (hyperedges) to connect any number of vertices. This library provides a flexible, efficient, and idiomatic Go implementation with rich operations, transforms, and algorithms.

The HoTT kernel implements a cutting-edge type theory foundation:

• Normalization by Evaluation (NbE) with closure-based semantic domain
• Definitional equality with optional η-rules for Π/Σ types
• De Bruijn indices with bidirectional type checking
• Cubical type theory foundations for univalent mathematics

---

Highlights

Phase 5 In Progress: Inductives & Recursors

Parameterized Inductives (v1.5.8+):

• Parameterized types: List : Type -> Type, Maybe : Type -> Type
• Constructor validation: Ensures constructors return applied inductive with correct params
• Eliminator generation: listElim : (A : Type) -> (P : List A -> Type) -> ... -> (xs : List A) -> P xs
• NbE reduction: Generic recursor reduction with parameter-aware spine handling
• Strict positivity: Full positivity checking for parameterized constructors

Core Inductives (v1.5.3+):

• User-defined inductives: DeclareInductive with full validation pipeline
• Recursor generation: Automatic eliminator type generation with IH binders
• Generic reduction: Registry-based recursor reduction for arbitrary inductives
• Built-in primitives: Nat, Bool with natElim, boolElim

Phase 4 Complete: Identity Types + Cubical Path Types

Martin-Löf Identity Types (v1.5.0):

• Identity types: Id A x y for propositional equality
• Reflexivity: refl A x : Id A x x
• Path induction: J A C d x y p : C y p eliminator
• Computation rule: J A C d x x (refl A x) --> d
• NbE support: VId, VRefl semantic values with J reduction
• Derived operations: transport, symmetry, transitivity, congruence

Cubical Path Types (gated by cubical build tag):

• Path types: Path A x y, PathP A x y for cubical equality
• Path abstraction: <i> t : PathP (λi. A) t[i0/i] t[i1/i]
• Path application: p @ r : A[r/i] with endpoint beta reduction
• Transport: transport A e : A[i1/i] with constant reduction
• Interval type: I, i0, i1, IVar with separate de Bruijn space
• Build to enable: go build -tags cubical ./...

Phase 3 Complete: Bidirectional Type Checking

• Bidirectional type checker at kernel/check with Synth/Check/CheckIsType API
• Built-in primitives: Nat, zero, succ, natElim, Bool, true, false, boolElim
• Structured error types with source spans for precise diagnostics
• Global environment with axioms, definitions, inductives, and primitives

Phase 2 Complete: NbE & Definitional Equality

• NbE skeleton under internal/eval with semantic domain (Values, Closures, Neutrals)
• Definitional equality at core.Conv with environment support
• Optional η-rules for functions and pairs behind feature flags

---

Quickstart

go get github.com/watchthelight/hypergraphgo

package main

import (
    "fmt"
    "github.com/watchthelight/hypergraphgo/hypergraph"
)

func main() {
    hg := hypergraph.NewHypergraph[string]()
    _ = hg.AddEdge("E1", []string{"A", "B", "C"})
    fmt.Println("Vertices:", hg.Vertices())
    fmt.Println("Edges:", hg.Edges())
}

Run the examples:

go run ./examples/basic
go run ./examples/algorithms

---

Installation

Go Module

go get github.com/watchthelight/hypergraphgo

APT (Cloudsmith)

curl -1sLf 'https://dl.cloudsmith.io/public/watchthelight/hypergraphgo/setup.deb.sh' | sudo -E bash
sudo apt install hypergraphgo

Other Package Managers

---

CLI

Hypergraph CLI (hg)

hg info -file example.json
hg add-vertex -file example.json -v "A"
hg add-edge -file example.json -id E1 -members "A,B,C"
hg components -file example.json
hg dual -in example.json -out dual.json
hg section -in example.json -out section.json

HoTT CLI (hottgo)

hottgo --version
hottgo --check FILE        # Type-check S-expression terms
hottgo --eval EXPR         # Evaluate an expression
hottgo --synth EXPR        # Synthesize the type

Interactive REPL with :eval, :synth, :quit commands.

---

Architecture

The kernel follows strict design principles documented in DESIGN.md:

• Kernel boundary — minimal, total, panic-free
• De Bruijn indices — core terms only; surface syntax keeps user names
• NbE conversion — no ad-hoc reductions outside documented rules
• Strict positivity — validated for all inductive definitions

See DIAGRAMS.md for comprehensive Mermaid architecture diagrams covering:

• Package dependencies
• Term and value type hierarchies
• Bidirectional type checking flow
• NbE pipeline (Eval → Apply → Reify)
• J elimination and conversion checking

---

Roadmap

Phase	Status	Description
Phase 0	✅	Ground rules and interfaces
Phase 1	✅	Syntax, binding, pretty printing
Phase 2	✅	Normalization and definitional equality
Phase 3	✅	Bidirectional type checking
Phase 4	✅	Identity types + Cubical path types
Phase 5	🔄	Inductives, recursors, positivity (parameterized ✓)
Phase 6	⏳	Univalence
Phase 7	⏳	Higher Inductive Types (HITs)
Phase 8	⏳	Elaboration and tactics
Phase 9	⏳	Standard library seed
Phase 10	⏳	Performance, soundness, packaging

Current: Phase 5 In Progress — Parameterized inductives complete Next: Indexed families, mutual inductives

---

Releases & Packaging

Releases are automated via GoReleaser. See:

• .goreleaser.yaml for build configuration
• CHANGELOG.md for version history
• RELEASING.md for release process

Release a new version:

./scripts/release.sh patch   # or minor | major | 1.2.3

This updates VERSION, creates tag vX.Y.Z, and pushes to origin.

---

Algorithms

• Greedy hitting set: polynomial time heuristic
• Minimal transversals: exponential, supports cutoffs
• Greedy coloring: heuristic
• Transforms: dual, 2-section, line graph
• Traversal: BFS/DFS connectivity

---

Contributing

Read CONTRIBUTING.md. The short version:

• Small PRs. One logical change per PR.
• Tests required. If it's not tested, it doesn't exist.
• CHANGELOG entry required.
• Kernel boundaries are sacred. Don't blur them.

If your PR is a hot take, open an issue first. It saves everyone grief.

---

License

MIT License © 2025 watchthelight

See LICENSE.md for full text.