`Idea` typeclass: What?

[balacij]

A chunk that satisfies Idea means that it might have an abbreviation and is also named (via the NamedIdea constraint, which says that the chunk has an NP ["the 'term' being defined by this chunk"]).

Commentary:

1. DataDefinition` satisfies it, implying it might have an abbreviation. While I don't have any issue with that, the abbreviation instance refers to the abbreviation of the quantity being defined by the DD. That seems wrong. ModelKinds, TM, GD, and IM too.
2. Quantity is a constraint that wraps together Idea, HasSpace, and HasSymbol, but I don't quite see why Idea is involved rather than NamedIdea.

Now, two questions:

1. Following the wiki, should we rename Idea to MayHaveAbbreviation?
2. Recall that we want to stop nesting chunks. With NamedIdea, Idea is effectively a classy lens for IdeaDict (a record pairing a UID, noun phrase [a term being declared] and Maybe an abbreviation). Many chunks currently still "extend" IdeaDicts (e.g., they carry an entire IdeaDict within them, from which they get their UID, term/name, and Maybe abbreviation). QuantityDict is one such example, and its Idea+NamedIdea instances are immediately reliant on the internal IdeaDict. Assuming we want to inch further towards not nesting chunks, the QuantityDict has its own UID and would only contain a reference to IdeaDict (via a typed UID reference). Should Idea and NamedIdea still be instantiated for Quantity if this happens? Or should they be replaced with an instance of a hypothetical typeclass GivesStructureTo that points towards the IdeaDict (via UID) rather than giving the data from the IdeaDict?

I suppose (2) belongs to a broader question of: What is going to happen to all of our lenses that are defined purely by "deferring to the instance of some internally held chunk" as well?

[JacquesCarette]

To make real progress, I think we first need to answer:

1. What is an abbreviation?
2. How do we use abbreviations?
3. Are each of these uses correct?
4. Are there places where abbreviations are mandatory?

• The answer to 2 will help figure out what's going on with DD, ModelKinds, TM, GD and IM. Indeed the 'abbreviation for what' is the key question in those cases
• Again, I think the answer will lie in use-site code, i.e. where is the abbreviation for a Quantity used

On the two questions:

1. Perhaps. But only after the 4 steps above have been done.
2. Again, I think the 4 questions will help. Do we ever use the Idea + NamedIdea lenses associated to a QuantityDict? Maybe we don't! That would let us cleanly remove those instances, which would be progress. Easy enough to test.