Specifying Domain of a Functor

Stream: new members

[Reed Mullanix]

I've defined a category instance, and would like to define a functor out of it. However, as categories are implemented as typeclasses on objects and not structures unto themselves, it appears that I can't select a specific category to be the domain of the functor. Is there a work around to this?

[Markus Himmel]

There are several ways to do this.

1. Don't provide multiple instances for the same type, but use type tags: if you want to define a second category instance on foo, do def bar := foo and define the second instance on bar. This approach is sometimes used in mathlib, see for example docs#additive
2. use local attribute [instance, priority <some large number>] to make type class resolution pick your instance.
3. Instead of C \func D, write @category.functor and supply the instance explicitly.

[Johan Commelin]

Markus is spot on, but note that from the point of library design and larger scale of things, option (1) is clearly the most desirable. Option (2) and (3) will most give annoying clashes when multiple files are interacting and have different ideas of which category instance they expect on a given type. And users will also get confused (not at the place where you define the functor, but when it gets used and they have forgotten which category instance was used on the domain).

[Scott Morrison]

It's important to remember that typeclass resolution is essentially syntactical: if foo already has a category structure, and you def bar := foo, then by default there's no category structure on bar. (And in particular, you're welcome to put a different category structure on it, without causing problems.)

[Scott Morrison]

When you do want to move a category (or anything else) structure across such a synonym, there are derive handlers: grep for @[derive category] for examples.

[Scott Morrison]

This is not a workaround, but the intended use of the typeclass system.

[Kenny Lau]

#xy

[Reed Mullanix]

Ah, I didn't know about the def thing, that looks like it will for nicely. Thanks for the clarification everyone!