type class for combination of two type classes

Stream: general

[Bernd Losert]

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]

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]

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

[Yakov Pechersky]

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]

But with that,

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

example : foobar T := by apply_instance -- fails

[Bernd Losert]

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

[Bernd Losert]

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

[Bernd Losert]

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]

I think X is implicit in t0_space right now

[Kevin Buzzard]

So t0_space X makes no sense

[Kevin Buzzard]

Change variables { to variables (?

[Bernd Losert]

Ah crap. I did not notice that.

[Bernd Losert]

Yep, that worked. Thanks a lot.

[Yakov Pechersky]

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]

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.