having to specify members of type class with default values

Stream: general

[Bernd Losert]

I am being forced to specify members of a type class with default values. MWE:

import tactic
import order.filter.n_ary
import order.filter.partial
import order.filter.ultrafilter
import order.filter.bases
import algebra.support
import category_theory.concrete_category.bundled

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

variables {α α₁ α₂ β β₁ β₂ γ : Type*}

@[ext] class convergence_space (α : Type*) :=
(converges : filter α → α → Prop)
(pure_converges : ∀ x, converges (pure x) x)
(le_converges : ∀ {f g}, f ≤ g → ∀ {x}, converges g x → converges f x)

open convergence_space

@[ext] class kent_convergence_space (α : Type*) extends convergence_space α :=
(kent_converges : ∀ {f x}, converges f x → converges (f ⊔ pure x) x)

open kent_convergence_space

@[ext] class limit_space (α : Type*) extends kent_convergence_space α :=
(sup_converges : ∀ {f g x}, converges f x -> converges g x -> converges (f ⊔ g) x) -- f ⊔ g means f ∩ g
(kent_converges := λ f x hconv, sup_converges hconv (pure_converges x))

open limit_space

instance : limit_space ℕ :=
{
  converges := sorry,
  pure_converges := sorry,
  le_converges := sorry,
  sup_converges := sorry,
}

The error that I get here is useless:

type mismatch at field 'sup_converges'
  sorry
has type
  ∀ {f g : filter ℕ} {x : ℕ}, converges f x → converges g x → converges (f ⊔ g) x
but is expected to have type
  ∀ {f g : filter ℕ} {x : ℕ}, converges f x → converges g x → converges (f ⊔ g) x

I can fix the problem by adding kent_converges := sorry to the instance. But I want to avoid having to do this - hence the default implementation in limit_space.

[Eric Wieser]

Does using old_structure_cmd help?

[Bernd Losert]

No. It seems to cause other problems.

[Yury G. Kudryashov]

Do you have an #mwe without sorrys?

[Yaël Dillies]

Why are you making limit_space extend kent_convergence_space if that makes it have redundant fields?

[Yaël Dillies]

The right thing to do here is to make limit_space extend convergence_space and write the instance limit_space α → kent_convergence_space α.

[Yaël Dillies]

This is what we do between docs#ring and docs#semiring.

[Yaël Dillies]

The rule of thumb is "Don't have default Prop fields that do not depend on other default fields" ("Do not write default Prop fields" would fail to explain docs#preorder.lt_iff_le_not_le).

[Bernd Losert]

Isn't what I am doing similar to what is done in monad? https://github.com/leanprover-community/lean/blob/master/library/init/control/monad.lean#L23

[Bernd Losert]

The right thing to do here is to make limit_space extend convergence_space and write the instance limit_space α → kent_convergence_space α.

I can do this, but that ruins the hierarchy that I wanted to make.

[Yaël Dillies]

Those are Type-valued fields though. The implementation is important in Type, but not in Prop.

[Yaël Dillies]

How does that "ruin" your hierarchy? The only differences with what you're doing now is that you have one field less and one instance more (limit_space α → convergence_space α).

[Bernd Losert]

Well, this is just part of the hierarchy. There's two more levels after limit_space.

[Bernd Losert]

Those are Type-valued fields though. The implementation is important in Type, but not in Prop.

How is this important?

[Eric Wieser]

I don't really agree with @Yaël Dillies' "don't have default prop fields" claim, we do it in a few places and it's normally harmless

[Eric Wieser]

The only real downside seems to be whatever you're running into

[Yaël Dillies]

... and that the user is by default prompted with a goal that doesn't need solving.

[Yaël Dillies]

Bernd Losert said:

Well, this is just part of the hierarchy. There's two more levels after limit_space.

I maintain my claim. My proposed fix is local.

[Yaël Dillies]

Eric Wieser said:

I don't really agree with Yaël Dillies' "don't have default prop fields" claim, we do it in a few places and it's normally harmless

I specifically claimed that I was not advocating for "Don't have default Prop fields", but instead for "Don't have default Prop fields that do not depend on other default fields".

[Bernd Losert]

Alright. I'll have to rethink my design (I'll try Yaël's suggestion). Thanks a lot guys.