Abstractions

Disclaimer not everything mentioned here is on main at the time of writing this.

Abstractions

What they Are

Abstractions encapsulate the relationship between a model and a sub-model.

HasAbstractions

The HasAbstractions class is generally the best way to use abstractions. HasAbstractions has the method abstractions :: [AbstractionFor p m], which you will need to implement. AbstractionFor is a GADT wraper type on Abstraction which can be created with the WrapAbs constructor, it's purpouse is to hide some of the type information so that abstractions can be a heterogenous list allowing different abstractions to point to sub models of different types.

Writing Abstractions

There are two kinds of abstractions product abstractions and sum abstractions.

Product Abstractions

Product Abstractions encapsulate relationships to subtypes of a product type.

TODO talk about IntPair example

Sum Abstractions

Sum Abstractions encapsulate relationships to subtypes of a sum type.

TODO talk about IntEither example

Using Abstractions

Once you have abstractions there are a handfull of functions that make use of the class.

abstractionLogic

abstractionLogic :: forall m p. HasAbstractions p m => Formula p

AbstractionLogic generates a formula for all the logic implyed by your abstractions.

For product abstractions this will just be that the submodels obey their own logic ie. (SubModelLabel <$> (logic :: Formula SubModelProp)) :: ModelProp). For sum abstractions this will ensure that when the label var is true the logic is obeyed and otherwise all vars are false ie. (Var SumLabel :->: (SubModelLabel <$> (logic :: Formula SubModelProp))) :&&: ((Not (Var SumLabel)) :->: None (Var . SubModelLabel <$> (enumerated :: [SubModelProp]))). Note that for sum abstractions it is not assumed that the abstractions are exhaustive and exclusive so you will generally need something like ExactlyOne [Var IsLeft,Var IsRight] in addition to the abstractionLogic.

abstractionMorphisms

abstractionMorphisms :: forall p m. (LogicalModel p, HasAbstractions p m) => [Morphism p m] Generates morphisms from your abstractions. For product morphisms this will simply transform the morphisms of the sub model through lenses in your abstractions. For sum morphisms this will create similar morphisms (though the match logic also requires the appropriate label to be set) but it will also create new morphisms that bring the model into a given branch of the sum.

Making abstractions work with entangled logic

There are a few ways logic can become "entangled" and break the abstractions.

SubModel relationships

If the submodels have relationships enforced by the logic of the model abstractions of morphisms may be invalid. For instance if you modeled Ints as even or odd, and wanted to model pairs where one must be even and the other odd, your morphisms "right of (make even)" would be invalid because changing the pairity of the right element without changing the pairity of the left will violate your model logic.

TODO write up this example and talk about it here

To work around this we can use: parallelAbstractionMorphisms :: forall p m. (LogicalModel p, HasAbstractions p m) => [Morphism p m] This generates morphisms which use some (non-strict) subset of your abstractions on morphisms of the coresponding models and then composes them in parallel.

Trivial Model to Submodel relationships

If the model properties have a logical relationship with the submodel properties that can also break the abstractions. For instance with rationals the sign of the rational , represented by which of RatPos RatZero and RatNeg are true, is determened by the signs of the submodels ,Which of Num/Den IsPositive/IsZero/IsNegative are true. So while the morphism numerator of (negate) is invalid as it changes the sign of the rational without changing the properties, this can be fixed by composing the "fix sign" morphism:

      >>> [ Morphism
              { name = "fix sign"
              , match = Yes
              , contract =
                  removeAll [RatZero, RatPos, RatNeg]
                    >> branches
                      [ add RatZero >> matches logic
                      , add RatPos >> matches logic
                      , add RatNeg >> matches logic
                      ]
              , morphism = pure
              }
          ]

all the morphism has to do is create a branch for each sign and terminate the branches where the logic is not satisfied.

Non Trivial Model to Submodel relationships

If the model properties have a complex relationship with the submodel it can also cause morphisms to fail. For instance in the rational model the "numerator of (make large)" morphism may cause RatSmall to become invalid (and RatLarge to become Valid). This is also best to fix with sequential morphism composition, but the morphisms need to actually fix the properties.

TODO talk more about the example