Zulip Chat Archive

Stream: general

Topic: type class for combination of two type classes


Bernd Losert (Jan 06 2022 at 23:24):

Say I have two type classes foo and bar. What is the idiomatic way of making a type class foobar that represents fooand bartogether in the sense that if a type has instances of foo and bar, it will also have an instance of foobar.

Yakov Pechersky (Jan 06 2022 at 23:25):

Question. Let's say you explicitly provide some type X an instance of foobar X. Would you also want to now, "for free", get foo X and bar X instances?

Bernd Losert (Jan 06 2022 at 23:27):

No. The type class foobar won't have any methods.

Yakov Pechersky (Jan 06 2022 at 23:31):

universes u v w

variables (α : Sort u) (β : Sort v) (γ : Sort w)

class foo :=
(as_foo : β)

class bar :=
(as_bar : γ)

class foobar extends foo α, bar α.

variables {α} [foobar α]

example : foo α := by apply_instance
example : bar α := by apply_instance

Like that?

Yakov Pechersky (Jan 06 2022 at 23:31):

But with that,

variables {T : Type u} [foo T] [bar T]

example : foobar T := by apply_instance -- fails

Bernd Losert (Jan 06 2022 at 23:33):

Ah, so to make a class with no methods, you use a period. I didn't know that.

Bernd Losert (Jan 06 2022 at 23:33):

Hmm... this is not working for me. Let me create a MWE.

Bernd Losert (Jan 06 2022 at 23:37):

Here's my MWE:

import tactic
import order.filter.partial
import algebra.support
import category_theory.concrete_category.bundled

noncomputable theory
open set function filter classical option category_theory
open_locale classical filter

variables {X Y Z : Type*}

structure convergence_space (X : Type*) :=
(converges : filter X  X  Prop)
attribute [class] convergence_space

open convergence_space

constants foo bar : Prop

class t0_space [p : convergence_space X] : Prop :=
(t0_prop : foo)

class r2_space [p : convergence_space X] : Prop :=
(r2_prop : bar)

class t3_space [p : convergence_space X] extends t0_space X, r2_space X. --  error: function expected at t0_space term has type Prop

Kevin Buzzard (Jan 06 2022 at 23:39):

I think X is implicit in t0_space right now

Kevin Buzzard (Jan 06 2022 at 23:40):

So t0_space X makes no sense

Kevin Buzzard (Jan 06 2022 at 23:41):

Change variables { to variables (?

Bernd Losert (Jan 06 2022 at 23:43):

Ah crap. I did not notice that.

Bernd Losert (Jan 06 2022 at 23:44):

Yep, that worked. Thanks a lot.

Yakov Pechersky (Jan 06 2022 at 23:48):

For posterity:

variables (X)

class t0_space [convergence_space X] : Prop :=
(t0_prop : foo)

class r2_space [convergence_space X] : Prop :=
(r2_prop : bar)

class t3_space [convergence_space X] extends t0_space X, r2_space X.

Anne Baanen (Jan 07 2022 at 10:14):

Yakov Pechersky said:

But with that,

variables {T : Type u} [foo T] [bar T]

example : foobar T := by apply_instance -- fails

Note that the above "foobar.mk", or the pair of projections foobar.to_foo/foobar_to.bar, can't both be instances due to Lean 3's typeclass implementation. Since an instance for foobar T would lead to a looping search foobar T → foo T (via the above) → foobar T (via foobar.to_foo) → foo T → foobar T →. Lean 4 should fix this specific issue because it only starts one search for each equal goal.


Last updated: Dec 20 2023 at 11:08 UTC