Package0.2.0.0
sheaf
Theories as first-class data — the L4 skeleton of the vortex estate
- Version0.2.0.0
- LicenceMIT
- AuthorDaniel Firth
- Maintainerlocallycompact@gmail.com
- Pinned byhackage sheaf 0.2.0.0
- Sourcehackage.haskell.org/package/sheaf-0.2.0.0
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- base-4.22.0.0with GHC
- containers-0.8with GHC