Interrogating typeclasses

Stream: general

[Chris B]

Hi, I'd like to ask two questions about typeclasses in the Lean vscode extension :

1. Is there a way to display the (combinations of) "minimal/required fields" of some superclass? For example getting Lean to tell you that you can implement monad with just pure and bind even though monad extends functor, has_pure, has_seq, has_seq_left ...?
2. Is there a way to view the actual definition that lies at the end of some typeclass resolution? IE getting ⊥ : nat := 0 instead of what you get with pp.all or by turning trace.class_instances on :

@has_bot.bot nat
  (@order_bot.to_has_bot nat
     (@canonically_ordered_add_monoid.to_order_bot nat
        (@canonically_ordered_comm_semiring.to_canonically_ordered_add_monoid nat
           nat.canonically_ordered_comm_semiring)))

Thanks!

[Jalex Stark]

suggest can help with 1

[Chris B]

Thanks. Can you expand a little bit on what you had in mind? The docs didn't have any examples of it as a means of typeclass synthesis/getting hints via errors, and the naive approach didn't get me too far.

inductive Option (A : Type)
| none : Option
| some : A → Option

instance : monad Option :=
begin
  suggest,
end

There are no applicable declarations
state:
⊢ monad Option

instance suggestMonad (m : Type u → Type v) : monad m :=
begin
  suggest,
end

There are no applicable declarations
state:
m : Type u → Type v
⊢ monad m

[Jalex Stark]

ah, sad. here is an example of suggest being helpful:

import ring_theory.polynomial_algebra

variables {R A B : Type*} [comm_ring R] [semiring A] [algebra R A] [semiring B] [algebra R B]

def f1 : A ≃ₐ[R] B :=
begin
  suggest,
end

it points out that you can either directly construct the whole equiv, or that you can provide two homomorphisms and proofs that they are inverse

[Jalex Stark]

the latter is called alg_equiv_of_alg_hom

[Jalex Stark]

are you sure that mathlib has a proof that monad can be implemented from pure and bind?

[Chris B]

The instance of parser.monad in core is defined only using pure and bind, but the output of #print parser.monad with implicits on is crazy, so I'll spare you the markdown. Thanks for posting that other example, I can see how that's helpful.

[Scott Morrison]

#eval (⊥ : nat)    -- prints `0`

[Chris B]

@Scott Morrison
Thanks. So in situations where I can't just eval my way to enlightenment, is there a way to get IE has_sup.sup : nat -> nat -> nat := maxinstead of a bunch of lattice/to_has_sup stuff?

[Scott Morrison]

This is a good question, to which I don't have a definitive answer, so hopefully others will make suggestions.

[Scott Morrison]

For your second example,

run_cmd to_expr ``(has_sup.sup : ℕ → ℕ → ℕ) >>= whnf >>= trace.    -- prints `λ (a b : ℕ), ite (a ≤ b) b a`

works well.

[Chris B]

Ah that's really cool, thank you.

[Scott Morrison]

Perhaps we need a #whnf command that does exactly that.

[Kevin Buzzard]

For figuring out which fields to add when I'm making an instance of a structure I usually look at the definition of the structure, and then define the instances for the classes it's extending (recursively, ie by looking at those definitions too) and finally fill in the remaining fields manually. Of course I also look out for any slick constructors which do the work for me