Package0.2.0.1
sheaf
Theories as first-class data — the L4 skeleton of the vortex estate
- Version0.2.0.1
- LicenceMIT
- AuthorDaniel Firth
- Maintainerlocallycompact@gmail.com
- Pinned byhackage sheaf 0.2.0.1
- Sourcehackage.haskell.org/package/sheaf-0.2.0.1
Modules
- Sheaf.MorphismA theory morphism T₁ → T₂: a mapping of the source theory's
- Sheaf.TheoryA 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.23.0.0with GHC
- containers-0.8with GHC