Declaring canonical instance of typeclass?

Stream: new members

[cbailey]

If I have a typeclass with a funciton f : A -> B , and for any argument type A it will have at most one instance declared, is there a way to mark it so that I don't have to annotate the return type at the call site? As an artificial example:

-- class provides one function f mapping α to some representation
class to_representable (α : Type) {β : Type} [has_repr β] :=
(f : α → β)

def nat_to_string : ℕ → string := (λ n : ℕ, "I am a nat")
def int_to_list : ℤ → list ℤ := (λ z : ℤ, [z])

-- These will be the only instances of this typeclass for nat and int respectively
instance : to_representable ℕ := ⟨ nat_to_string ⟩
instance : to_representable ℤ := ⟨ int_to_list ⟩

open to_representable

-- Have to call like this, explicitly passing β
def with_type1 := f string (999 : ℕ)
def with_type2 := f (list ℤ) (1 : ℤ)

-- Want to be able to call like this
def without_type1 := f (999 : ℕ) -- type mnismatch application...
def without_type2 := f (1 : ℤ)

[Kevin Buzzard]

Well we were just talking about the dangers of this in another thread, but you could move beta into the class as a field I guess

[Mario Carneiro]

-- class provides one function f mapping α to some representation
class to_representable (α : Type) :=
(β : Type) [r : has_repr β] (to_fun : α → β)

def to_representable.f {α} [to_representable α] :
  α → to_representable.β α := to_representable.to_fun

def nat_to_string : ℕ → string := (λ n : ℕ, "I am a nat")
def int_to_list : ℤ → list ℤ := (λ z : ℤ, [z])

-- These will be the only instances of this typeclass for nat and int respectively
instance : to_representable ℕ := ⟨_, nat_to_string⟩
instance : to_representable ℤ := ⟨_, int_to_list⟩

open to_representable

-- Want to be able to call like this
def without_type1 := f (999 : ℕ)
def without_type2 := f (1 : ℤ)

[Mario Carneiro]

alternatively, with out_param:

-- class provides one function f mapping α to some representation
class to_representable (α : Type) (β : out_param Type) [out_param (has_repr β)] :=
(to_fun : α → β)

def to_representable.f {α β} [has_repr β] [to_representable α β] :
  α → β := to_representable.to_fun

def nat_to_string : ℕ → string := (λ n : ℕ, "I am a nat")
def int_to_list : ℤ → list ℤ := (λ z : ℤ, [z])

-- These will be the only instances of this typeclass for nat and int respectively
instance : to_representable ℕ _ := ⟨nat_to_string⟩
instance : to_representable ℤ _ := ⟨int_to_list⟩

open to_representable

-- Want to be able to call like this
def without_type1 := f (999 : ℕ)
def without_type2 := f (1 : ℤ)

[cbailey]

I was just about to ask what the syntax was to shoehorn the typeclass constraint in there. This is perfect.

[cbailey]

@Kevin Buzzard You mean the danger for the consumers of the API?

[Mario Carneiro]

I cheated a bit in the first version, because everything is in Type 0

[Mario Carneiro]

when you allow for universes the free universe argument for beta can cause problems

[Mario Carneiro]

but at least with the stuff in the example, everything works without incident if you put universes in as in

universes u v
class to_representable (α : Type u) :=
(β : Type v) [r : has_repr β] (to_fun : α → β)

[cbailey]

I'll keep that in mind. What exactly is out_param? I've seen it here and there, but searching the lean repo wasn't terribly enlightening.

[Mario Carneiro]

searching the chat will have better results

[cbailey]

Word.

[Kevin Buzzard]

https://gitter.im/leanprover_public/Lobby?at=5a6e31685a9ebe4f75e77351

[Kevin Buzzard]

searching the old chat has the best results :-)

[cbailey]

Oh, nice. I didn't even know there was an old chat.

[Kevin Buzzard]

please don't post anything there :-)

[Kevin Buzzard]

we all got bored of going back once a month saying "we're now at the new chat"