class dot notation

Stream: lean4

[Chris B]

I know you couldn't do this in Lean 3 (at least) names were resolved before typeclasses, but is there a way to use dot notation or some shorthand with classes in Lean 4? Example:

class Profile (A : Type u) where
  name : A → String
  email : A → String

def Profile.allInfo (A : Type u) [Profile A] (user : A) : String := user.name ++ user.email

[Evgeniy Kuznetsov]

I recently discovered that chained dot notation application of a class argument requires extra parentheses. Don't sure whether it's expected or not.

class Foo (f: Type)
class Bar (f: Type)
class Bar' (f: Type) extends Bar f

instance Foo.toBar' [self: Foo f]: Bar' f := {}

/- produces error
function expected at
  Foo.toBar'
term has type
  Bar' ?m.59 -/
example [self: Foo f]: True :=
  let i := self.toBar'.toBar
  trivial

-- it works
example [self: Foo f]: True :=
  let i := (self.toBar').toBar
  trivial

[Chris B]

That's interesting. I'm not sure whether the elaborator handles that case differently (where self is the instance rather than the element that implements the class) but that is good data, thanks.

[Chris B]

@Leonardo de Moura

The example in the first message shows the dot notation question I brought up on Wednesday; I'd be interested to get your thoughts if you have a moment later.

[Leonardo de Moura]

@Chris B Thanks for pointing it out. It is now clear to me what you meant last Wednesday. The example above does not work in Lean 4. I incorrectly assumed you wanted to use dot notation as follows. AFAIR, the following does not work in Lean 3.

def Profile.allInfo (A : Type u) [inst : Profile A] (user : A) : String := inst.name user ++ inst.email user

The feature you suggested sounds interesting, it seems related to a feature that @Sebastian Ullrich suggested before. In his proposal, we should allow users to use polymorphic operations such as toString x with dot notation, that is, we would be able to write x.toString.
However, in his proposal, we would have to export the Profile fields.

export Profile (name email)

It is clear to us how to support Sebastian's proposal. However, I suspect you would not want to have name in the top-level namespace. What kind of name resolution do you have in mind for terms such as user.name and user.email? Would we just infer user's type ty and inspect local instances that depend on ty? What should we do if there is more than one local instance?

[Chris B]

Rust has two behaviors. If x.y refers to both an associated method y AND one or more trait (typeclass) methods in scope named y, the associated method always takes priority, and no error is thrown.

trait A {
    fn message(&self) -> String;
}

trait B {
    fn message(&self) -> String;
}

struct Concrete;

impl Concrete {
    fn message(&self) -> String {
        "From the associated method".to_string()
    }
}

impl A for Concrete {
    fn message(&self) -> String {
        "From trait A".to_string()
    }
}

impl B for Concrete {
    fn message(&self) -> String {
        "From trait B".to_string()
    }
}

fn main() {
    let x = Concrete;

    // Prints "From the associated method"
    // The associated method takes priority over any trait
    // methods, so there's no error and no special syntax.
    println!("{}", x.message());


    // Prints "From trait A"; the invocation is disambiguated with "Fully Qualified Syntax".
    println!("{}", A::message(&x));
}

If x.y refers only to a trait method, but there are multiple trait methods in scope x.y, you get an error requiring you to disambiguate with the fully qualified syntax:

trait A {
    fn message(&self) -> String;
}

trait B {
    fn message(&self) -> String;
}

struct Concrete;

impl A for Concrete {
    fn message(&self) -> String {
        "From trait A".to_string()
    }
}

impl B for Concrete {
    fn message(&self) -> String {
        "From trait B".to_string()
    }
}

fn main() {
    let x = Concrete;

    // Error:
    // multiple applicable items in scope
    // multiple `message` found
    // main.rs(280, 5): candidate #1 is defined in an impl of the trait `A` for the type `Concrete`
    // main.rs(286, 5): candidate #2 is defined in an impl of the trait `B` for the type `Concrete`
    println!("{}", x.message());


    // Can disambiguate again using the fully qualified syntax.
    println!("{}", A::message(&x));
}

Since Lean uses whitespace for function application, I think the fallback could just be to require users to expand x.method into class.method x to disambiguate. People might have strong opinions about whether projections should trump typeclass methods. For non-projection clashes (like Nat.add), my perception is that most of the time there's both a Type.method and a Class.method, users would want the typeclass method to take precedence.

I wasn't able to find much information about the ML strategy that was mentioned, I'll ask for more details and do some reading.

[Mario Carneiro]

For non-projection clashes (like Nat.add), my perception is that most of the time there's both a Type.method and a Class.method, users would want the typeclass method to take precedence.

I would say it is the other way around: the namespaced method should always take priority over a typeclass method

[Mario Carneiro]

this might be affected by the lean 3 behavior (where typeclass methods never use dot notation), but the rust behavior also seems to make sense to me

[Mario Carneiro]

I'm a little dubious about sebastian's idea to open typeclasses in order to get dot notation. (1) typeclasses are very rarely opened currently, and the namespaces are generally not curated expecting the typeclasses to be open, (2) dot notation currently explicitly does not depend on things being open, and this is one of the main reasons it is used so extensively, and (3) there are a lot of typeclasses so this is a lot of busywork. (It's busywork in rust too.)

[Chris B]

Mario Carneiro said:

For non-projection clashes (like Nat.add), my perception is that most of the time there's both a Type.method and a Class.method, users would want the typeclass method to take precedence.

I would say it is the other way around: the namespaced method should always take priority over a typeclass method

I'll defer to your experience on this, but I feel like most of the time I write an explicit method like SomeType.toString when there's also an instance of ToString, it's because the namespaced method is recursive or something and it's ultimately intended define the typeclass version . Maybe this will be less of a thing now that there's let rec aux.

[Mario Carneiro]

I suppose that's true; if this became the new standard then I imagine either we would rename those methods to avoid them getting accidentally called, or alternatively if they have the right type and the instance just defers to it then there is no harm in calling the function directly and save yourself one step of inlining

[James Gallicchio]

after letting this simmer for a bit, here are some thoughts

I feel like I'm too scared to export typeclasses I make because I don't want to pollute the namespace, but I do want the functions exported in (almost?) all of the contexts I declare class instances. for example, if I declare an instance : ToString X in namespace X then I would sort of like it to also generate a declaration toString : X -> String for stuff like dot notation

It's fine (read: annoying) doing this manually for small typeclasses, but I am working on some larger typeclasses with potentially dozens of members, being instantiated largely with default values, that I would also like to export into namespaces where instances are declared.

Auto-generating new declarations feels like a bad approach. It would make lots more jumping around to find the "actual" definitions of functions, it adds lots of clutter to namespaces, and in a future world where we have auto-completion for this kind of thing, I'd rather it show what typeclass each option is being provided by instead of just a monstrous mound of "X.something"s

But I think it makes sense as a mental model for the resolution rules? Given X.foo, we look in namespace X for functions foo, but also for instances with member foo. Note that this isn't typeclass resolution, it's fully namespace driven. The member just happens to also be available for typeclass resolution.

Perhaps we just add a way to "include" all of the members of a structure within a namespace, sorta like the ML include behavior.

def X := SomeType

namespace X

instance : Foo X where
  foo := blah

include instFooX

end X

#check (... : X).foo

but instead of literally copying all of the definitions, it just changes namespace resolution rules to include those members.