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