## Stream: new members

### Topic: Type class inference with parameters

#### Alastair Horn (Apr 12 2020 at 23:19):

Lean doesn't seem to be able to infer types when parameters are involved, so while trying to implement my own version of the integers mod n, I'm having to specify all type classes explicitly. Is there a fix/workaround?
Here's a (ridiculous) example of the kind of stuff that causes problems:

section test

parameter n : ℕ

def inv_wrt_n (a : ℕ) : ℕ := a + n

instance: has_inv ℕ := ⟨inv_wrt_n⟩

#check n⁻¹ -- Fails

end test


#### Scott Morrison (Apr 13 2020 at 01:21):

Sorry, I don't have much experience with parameters (mostly because I decided long ago I didn't like them, hiding too much, and prefer to use variables). So my suggestion would be to learn to love variables instead!

#### Reid Barton (Apr 13 2020 at 01:53):

I think you'll encounter other serious problems with this approach anyways, unless you only planned to ever use this instance within the scope of the parameter.

#### Alastair Horn (Apr 13 2020 at 02:08):

Okay I'll go back to variables, thanks for the advice

#### Reid Barton (Apr 13 2020 at 02:11):

variables will make the problems clearer. How do you expect to ever specify n?

#### Alastair Horn (Apr 13 2020 at 11:02):

But I want to create a quotient that depends on a value n - the integers mod n

#### Alastair Horn (Apr 13 2020 at 11:03):

But type class resolution won't work with variables either because the instance depends on n

#### Alastair Horn (Apr 13 2020 at 11:03):

Is there a way to feed lean my specific setoid?

#### Mario Carneiro (Apr 13 2020 at 11:04):

You can put the n in the type

#### Mario Carneiro (Apr 13 2020 at 11:04):

If you have an instance instance (n : nat) : setoid (mytype n) there are no problems

#### Mario Carneiro (Apr 13 2020 at 11:05):

(also, setoids often don't need to be instances)

#### Kevin Buzzard (Apr 13 2020 at 11:05):

Or you can not use type class resolution. Mathlib has a whole collection of primed quotient stuff where the equivalence relation is found via unification.

#### Kevin Buzzard (Apr 13 2020 at 11:06):

#check @quotient.eq
-- quotient.eq : ∀ {α : Sort u_1} [r : setoid α] {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ x ≈ y
#check @quotient.eq'
-- quotient.eq' : ∀ {α : Sort u_1} {s₁ : setoid α} {a b : α}, quotient.mk' a = quotient.mk' b ↔ setoid.r a b


#### Kevin Buzzard (Apr 13 2020 at 11:06):

Note [setoid] v {setoid}

#### Kevin Buzzard (Apr 13 2020 at 11:15):

You lose notation this way though, as you can see from the example.

#### Alastair Horn (Apr 13 2020 at 11:28):

@Mario Carneiro but if I'm trying to get type class resolution for setoid int (although I'm actually using setoid myint, as I'm using my own implementation of integers) I can't put n in the type

#### Alastair Horn (Apr 13 2020 at 11:29):

@Kevin Buzzard that, or explicitly stating everything might be the only way

#### Alastair Horn (Apr 13 2020 at 11:29):

But it's not ideal

#### Kevin Buzzard (Apr 13 2020 at 11:30):

import tactic
import data.int.modeq

section

parameter (n : ℕ)

def r : ℤ → ℤ → Prop := int.modeq n

open int.modeq quotient

def s : setoid ℤ := { r := r,
iseqv := ⟨int.modeq.refl, λ _ _, int.modeq.symm, λ _ _ _, int.modeq.trans⟩ }

example : add_semigroup (quotient s) :=
{ add := λ q r, quotient.lift_on₂' q r (λ a b, quotient.mk' (a + b))
begin
intros a₁ b₁ a₂ b₂ ha hb,
show quotient.mk' (a₁ + b₁) = quotient.mk' (a₂ + b₂),
sorry
end,

end


#### Mario Carneiro (Apr 13 2020 at 11:32):

@Alastair Horn You can, you can define foo n := int and then put the typeclass on foo n

#### Alastair Horn (Apr 13 2020 at 11:40):

Okay that seems to get rid of the errors somehow :joy:. I'll see how far I get with that and fall back on Kevin's method otherwise. Thanks

Last updated: May 10 2021 at 00:31 UTC