Auxiliary types

Stream: general

[Kenny Lau]

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]

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]

auxiliary types can be used to help here

[Mario Carneiro]

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]

This is how Qp works, for example

[Kenny Lau]

what is Qp?

[Mario Carneiro]

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

[Mario Carneiro]

padic rats

[Kenny Lau]

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

[Kenny Lau]

I'm now experimenting them on semidirect products

[Mario Carneiro]

aha, zmodp is an example

[Mario Carneiro]

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

[Mario Carneiro]

semidirect product is a pretty good example

[Kenny Lau]

@Mario Carneiro it worked great with dihedral

[Kenny Lau]

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

[Simon Hudon]

(deleted)

[Kenny Lau]

I think we should use auxiliary types for modules

[Kevin Buzzard]

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

[Mario Carneiro]

what is the proposal exactly?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kenny Lau]

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