dot notation for class methods?

Stream: lean4

[Yuri de Wit]

Consider the following:

class A (α : Type) where
  a : Unit -> α

def a1 [A α] : α := A.a () -- ok
def a2 [A α] : α := .a () -- error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant α

Should the dot notation feature also resolve methods in scope for the result type (in this case, methods from A α) automatically?

[Sebastian Ullrich]

How would you define "methods in scope"?

[Yuri de Wit]

I am out of my depth here, but my initial intuition would be to consider only the classes explicitly declared for the return type above.

[Andrés Goens]

@Yuri de Wit so you want it to automatically open the namespace? wouldn't that be a bit going against the point of namespaces?

[Andrés Goens]

you can also open the namespace and it will work:

open A

def a1 [A α] : α := A.a () -- ok
def a2 [A α] : α := a () -- ok

[Henrik Böving]

No he wants to extend dot notation to respect type classes as well, note that he is doing .a instead of a. We already support this if we have a term: .func a b c and the expected type is known to be a certain T and T.func exists Lean will intelligently translate the term into T.func a b c. The exact point of this notation is that you do not open the namespace but that type inference figures the namespace out for you.

The thing that is at question is what heuristic to use to also capture type classes on T instead of just functions directly declared on T

[Yuri de Wit]

@Andrés Goens yes, exactly what @Henrik Böving described.

It is an extra convenience, although I am not sure about the underlying implications. So just a thought.

[Sébastien Michelland]

Note that if A is long and you want to avoid typing it, you can usually use dot-notation on the instance itself:

class LongClassName (α : Type) where
  a : Unit -> α

def a1 [i: LongClassName α] : α := i.a ()

[Andrés Goens]

Ahh, I see. I guess in a lot of cases it coincides, right? At least when I've implemented instances like ToString I do so in that namespace (e.g. A.toString), but for derived instances or examples like yours it seems convienient

[Henrik Böving]

Given the previous discussion in #std4 about having a rust style stream/iterator API I'd like to bring this point up again. Rust does have support for this type of syntax as well and that is what enables it to define its stream API in the way it does. As I see it the rust trait system comes close to our type class system so why can we not have dot notation for type class instances as proposed here?

Given that both the iterator API and the dot notation of type class methods would follow the default design heuristic of: If Rust does it we can do it.

[Mario Carneiro]

One issue with implementing this a la rust is that unlike in rust, typeclass methods don't really have a distinguished "receiver" argument. In fact in the example it's not even an argument being used for the lookup! (You can argue that there is a distinguished "co-receiver" though, since functions only have one return value.) But for a multi-arg function with a multi-type typeclass it's not really clear what to dispatch on.

[Alex Keizer]

How does this work with regular dot notation, there is no distinguished receiver there either, no? IIRC, we take the first argument of the namespace type as receiver, maybe we do something similar here; the first (explicit) type argument to a typeclass can be it's receiver

[Henrik Böving]

Mario Carneiro said:

One issue with implementing this a la rust is that unlike in rust, typeclass methods don't really have a distinguished "receiver" argument. In fact in the example it's not even an argument being used for the lookup! (You can argue that there is a distinguished "co-receiver" though, since functions only have one return value.) But for a multi-arg function with a multi-type typeclass it's not really clear what to dispatch on.

That's a fair point but I'd say we can at least implement this for single argument type classes? (or even funkier: type classes that only have 1 parameter that is not an out param?) in which case (given that we know the type of the thing that is getting "dotted" of course) we should be able to come up with a correct TC synthesis query? Another interesting question might be how to deal with type classes like functor? So for example when I have x : Array a and I do x.map ... the query would have to..I guess speculatively try to find instances for just Array? That does seem kinda hacky as well though so maybe it would be better to limit to just: Type classes that only have a single not out param.

[James Gallicchio]

might have already suggested this, but I think I'd prefer if there were an annotation to register these dot notation extensions and lets you specify the argument to dot on. something like

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  @[dotExt _ α β f c => c]
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α

taking inspiration from termination_by clauses

[Henrik Böving]

What does the underscore do here?

[James Gallicchio]

stand-in for map, but now that I think about it, if we were using the termination_by syntax you could write this as @[dotExt c => c] since the parameters are added right to left

[Henrik Böving]

Well either way in this syntax lean should know that it is map that you are referring to since you are tagging it directly. However putting arguments like this is currently not possible iirc?

[James Gallicchio]

Noted. A non-annotation command would also be fine:

addDotExtension @Functor.map α β f c => c

[James Gallicchio]

I also think having a command to register each function is very reasonable, since this is a feature that is primarily intended for Std and other libraries to make use of (introducing class methods to the dot namespace is an advanced feature, even if the resulting extended dot notation is a beginner feature)