Zulip Chat Archive

Stream: new members

Topic: Type class inference with parameters


view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Alastair Horn (Apr 13 2020 at 02:08):

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

view this post on Zulip Reid Barton (Apr 13 2020 at 02:11):

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

view this post on Zulip 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

view this post on Zulip Alastair Horn (Apr 13 2020 at 11:03):

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

view this post on Zulip Alastair Horn (Apr 13 2020 at 11:03):

Is there a way to feed lean my specific setoid?

view this post on Zulip Mario Carneiro (Apr 13 2020 at 11:04):

You can put the n in the type

view this post on Zulip Mario Carneiro (Apr 13 2020 at 11:04):

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

view this post on Zulip Mario Carneiro (Apr 13 2020 at 11:05):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 11:06):

Note [setoid] v {setoid}

view this post on Zulip Kevin Buzzard (Apr 13 2020 at 11:15):

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

view this post on Zulip 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

view this post on Zulip Alastair Horn (Apr 13 2020 at 11:29):

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

view this post on Zulip Alastair Horn (Apr 13 2020 at 11:29):

But it's not ideal

view this post on Zulip 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,
  add_assoc := sorry }

end

view this post on Zulip 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

view this post on Zulip 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