Declaring vs inferring schemata

[wwaites]

There is a choice here:

1. Write rules that need to be in some sense consistent with each other, and from the rules, infer the schema for system state. So if a rule talks about an agent's age, well, age must be in the schema for those kinds of agents.
2. Specify the schema and then check that the rules are consistent with it. If not, it is an error.

Both approaches have advantages and disadvantages. (1) is nice because you can just write rules, and when we start think of composing models together (basically by concatenating rule-sets) we do not have to do anything explicitly with the schema. Very convenient. (2) is nice because sometimes rules become complicated and getting them right is tricky so a declaration of the schema ahead of time means you can do a kind of type checking on the rule. Also very convenient.

FWIW, KaSim allows both of these strategies. If you declare agents (~ specify the schema) then it will check that the rules make sense, if you don't it will derive the appropriate declarations if possible.

[kris-brown]

This comes up not just for rules, but also parts of the schema which are implicitly defined via state charts and Petri nets (we'd want to hide the idea that there exists a schema at all from users who want to work exclusively with that interface!). But, to just focus on rewrite rules:

We can imagine making rewrite rules for different schemas, but these schemas can all be glued together (objects and generating morphisms with the same name are identified), so there is a canonical schema that they all live in, and the rules can be $\Sigma$ migrated into such a schema. Do you think that would work?

Note, one way it could fail at runtime is if one schema is $A \rightarrow B$ and the other is $B \rightarrow A$, such that when you $\Sigma$ migrate something into it you'll generate an infinitely-sized ACSet.

[wwaites]

Yes, that handles (1). Just saying that sometimes it's nice to have something akin to type checking.