A candidate morphism from morSource to morTarget: a map on sort
names and a map on op names. A sort/op not in a map is sent to itself
(the common case for an inclusion S ↪ T, where most names are
shared). Whether this candidate actually preserves the source's
equations is decided by checkMorphism.
Modulesheaf-0.2.0.0GHC2021
Sheaf.Morphism
A theory morphism T₁ → T₂: a mapping of the source theory's
sorts to the target's sorts and its operations to the target's
operations, that preserves the equations. This is how a feature
translates between apps (estate master plan G18b, L4-P1): beat
detection in strobe maps into mast because both present over the same
signal vocabulary, and the morphism is the witness.
A candidate mapping is just data; whether it is a genuine morphism is
a checked property (checkMorphism). The two laws that make morphisms
a category — identity and composition — are provided and are the
exit checks for this phase, alongside "a valid mapping is accepted and
an equation-breaking one is rejected with a precise message."
No interpretation here: a morphism relates two theories (syntax). Models (interpreters) and their reindexing along a morphism come with the sheaf phase (G18e).
- 2 types
- 7 values
- Packagesheaf-0.2.0.0
- Exports9
- LanguageGHC2021
- LicenceMIT
- SourceMorphism.hs
Morphisms
3 declarationsThe identity morphism on a theory: every sort and op to itself.
checkMorphism identityMorphism = [] always.
Compose g : T₂ → T₃ after f : T₁ → T₂, giving T₁ → T₃. The
composite's maps are the source names run through f then g. (The
caller is responsible for morTarget f == morSource g; that
precondition is checked and reported rather than assumed.)
Applying a mapping
3 declarationsSend a source sort to its target sort (as a Sort).
Send a source op's name to its target op, looked up in the target theory (so the result carries the target's arity). Nothing if the mapped name is not an op of the target — a well-formedness failure the check reports.
Translate a source term into a target term by renaming its ops and its variables' sorts. Variable names are kept; their sorts move.
Checking
3 declarationsWhy a candidate mapping fails to be a morphism.
Constructors
SortNotInTarget String Stringa source sort maps to a name that is not a sort of the target
OpNotInTarget String Stringa source op maps to a name that is not an op of the target
OpArityChanged String Int Inta source op and its image differ in argument count
OpSortsChanged Stringa source op's argument/result sorts do not map to its image's
EquationNotPreserved Equationthe image of a source equation is not an equation of the target
MismatchedCompositecomposing
g . fwheretarget f ≠ source g
Instances2Eq, Show
Eq MorphismErrorDefined in sheaf-0.2.0.0 · Sheaf.MorphismShow MorphismErrorDefined in sheaf-0.2.0.0 · Sheaf.Morphism
Check that a candidate mapping is a genuine morphism: every mapped sort and op exists in the target, each op's arity and sorts are respected (its image's argument/result sorts are exactly the images of the source op's), and — the substance — the image of every source equation holds in the target (is, up to the target's own equations at a later phase, one of the target's equations; here, syntactically present after canonicalising). Returns the list of failures (empty = a genuine morphism).
At this phase "the image equation holds in the target" is checked syntactically: the mapped equation must appear among the target's equations (order-insensitively, either orientation). A later phase, once the rewrite system exists (theory-verification #3), upgrades this to "the two sides normalise equal in the target", which is the proper semantic check.
Convenience: is this candidate a genuine morphism?