Why does `LawfulFunctor` not extend `Functor`

Stream: mathlib4

[Markus Schmaus]

docs#LawfulFunctor is written using a type class dependency on docs#Functor, but I could imagine another implementation which instead extends Functor:

class LawfulFunctor' (f : Type u → Type v) extends Functor f where
    map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β
    id_map : ∀ {α : Type u} (x : f α), id <$> x = x
    comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

What's the advantage of the chosen implementation over this alternative?

[Robert Maxton]

The biggest issue, at least IME, is that it's much more annoying to actually rely on structures being lawful that way.

For starters, I can't actually make the code block you posted run on its own; I had to give Lean two extra hints:

class LawfulFunctor' (f : Type u → Type v) extends Functor f where
    map_const : ∀ {α β : Type u}, mapConst = map ∘ Function.const β (α := α)
    id_map : ∀ {α : Type u} (x : f α), id <$> x = x
    comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

This ... is a running theme. Lean seems to have trouble finding typeclass instances when they're included by extends, and you'll often end up making your own projections to help it along anyway. On top of that, while it doesn't happen in the LawfulFoo pattern specifically, in general there's a footgun that can crop up whenever using extends -- if you specify the definitions of fields existing in the base object, you aren't actually specifying the definitions, you're just giving default definitions and can't rely on those definitions in proofs.

Certainly, if you already know about that trap you can just not do that and make instances for those cases, but as a general habit + good habit to teach new users, it's probably better to just make separate instances to begin with.

... Also, I recall hearing about performance issues from typeclass search, that result from instance loops (class C X extends A X, B X means [C X] implies [A X] and [B X], but then you -- quite reasonably -- create an automatic instance [A X] [B X] : C X). And while it's annoying and verbose to have to type out too many typeclasses, separating them when possible does allow you to not need that backward direction that closes the instance loop, if you just depend on the component typeclasses directly.

[Markus Schmaus]

I see what you mean, even the code you provided throws an error in the current Lean playground. I got it to work using the code below, but I can see how this is annoying.

class LawfulFunctor' (f : Type u → Type v) extends Functor f where
    map_const : ∀ {α β : Type u}, toFunctor.mapConst (α := α) = toFunctor.map ∘ Function.const β
    id_map : ∀ {α : Type u} (x : f α), id <$> x = x
    comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : f α), (h ∘ g) <$> x = h <$> g <$> x

[Eric Wieser]

I don't think the comment about typeclass loops is relevant here

[Yaël Dillies]

I don't think there's a particular reason why LawfulFunctor does not extends Functor. One reason would be that you want to talk about functors which have stronger properties that Functor and state they're lawful without having to introduce StrongerLawfulFunctor, but I don't think that really happens in practice.

[Eric Wieser]

It used to extend functor, but @Sebastian Ullrich changed it (without comment) 6 years ago in https://github.com/leanprover-community/lean/commit/940aca1ec331707ee4c789cf86069070a6f5931e