## Stream: general

### Topic: Auxiliary types

#### 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?

#### 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?

#### Mario Carneiro (Dec 11 2018 at 23:55):

auxiliary types can be used to help here

#### 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

#### Mario Carneiro (Dec 11 2018 at 23:57):

This is how Qp works, for example

what is Qp?

#### Mario Carneiro (Dec 11 2018 at 23:59):

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

#### Kenny Lau (Dec 11 2018 at 23:59):

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

#### Kenny Lau (Dec 11 2018 at 23:59):

I'm now experimenting them on semidirect products

#### Mario Carneiro (Dec 11 2018 at 23:59):

aha, zmodp is an example

#### Mario Carneiro (Dec 12 2018 at 00:00):

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

#### Mario Carneiro (Dec 12 2018 at 00:00):

semidirect product is a pretty good example

#### Kenny Lau (Dec 12 2018 at 01:14):

@Mario Carneiro it worked great with dihedral

#### Kenny Lau (Dec 12 2018 at 01:16):

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

(deleted)

#### Kenny Lau (Dec 16 2018 at 09:53):

I think we should use auxiliary types for modules

#### 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?

#### Mario Carneiro (Dec 16 2018 at 10:00):

what is the proposal exactly?

#### Kevin Buzzard (Dec 16 2018 at 11:21):

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

#### 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

#### 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