(Algebraic) structures

[Jazzpirate]

Problem

Structured concepts (e.g. groups, topological spaces, probability spaces etc.) in informal mathematics act as both "types" ("Let G a group") as well as bundles of declarations (a group is a tuple (G,o,e,⁻¹)). They can be "instantiated" with an arbitrary number of explicit concepts (e.g. "ℤ is a group", "(ℤ,+) is a group", "(ℤ,+,0,-) is a group",...)

=> They need to be both symbols (to act as types) as well as theories (for extension/inheritance: "A group is a monoid such that...")

Ideas

Obvious solution for symbol/theory duality: Mod-types => structures as records

Inheritance/Instantiation: Parametric theories: fields are theory parameters, declared individually, treated like variables (OMVs), e.g. (prototypical syntax:)

\begin{theory}[name=Magma]
  \parameter[type=\set]{universe}{M}
  \parameter[type={\funtype{\universe,\universe}{\universe}}]{op}[2]{#1 \circ #2}
\end{theory}

\begin{theory}[name=Monoid]
  \parameter[type=\set]{universe}{M}
  \parameter[type={\funtype{\universe,\universe}{\universe}}]{op}[2]{#1 \circ #2}
  \parameter[type=\universe]{unit}{e}
  \extendmodule[universe=\universe,op=\op]{Magma}

  (axioms)
\end{theory}

where \parameter follows the syntax of \symdef (see #3) and \extendmodule[...]{T} behaves like \importmodule, except that it \lets the parameter declarations in T to their assignments in the optional arguments (if given).

Note: this is probably best implemented by having the macro that stores all declarations in a model contain the unexpanded macro definitions, the actual semantic-macro definition macros (\notation,\symdefetc.) expanding notations, and \protecting the inner-most semantic-macro expansion (the one that we need e.g. LaTeXML bindings for, which has access to the full URI of a symbol). That way, \extendmodule[foo=\bar] really should automatically replace \foo by \bar everywhere in the relevant scope, and similar for nested \extendmodules.

Instantiation

Question: Do we need to distinguish between the structure and the universe? Are there "structures" that don't have a set universe as its primary component? Does something like Let \mathcal G = (G,\circ,e,{}^{-1}) ever occur?

Either way: \instantiate[...]{T}{name } creates a macro \name. MMT can set the type of \name as Mod(T) and define it as a record with the provided assignments or undefined "dummy" constants for the missing ones. \name[p] yields the parameter declaration p in module T, which (analogous to \extendmodule) is being \let as \foo if p=\foo is part of the optional arguments of \instantiate. MMT can then lambda-abstract away the not-provided assignments (i.e. dummy constants), which corresponds to universally quantified variables or (equivalently) proof arguments (in the case of axioms) in the current scope. \instantiate then basically behaves like \extendmodule in tex, except that the names of the parameters are \name[*p*] instead of \name, and MMT can handle them differently.

If we additionally let \name without parameters be \name[p] for the first parameter p in T, and (in some cases) the macroname allowed to be empty, then this allows for both e.g. Let \instantiate{Monoid}{monoidM} $\monoidM$ a group with operation $\monoidM[op]{\cdot}{\cdot} as well as
\istantiate[universe=\IntegerNumbers,op=\natplus,unit=0]{Monoid}{} (introducing proof obligations for the monoid axioms, by abstracting away the missing declarations)

Question: It occurs to me, that we may then not even make a distinction between \parameter and \symdef - the only difference is then between \importmodule - which is an import on the MMT side - and \extendmodule and \instiate - which are an implicit structure and a named structure (or somewhat equivalently a record) respectively.
MMT needs to take care that all recursively included modules in the structures are assigned to plain includes.