Why Dot notation doesn't work for instance methods?

Stream: new members

[Luis Enrique Muñoz Martín]

Hi! In the following code:

structure Foo

class Bar (α : Type) where
    bar (a : α) : String

instance : Bar Foo where
   bar a := "bar"

def callBar (f : Foo) : String := Bar.bar f  --Compiles
def callBar' (f : Foo) : String := f.bar -- does not compile

Why the dot notation doesn't work in this context? Am I missing something or exists a workaround? thanks

[Julian Berman]

Were you meaning to create two separate threads in Zulip, or are these meant to be the same question essentially?

[Julian Berman]

The other one being #new members > Why Lean don't allow to call this instance method?

[Julian Berman]

Also just to be sure -- what's your background, or more specifically, is it in some non-functional-programming programming language?

[Julian Berman]

In particular, "class" and "instance" in Lean mean term#class and term#instance -- which is quite different from what that means in OOP languages.

[Julian Berman]

Oh. Did we lose the glossary linkifier. I guess so.

[Kyle Miller]

The proximal reason it doesn't work is that f.bar needs to know to look for Bar.bar and then know to feed f as the α argument. I think there's an RFC that outlines an idea for how to do this, but I couldn't find it.

Instead of OOP "class", you should think of these as being generic functions — they're global functions that dispatch on the types of the arguments.

Lots of times, you'll see the export command in conjunction with a class to make one of the functions available outside the class's namespace. For example, the toString function has been exported in this way from the docs#ToString class. Here's how it looks for bar:

class Bar (α : Type) where
    bar (a : α) : String

export Bar (bar)

instance : Bar Foo where
   bar a := "bar"

def callBar (f : Foo) : String := bar f

[Luis Enrique Muñoz Martín]

Hi @Julian Berman , yeah, I wanted to create two different threads because although the example is the same, the question, was pointing different aspects.

My background comes from Rust and a bit of Haskell, although I probably made a mess defining the question above :pray:

Basically, my mind is trying to figure out how I can do in Lean4 the things I was able to do in Rust. i.e. I'm still dealing with how Rust's Associated Types can be represented in Lean4 correctly, and similar things. That's why most questions I've been doing recently are more related to types than functional programming itself.

My main target is to evaluate how interesting it would be to use Lean4 for smart contracts because it seems like this language has all features required for it.