Zulip Chat Archive

Stream: general

Topic: head-based instance resolution

Yury G. Kudryashov (Jul 06 2019 at 06:49):

I think, it would be nice to have "canonical" class instances associated with some "heads". E.g.., if we're looking for [group (opposite α)], then we can go ahead and look for [group α].

Yury G. Kudryashov (Jul 06 2019 at 07:13):

Actually, I wonder how many cases can be covered by (1) "heads" based canonical instances; (2) substructures.
E.g., is_group_hom → is_monoid_hom is not covered right now but can be covered if we redefine is_group_hom to extend is_monoid_hom, and define (not an instance) is_group_hom.mk' : ∀ f, is_mul_hom f → is_group_hom f.

Yury G. Kudryashov (Jul 06 2019 at 08:10):

Another related idea: may be, it is easier to cache all substructures of defined instances than to go up the tree every time we need [has_mul α].

Yury G. Kudryashov (Jul 06 2019 at 16:00):

I guess, this is bad for some reason but I can't see what is the reason.

Last updated: Aug 03 2023 at 10:10 UTC