automatically declare helper classes

Stream: metaprogramming / tactics

[Perry]

for my own education, I'm trying to write something that will take a declaration of a class that represents models of an equational theory, such as (the obvious definition of) Monoid, and automatically declares a class like e.g. MonoidHomomorphism

I'm agnostic indifferent to how the syntax will look because I haven't been able to get anything to work, but it could look like

@[algebraic] class Monoid (a : Type) where
    mult : a \to a \to a
---...  etc.

#print MonoidHomomorphism -- struct MonoidHomomoprhism (M : Type) (N :Type) [Monoid M] [Monoid N]  : Type
--... etc.

Do I want a macro, elab, or attribute? or some combination, or something else? Like I said, I haven't been able to get any of these to work so far. Is this even possible?

Also, would this type of thing ever make its way into mathlib, or does this go against any conventions? Note that your answer to this question will not determine whether I make this thing for myself

[Thomas Murrills]

I think an attribute is indeed likely what you want, since attributes are applied to declarations (actual constants and their types and values, as Lean expressions), and I’m guessing you’d want to operate on the actual types of the class’s fields as opposed to their syntax! :)

[Thomas Murrills]

You’d then be doing your work primarily in the add field of the attribute, and you’d have the chance to operate on the declaration’s name with the environment available. This would let you check if it’s a class, look up the projections/fields and their values/types, then construct appropriate expressions for the types/values of your new declaration, and add the new declaration(s).

Which doesn’t give you the hooks you need yet—there is a small zoo of different attribute kinds to choose from—but it is doable. The real work would be figuring out how to transform the expressions systematically, and the rest is fairly standard (if esoteric and not well-known!).

You could in fact start with that hard part, and try to figure out how you’ll transform the Exprs of the class’s type and projections into the generated structure’s type and projections.

(Various attributes already generate and add declarations, which you could pattern off of; for example, to_additive, though that particular example is quite complex. Surely there’s a better example… :thinking:)

[Perry]

thank you Thomas :) and thanks for giving me the impression that this not a very well-trodden path, was worried i was messing up something easy