Basic EquationalRealms #2532
Basic EquationalRealms #2532
Conversation
…main EquationalRealm
|
I'm going to review this "later", as it will need quite a bit of effort. |
| instance HasUID GenDefn where uid = lensMk uid uid uid | ||
| instance NamedIdea GenDefn where term = lensMk term term term | ||
| instance Idea GenDefn where getA = getA . (^. mk) | ||
| instance Definition GenDefn where defn = lensMk defn undefined defn |
There was a problem hiding this comment.
There should never be any undefined in any of the accessors. This is a symptom that something is wrong with the design.
There was a problem hiding this comment.
I agree! The undefineds are definitely very odd.
Additionally, while working on it, I really wanted to take the lensMk, elimMk, and setMk's 3 function parameters (acting on RelationConcepts, QuantityDicts, and QDefinitions) and merge them into 1 param using typeclasses, but I couldn't get a sufficient "common denominator" between the various models.
The "definition" of an EquationalRealm is interesting. I think we want it be undefined until the EquationalRealm is observed and converted into an EquationalModel using a specific RealmVariant with the attached QuantityDict.
|
|
||
| -- | Retrieve internal data from QDefinitions/RelationConcepts | ||
| elimMk :: Getter QDefinition a -> Getter QuantityDict a -> Getter RelationConcept a -> ModelKinds -> a | ||
| elimMk l _ _ (EquationalModel q) = q ^. l |
There was a problem hiding this comment.
So what this elimMk seems to say is that a "better" representation for a ModelKind would be a product of a QDefinition and "the rest of the information", labelled with the kind of model. So EquationalModel would have no payload, only EquationalRealm would.
There was a problem hiding this comment.
Would we be able to form a QDefinition for an EquationalRealm if we want EquationalRealms to represent "more than one way to define a quantity"? I think the "right-hand side" of the QDefinition would be ambiguous for an EquationalRealm, unless we wanted to have the Realm's QDefinition be of the form x $= y $= z $= ....
There was a problem hiding this comment.
Correct, the 'right hand side' will not make sense. 'a' right hand side will. I think a QDefinition needs to be precise. So indeed, there would be no such Getter. I consider that to be a good thing, as it will force us to be precise about what we mean. It would be interesting to see who uses this getter. Maybe it should return an NonEmpty ?
…DefSt from mkQuantDef and mkQuantDef'
Contributes to #2440
Closes #2436