Zulip Chat Archive

Stream: Is there code for X?

Topic: Functoriality of finset

Yaël Dillies (Dec 22 2021 at 14:37):

For #10955, I need the fact that finset is docs#alternative. It seems like the only ingredients we have in that direction are docs#finset.is_lawful_functor and file#src/data/multiset/functor.lean. Am I right?

Eric Wieser (Dec 22 2021 at 14:47):

I'm thinking this might end up being noncomputable, because the obvious choice for or_else is insert (using the list version for reference) and that requires decidability, for which there's no way to accept a decidable instance

Eric Wieser (Dec 22 2021 at 14:48):

That is: probably worth having anyway, but not necessarily worth using in your PR

Yaël Dillies (Dec 22 2021 at 14:52):

That's what I'm thinking too. It will be noncomputable for sure. Similarly, #2997 provides a computable |equiv_functor.map instead of the noncomputable one coming from finset.is_lawful_functor

Eric Wieser (Dec 22 2021 at 14:55):

Given that one of the main uses of the monadic stuff seems to be for actually writing executable meta code, it seems awfully unfortunate that the typeclass design doesn't allow a computable instance here

Anne Baanen (Dec 22 2021 at 14:57):

Indeed, it would be an amazing function if we could somehow restrict the quantification of classes. Here, we have that finset is (computably) applicative, but only if there's decidable_eq on the parameter to finset. Similarly, I would love to just write instance : monoid_hom_class ring_hom but this only holds under the assumption that the domain and codomain are rings. And I think a lot of the category theory library could do without bundling.

Eric Wieser (Dec 22 2021 at 15:16):

One way to fix this monadic stuff (both in terms of extra assumptions, and in terms of universe polymorphism) might be to change the classes to:

class functor' (α β : out_param Type*) (fα fβ : Type*) :=
(map : (α → β) → fα → fβ)
(map_const : β → fα → fβ := map ∘ function.const α)

instance {α β : Type*} : functor' α β (list α) (list β) :=
{ map := list.map }

It wasn't immediately obvious whether this would work for the full heirarchy of classes

Eric Wieser (Dec 22 2021 at 15:19):

Or even using out_param to avoid some verbosity:

-- this name is lousy!
class is_monadic (α : out_param Type*) (fα : Type*) : Prop
instance {α : Type*} : is_monadic α (list α) := is_monadic.mk

class functor' {α β : out_param Type*} (fα fβ : Type*) [is_monadic α fα] [is_monadic β fβ] :=
(map : (α → β) → fα → fβ)
(map_const : β → fα → fβ := map ∘ function.const α)

instance {α β : Type*} : functor' (list α) (list β) :=
{ map := list.map }