|
| 1 | +{-# LANGUAGE RankNTypes #-} |
| 2 | +-- | Invertible mappings between named pattern kinds. |
| 3 | +-- |
| 4 | +-- A 'RepresentationMap' names a pair of compatible structural transforms between |
| 5 | +-- two 'PatternKind's. The map itself carries only executable behavior and its |
| 6 | +-- round-trip witness. Explanatory metadata about how a map works is deferred for |
| 7 | +-- a later design that can express declarative, checkable claims rather than |
| 8 | +-- inline prose attached to the value. |
| 9 | +module Pattern.RepresentationMap |
| 10 | + ( RepresentationMap(..) |
| 11 | + , compose |
| 12 | + ) |
| 13 | +where |
| 14 | + |
| 15 | +import Pattern.Core (Pattern, PatternKind, ScopeQuery, kindName) |
| 16 | + |
| 17 | +-- | A named, invertible mapping between two pattern kinds. |
| 18 | +-- |
| 19 | +-- A 'RepresentationMap' is the executable form of an isomorphism between named |
| 20 | +-- shapes. 'forward' and 'inverse' are the two morphism components, while |
| 21 | +-- 'roundTrip' is the machine-checkable witness that the mapping preserves |
| 22 | +-- information on the domain kind. |
| 23 | +-- |
| 24 | +-- Invariants for domain-kind inputs: |
| 25 | +-- |
| 26 | +-- * 'forward' should produce a pattern accepted by 'codomain'. |
| 27 | +-- * 'roundTrip' should hold. |
| 28 | +-- * When 'roundTrip' holds, @(inverse m q . forward m q) p == p@ structurally. |
| 29 | +-- |
| 30 | +-- Notes: |
| 31 | +-- |
| 32 | +-- * Scope remains polymorphic, so maps are not tied to a particular backing |
| 33 | +-- representation. |
| 34 | +-- * Declarative, machine-checkable claims about map-specific encoding choices |
| 35 | +-- are deferred; for now those details live in documentation and tests next to |
| 36 | +-- concrete maps. |
| 37 | +data RepresentationMap v = RepresentationMap |
| 38 | + { repMapName :: String |
| 39 | + -- ^ Unique human-readable name for the map. |
| 40 | + , repMapDomain :: PatternKind v |
| 41 | + -- ^ Source kind. 'forward' is intended for patterns of this kind. |
| 42 | + , repMapCodomain :: PatternKind v |
| 43 | + -- ^ Target kind. 'forward' should produce patterns of this kind. |
| 44 | + , repMapForward :: forall q. ScopeQuery q v => q v -> Pattern v -> Pattern v |
| 45 | + -- ^ Domain-to-codomain transform, polymorphic over any valid scope. |
| 46 | + , repMapInverse :: forall q. ScopeQuery q v => q v -> Pattern v -> Pattern v |
| 47 | + -- ^ Codomain-to-domain transform, polymorphic over any valid scope. |
| 48 | + , repMapRoundTrip :: forall q. ScopeQuery q v => q v -> Pattern v -> Bool |
| 49 | + -- ^ Isomorphism witness for domain-kind inputs at a given scope. |
| 50 | + } |
| 51 | + |
| 52 | +-- | Compose two compatible representation maps. |
| 53 | +-- |
| 54 | +-- Composition is defined only when the codomain kind of the first map has the |
| 55 | +-- same 'kindName' as the domain kind of the second. The resulting map keeps |
| 56 | +-- the first domain, the second codomain, composes 'forward' left-to-right, |
| 57 | +-- composes 'inverse' right-to-left, and preserves round-trip validation in the |
| 58 | +-- same order. |
| 59 | +-- |
| 60 | +-- Categorical note: this is morphism composition for the category whose |
| 61 | +-- objects are 'PatternKind's and whose isomorphisms are 'RepresentationMap's. |
| 62 | +compose :: RepresentationMap v -> RepresentationMap v -> Either String (RepresentationMap v) |
| 63 | +compose m1 m2 |
| 64 | + | kindName (repMapCodomain m1) /= kindName (repMapDomain m2) = |
| 65 | + Left $ |
| 66 | + "compose: codomain of '" <> repMapName m1 |
| 67 | + <> "' (" <> kindName (repMapCodomain m1) |
| 68 | + <> ") does not match domain of '" <> repMapName m2 |
| 69 | + <> "' (" <> kindName (repMapDomain m2) <> ")" |
| 70 | + | otherwise = |
| 71 | + Right |
| 72 | + RepresentationMap |
| 73 | + { repMapName = repMapName m1 <> " >>> " <> repMapName m2 |
| 74 | + , repMapDomain = repMapDomain m1 |
| 75 | + , repMapCodomain = repMapCodomain m2 |
| 76 | + , repMapForward = \q p -> repMapForward m2 q (repMapForward m1 q p) |
| 77 | + , repMapInverse = \q p -> repMapInverse m1 q (repMapInverse m2 q p) |
| 78 | + , repMapRoundTrip = |
| 79 | + \q p -> repMapRoundTrip m1 q p && repMapRoundTrip m2 q (repMapForward m1 q p) |
| 80 | + } |
0 commit comments