HORIZON HASKELLDocslts/ghc-9.14.xb2f3bfd2026-10-11Search names, modules, packages, or :: a typeCtrl K

GHC 9.14.1 · lts/ghc-9.14.x · b2f3bfd · 2026-10-11

Package0.2.0.0

sheaf

Theories as first-class data — the L4 skeleton of the vortex estate

Modules

2 modules
  • Sheaf.Morphism9A theory morphism T₁ → T₂: a mapping of the source theory's
  • Sheaf.Theory17A theory as first-class data: the signature of a vortex DSL —

Description

A theory is the signature of a vortex DSL: its sorts, its operations (sorted arities) and the equations its terms satisfy — pure syntax, no interpretation, no IO. This package holds the Theory datatype, a well-formedness check, and a canonical printer/parser whose round-trip law is the estate master plan's G18a (L4-P0) exit check. Morphisms, pushouts and the sheaf gluing of models are later phases that build on this. Library-only so the elaborator's closure carries no host code.

Depends on

2 packages

Used by in this set · 1