passing instances explicitly

Stream: lean4

[Petar Maymounkov]

How can I pass instances explicitly to a function f as below?

class Chromatic (α : Type) where -- something that has color
  chroma : String

instance {α : Type} : Chromatic α where -- everything is green
  chroma := "green"

def f [χ : Chromatic α] : String := χ.chroma

#eval f -- does not work

[Stuart Geipel]

You can use @ to pass in hidden parameters such as this one.
I only got it working when saving it to a variable though:

def foo := @f (Chromatic Nat)

#eval @f (Chromatic Nat) -- does not work
#eval foo -- does work

[Petar Maymounkov]

That's puzzling. I wonder what the rationale is. A related question. I would have expected this to work:

def f2 [Chromatic α] : String := chroma

I have seen this pattern in the implementation of Monad. However in this case here, the compiler returns the function chroma (which requires a self parameter), rather than the value that chroma returns.

[Henrik Böving]

Petar Maymounkov said:

How can I pass instances explicitly to a function f as below?

class Chromatic (α : Type) where -- something that has color
  chroma : String

instance {α : Type} : Chromatic α where -- everything is green
  chroma := "green"

def f [χ : Chromatic α] : String := χ.chroma

#eval f -- does not work

The reason this does not work is because your function signature is badly formed for type inference. if you just call it like that the only thing Lean will ever be able to infere is that it returns a String, it will never be able to make statements about the alpha parameter and thus also not about the type class instance. What you actually want to write here is:

def f (α : Type) [χ : Chromatic α] : String := χ.chroma

#eval f Nat

Stuart Geipel said:

You can use @ to pass in hidden parameters such as this one.
I only got it working when saving it to a variable though:

def foo := @f (Chromatic Nat)

#eval @f (Chromatic Nat) -- does not work
#eval foo -- does work

Your approach is doing something bad if you #check f You will see that it takes at first the type parameter, then the instance as an implicit argument which now both become explicit thanks to the @f so what you are passing is Chromatic Nat as type parameter for alpha Lean will end up inferring that you actually wanted to write this in your def:

def foo : [χ : Chromatic (Chromatic Nat)] → String := @f (Chromatic Nat)

by use of the implicit lambda feature. It is however of course perfectly possible to call this function since there is a Chromatic instance for Chromatic Nat that can be automatically inferred.

On the other side your direct evaluation attempt is not hidden behind a def or w/e so it will not do the implicit lambda but leave the now explicit type class argument explicit so your code does not end up being executable since it is still missing a parameter. What you would've wanted to write in this case is something like:

#eval @f Nat _

or alternatively for more clarity

#eval @f Nat inferInstance

Petar Maymounkov said:

That's puzzling. I wonder what the rationale is. A related question. I would have expected this to work:

def f2 [Chromatic α] : String := chroma

I have seen this pattern in the implementation of Monad. However in this case here, the compiler returns the function chroma (which requires a self parameter), rather than the value that chroma returns.

This does not end up working out because of the same type inference issue as your original definition. The Monad definitions usually contain the generic m type in its return type so it can trivially infere what is being referred to while here it again can only know that you want a String but it has no clue what chroma instance you want to base this on. However Lean is actually smart enough to notice that you made this mistake on its own as you can see from the error message it provides if you add the correct export annotation for this to work out in the first place:

class Chromatic (α : Type) where -- something that has color
  chroma : String
export Chromatic (chroma)

instance {α : Type} : Chromatic α where -- everything is green
  chroma := "green"

def f2 [Chromatic α] : String := chroma

gives:

type mismatch
  chroma
has type
  (α : Type) → [self : Chromatic α] → String : Type 1
but is expected to have type
  String : Type

as you can see Lean was smart enough on its own to notice that it won't be able to infere the alpha type with the way that chroma is defined and decided to add it as an explicit argument for when you have to call chroma (note that it hides this from you for when you are defining the Chromatic instance because there it has enough information (namely the instance type itself) to know what type you are asking about)

So if we just pass the type explicitly to chroma now:

class Chromatic (α : Type) where -- something that has color
  chroma : String
export Chromatic (chroma)

instance {α : Type} : Chromatic α where -- everything is green
  chroma := "green"

def f2 [Chromatic α] : String := chroma α

This too works.

[Petar Maymounkov]

Wow. What a clear and comprehesnive answer. Thank you @Henrik Böving