Dot notation with type classes

Stream: new members

[misterdrgn]

Hi all. I've been enjoying playing around with this language. One thing I appreciate, which you wouldn't necessarily expect, is that the language supports dot notation for calling functions. However, as far as I can tell, two of Lean's nice language features, type classes and dot notation, do not mix. Here's a minimal example.

set_option autoImplicit true

class Doubleable (α : Type) where
  doubled: α → α

def Doubleable.quadruple [Doubleable α] (value: α) : α :=
  value |> doubled |> doubled

instance : Doubleable Nat where
  doubled := (· * 2)

-- This works.
#eval Doubleable.quadruple 4

-- However, calling quadruple via dot notation does not.
#eval (4: Nat).quadruple

Of course the final line fails because quadruple isn't defined in the Nat namespace. However, it seems interesting that functions can be inherited from another namespace when you extend a structure, but not when you make an instance of a type class. (EDIT: Maybe it's just that when A extends B, A can be coerced to B for free, so any function defined in B's namespace can be called on values of type A via dot notation.)

Could anyone please tell me if I'm missing a viable approach for using dot notation with generic functions whose types are constrained by type classes?

Thanks!

[Niels Voss]

There was some discussion about this earlier related to Digraphs in this thread: #Is there code for X? > Weak components of a digraph, where the goal was to develop a HasAdj typeclass. If I understand correctly, this is currently not possible, but it might become possible in the future, see lean4#6267. Even with this PR, I think you still can't directly use dot notation from typeclasses (maybe because doing so would be really bad for performance if every time you wrote x.y it had to resolve every possible typeclass for x?)

Do you have a specific use case in mind? It might be that there's a workaround for your particular use case that doesn't require the full generality of the unreleased dotParam widget.

[misterdrgn]

Thanks for the response. I don’t have a particular use case, I’m more just curious about how fully Lean supports dot notation, given that type classes are obviously a core feature of the language.

I find it interesting exploring the parallels between Lean and the Swift language, despite the languages having massively different primary purposes of course (I’ve been using Swift for CS research). Both languages allow you to essentially use types as namespaces and support dot notation for functions defined in a type’s namespace. But in Swift you can define a method for a protocol (protocols are like type classes, but without HKTs), and then you can call it on values of any type that implements that protocol via dot notation.

The PR you linked would allow the same in Lean, with a key extra step—you have to add the function to the namespace of a type that instantiates the type class manually before you can call it via dot notation. So this would require more forethought and planning before you get the convenience of dot notation.

Unless that extra step could be automated via metaprogramming, which is a part of Lean I’ve been meaning to explore.

[Kyle Miller]

I think a key difference between typeclasses and Swift protocols is that typeclasses are more like a way to define Lisp generic functions (which dispatch on all arguments), but Swift protocols have a distinguished receiver.

Lean typeclasses do not need to be "for" any particular type. In docs#Membership for example, is it "for" the alpha or the gamma type argument? I might say 'neither', though gamma is defensible.

The way Lean's dot notation works uses a fairly simple rule (at least to first approximation). If you write x.f, it elaborates x to see it has type T ..., then it looks for T.f, and then it looks for an argument to T.f whose type is of the form T .... (Complications: can try unfolding T ... to T' ... and look for T'.f, it can make use of aliases, it can try unfolding arguments when looking for matches, and it can even try coercing T.f to a function. Also, if x is a structure, it can also walk up the parent hierarchy an insert toParent coercions.)

So, when it comes to typeclasses and dot notation, here are some problems:

• Typeclasses might be called typeclasses, but they're not for any particular type. (There might not even be any types! That's very rare though.)
• The fields of a typeclass might not obviously mention the type. (It's not like Swift where every protocol member has an implicit "self" argument. There is an implicit "self" argument for typeclass fields in Lean, but it's for the typeclass instance itself.) So, there may be no way to apply the function.

Possibly we could have a way to annotate an instance (for arguments sake, suppose you add the attribute @[protocol]), which checks that the typeclass is protocol-like and registers the instance as being a way to resolve dot notation for that class for the specified type argument. Or, perhaps the class itself can be registered using @[protocol] and whenever an instance is made it registers dot notation. Something that would need to be answered here is exactly when in the dot notation resolution would protocol methods be considered. Also, for multi-parameter typeclasses, how you can specify which argument is the receiver. (One might also take the convention that the first explicit argument should be the receiver universally for protocols.)

Niels linked to one PR (lean4#6267, the dotParam widget). Another is lean4#6393, for permanently exporting namespaces, which with dotParam would be a way to add "mixins" to a type (you would define an instance for a class and then export its fields into the type's namespace). These are ways to solve the more general problem "how do I use generic functions using dot notation". I think the @[protocol] idea could be implemented using these primitives, but you would need to manually add in dotParam widgets.

[misterdrgn]

@Kyle Miller Thanks for the long response. I take your point about the ambiguity in which type to treat as the “receiver” of a Lean type class’s generic functions. I do think the ‘dotParam’ keyword in the first PR does a decent job of resolving this ambiguity. In this case, the only issue is needing to export each generic function in the type class’s namespace into a type’s namespace before you can use dot notation with it. Maybe that other PR addresses that by allowing you to export the type class’s entire namespace all at once, but I wasn’t quite sure about that.

Are these PRs on their way into Lean’s main branch, or are they still being considered?

Thanks for the help.