I have been quite intrigued by Lean 4’s sections. They allow to write a list of type parameters once and then all definitions referring to the declared types are implicitly augmented with additional type parameters.
Can we add similar functionality to Scala? The most logical way to do so would be by way of generalizing the extension mechanism. So far, an extension header consists of
- precisely one value parameter (the prefix)
- zero or one type parameter clauses
- zero or more using clauses
Example:
extension[X](xs: List[X])(using Ctx[X])
def combine(ys: List[X]) = ...
def extract = ...
The defined extension methods can be invoked like this
as.combine(bs)
as.extract
or like this
combine(as)(bs)
extract(as)
Now, how about we make the value parameter of an extension header also optional? I.e: An extension header consists of
- optionally, a value parameter (the prefix)
- … (as before)
So what would an extension clause without extended parameter mean? First, all methods in it must be called in prefix form, as in the second example above, since there is no separate object on which they are defined.
Then, every type parameter in the extension header that gets referred from the signature of an extension method gets added as a type parameter to the method. Example:
extension [A, B]
def f[C](x: A): C = ...
def g(y: B): B = ...
gets expanded to
def f[A][C](x: A): C = ...
def f[B](y: B): B = ...
Note this is more restrictive than Lean’s sections, since we only add type parameters referred to from the signature, not parameters referred to from the body. If a type in the body refers to an extension type parameter that is not also referred to from the signature, this would be an error.,
Passing explicit type arguments to these methods is a bit problematic since we have to do an expansion in our head to figure out what type parameters a method gets in what order. I propose to avoid those mental acrobatics and require that all added type parameters of these extension methods are instantiated by name. I.e. f[SomeA](a) would be illegal. You’d have to write f[A = SomeA](a).
Moving on to using clauses, the idea would be that every using clause in an extension header is added as a using clause to all methods defined in the extension. The using clause appears in its natural place, before all other parameters of the method. Example:
extension (using c: Context)
def f(x: c.A) = ...
def g[T <: c.B](x: T) =
gets expanded to
def f(using c: Context)(x: c.A) = ...
def g(using c: Context)[T <: c.B](x: T) = ...
Again we are different from Lean in that using clauses get added unconditionally, not just when they are referred to from the body of a method. This is done in the interest of binary stability. We do not want an implementation detail of a method to influence its binary signature.
That’s it. It’s syntactically a small change (just make one element of extensions optional). Its main benefit is DRYness. It’s a good tool to avoid repetitive type parameters and using clauses in method signatures without forcing methods to be factored out into separate objects.
I’d be interested to get your feedback on this.
