specific implementation of Applicative/Functor from Monad

Stream: Is there code for X?

[Asei Inoue]

inductive Many (α : Type u) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

def Many.one (x : α) : Many α := Many.more x (fun () => Many.none)

def Many.union {α : Type u} : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

def Many.bind : Many α → (α → Many β) → Many β
  | Many.none, _ =>
    Many.none
  | Many.more x xs, f =>
    (f x).union (bind (xs ()) f)

instance instMonadMany : Monad Many where
  pure := Many.one
  bind := Many.bind

-- how to get the implementation of `Functor` instance, or `Applicative` insatance?

-- The specific implementation cannot be known from this output message.
/-
Applicative.toFunctor
-/
#synth Functor Many

/-
unknown constant 'Many.map'
-/
#check Many.map

[Yaël Dillies]

Have you tried to #print the instance?

[Asei Inoue]

I don't know the instance name of Functor for Many

[Yaël Dillies]

That's why we have typeclass inference! Try #print show Functor Many by infer_instance

[Miyahara Kō]

No, try #synth Functor Many.

[Yaël Dillies]

That's what Asei tried above. It doesn't show you the body of the definition

[Asei Inoue]

Thank you! but I get an error

/-
unexpected token 'show'; expected 'axioms', 'eqns', 'equations', identifier or string literal
-/
#print show Functor Many by infer_instance

[Yaël Dillies]

Put brackets around? or do #print (inferInstance : Functor Many)

[Asei Inoue]

still erorr (I tried this in Lean 4 playground)

/-
unexpected token '('; expected 'axioms', 'eqns', 'equations', identifier or string literal
-/
#print (inferInstance : Functor Many)

[Asei Inoue]

oh no... This does not produce an error, but only useless output.

def instFunc : Functor Many := by infer_instance

/-
def instFunc.{u_1} : Functor Many :=
inferInstance
-/
#print instFunc

[Yaël Dillies]

Doesn't seem fantastic...

[Andrew Yang]

What info do you want to get? Can you click on Applicative.toFunctor to see the implicit arguments?

[Asei Inoue]

I want to get this information (which is an implementation of Functor class form Monad) automatically from Lean.

example (f : α → β) (x : Many α) : f <$> x = x.bind (Many.one ∘ f) := by rfl

[Andrew Yang]

Clicking on Applicative.toFunctor should point you to Monad.toApplicative, and going there you should see that the implementation is map f x := bind x (Function.comp pure f).

[Miyahara Kō]

Yaël Dillies said:

That's what Asei tried above. It doesn't show you the body of the definition

Sorry, try #whnf (inferInstance : Functor Many)!

[Miyahara Kō]

#whnf (inferInstance : Functor Many)
/-
{ map := fun {α β} f x ↦ x.bind (Many.one ∘ f), mapConst := fun {α β} ↦ (fun f x ↦ x.bind (Many.one ∘ f)) ∘ const β }
-/

[Asei Inoue]

@Pol'tta / Miyahara Kō Thank you!!

[Notification Bot]

Asei Inoue has marked this topic as resolved.

[Notification Bot]

Asei Inoue has marked this topic as unresolved.

[Asei Inoue]

why this does not work?

-- missing implementation info
/-
Applicative.mk
-/
#whnf (inferInstance : Applicative Many)

[Miyahara Kō]

This is because Applicative is an extended class.
To see the implementation of <*>, Try #whnf (inferInstance : Seq Many).

[Yaël Dillies]

I would really expect #print to be the tool to reach for when you want to know how something is defined.

[Eric Wieser]

pp.explicit true will make print check behave here

[Eric Wieser]

Or just click on inferInstance in the info view

[nesken7777]

I usually use #reduce instMonadMany.toSeq in this case, but this will show you the unfolded result up to Many.rec.

[Asei Inoue]

@Eric Wieser why #print (inferInstance : Functor Many) raise an error? (it says "unexpected token")

[Eric Wieser]

You meant #check

[Asei Inoue]

why this #print fails?

inductive Many (α : Type u) where
  | none : Many α
  | more : α → (Unit → Many α) → Many α

def Many.one (x : α) : Many α := Many.more x (fun () => Many.none)

def Many.union {α : Type u} : Many α → Many α → Many α
  | Many.none, ys => ys
  | Many.more x xs, ys => Many.more x (fun () => union (xs ()) ys)

def Many.bind : Many α → (α → Many β) → Many β
  | Many.none, _ =>
    Many.none
  | Many.more x xs, f =>
    (f x).union (bind (xs ()) f)

instance instMonadMany : Monad Many where
  pure := Many.one
  bind := Many.bind

-- pass!!
#check (inferInstance : Functor Many)

/-
unexpected token '('; expected 'axioms', 'eqns', 'equations', identifier or string literal
-/
#print (inferInstance : Functor Many)

[Eric Wieser]

Print expects a single name, not an expression

[Asei Inoue]

@Eric Wieser thanks!