Zulip Chat Archive

Stream: general

Topic: Auxiliary types


view this post on Zulip Kenny Lau (Dec 11 2018 at 23:48):

I've been thinking about auxiliary types. Types like additive and multiplicative. Types that help the type-class inference system do its job. Interestingly I don't see a wide use of auxiliary types. I understand that one of the inconveniences is that sometimes you want to refer to elements of the original type, and transferring between the real type and the auxiliary type might prove a bit troublesome. What are your thoughts on auxiliary types?

view this post on Zulip Kenny Lau (Dec 11 2018 at 23:49):

So for example there are definitions that should be instances, but is not so because the typeclass system could not possibly figure out the argument. What if we then created auxiliary types to solve this problem?

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:55):

auxiliary types can be used to help here

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:57):

for example, if you have a module on B from a ring hom f : A -> B, then this is a bad instance because the ring hom f is not a typeclass but it is required for the instance. If you have a wrapper type ring_hom_module f := B, then lean can handle it because it is now inferred by unification instead of typeclass inference

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:57):

This is how Qp works, for example

view this post on Zulip Kenny Lau (Dec 11 2018 at 23:59):

what is Qp?

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:59):

actually never mind, that's not a good example (it is an example of something else)

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:59):

padic rats

view this post on Zulip Kenny Lau (Dec 11 2018 at 23:59):

actually I've been using exactly the same example and it has been working great

view this post on Zulip Kenny Lau (Dec 11 2018 at 23:59):

I'm now experimenting them on semidirect products

view this post on Zulip Mario Carneiro (Dec 11 2018 at 23:59):

aha, zmodp is an example

view this post on Zulip Mario Carneiro (Dec 12 2018 at 00:00):

it has an explicit argument hp : prime p so that lean can derive the field instance

view this post on Zulip Mario Carneiro (Dec 12 2018 at 00:00):

semidirect product is a pretty good example

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:14):

@Mario Carneiro it worked great with dihedral

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:16):

https://github.com/kckennylau/Lean/blob/master/semidirect_product.lean

view this post on Zulip Simon Hudon (Dec 12 2018 at 01:18):

(deleted)

view this post on Zulip Kenny Lau (Dec 16 2018 at 09:53):

I think we should use auxiliary types for modules

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 09:58):

@Mario Carneiro you hoped that Kenny would know how to fix modules but he knows several possible solutions. Which is best?

view this post on Zulip Mario Carneiro (Dec 16 2018 at 10:00):

what is the proposal exactly?

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 11:21):

I don't even understand the outparam proposal, I am still an outparam amateur

view this post on Zulip Kevin Buzzard (Dec 16 2018 at 11:22):

There's an old thread which goes through it which I will dig up at some point

view this post on Zulip Kenny Lau (Dec 16 2018 at 11:33):

something like:

universes u v

class has_scalar (α : Type u) (γ : Type v) := (smul : α  γ  γ)

infixr `  `:73 := has_scalar.smul


structure module.core (R : Type u) [ring R] (M : Type v) [add_comm_group M] extends has_scalar R M :=
(smul_add :  (r:R) (x y:M), r  (x + y) = r  x + r  y)

def module_type {R : Type u} [ring R] {M : Type v} [add_comm_group M] (m : module.core R M) := M

Last updated: May 08 2021 at 09:11 UTC