# Zulip Chat Archive

## Stream: general

### Topic: bundling typeclasses

#### Tomas Skrivan (Nov 19 2020 at 12:47):

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 (Nov 19 2020 at 12:51):

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 (Nov 19 2020 at 13:03):

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 (Nov 19 2020 at 15:08):

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 (Nov 19 2020 at 15:29):

`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`

.

Last updated: Dec 20 2023 at 11:08 UTC