bundling typeclasses

Stream: general

[Tomas Skrivan]

I'm working with types that usually have bunch of data attached with typeclasses and my theorems quite often look like

lemma l1 {X : Type} [add_comm_group X] [semimodule ℝ X] [topological_space X] [locally_convex_space ℝ X] ...

I would like to bundle these type classes together. I have tried

class LCS (X : Type) extends add_comm_group X, semimodule ℝ X, topological_space X, locally_convex_space ℝ X

Now I can simply write

lemma l1 {X : Type} [LCS X] ...

This is nice and more or less solves my problem, but in some cases I would like to automatically get instance of LCS X if I have add_comm_group X, semimodule ℝ X, topological_space X, locally_convex_space ℝ X. So I define an instance:

instance LCS.make (X : Type) [add_comm_group X] [semimodule ℝ X] [topological_space X] [locally_convex_space ℝ X] : LCS X := LCS.mk

But this can cause cycles during typeclass resolution. How do I deal with this problem?

[Kevin Buzzard]

Judging by the way things are done in mathlib, the usual approach is to make things variables and list all the typeclasses at the top of the file/section/namespace, so at least they don't clutter up the lemmas.

[Tomas Skrivan]

Yes I have observed that is usually the way it is done. But I have started using categorical part of mathlib and suddenly everything is bundled. So I was thinking creating one typeclass and then using category_theory.bundled. However, I'm really confused how to do things because the definition of Module for example, does not use bundled.

[Eric Wieser]

I've been told that class one_argument (X: Type) extends two_arguments R X is a bad idea and you should never do it.

[Reid Barton]

class two_arguments R X extends one_argument X is bad because it creates an instance of one_argument X that depends on an underspecified variable R.