But as the others pointed out, we’re not extending anything so the extension keyword is very confusing.
Why not do the (imho) obvious? We’re defining methods / functions with implicit type- or value-parameters. The mechanic for implicit parameters are givens in Scala. So why not use given as keyword? Exactly like the using and with examples above.
The following syntax is illegal at the moment:
given [A]:
def foo(a: A) = ???
So this could be used, could it?
This would also extend in a very natural way to the version with “implicit parameters” as this is almost already what given (a: A) means, namely, “Define an implicit A parameter in scope”. Only that in this construct the given would be followed by a body with declarations and not an = sign.
Besides the syntax issue I would welcome this feature. It feels very intuitive and natural as Scala has implicit parameter lists anyway since forever. So this feature seems not surprising. (Especially when written with the usual syntax to declare implicit stuff in scope)^^.
The implementation under the hood can of course look however this is done best. No clue about that part. But the implementation would be hidden anyway, so this is not an issue.
Thanks for the proposal!
Maybe there is even more to copy form LEAN? At a quick peek that language looks very nice and clean.
Can someone please tell me what problem we are trying to solve?
What is wrong with repeating some type parameters? How many parameters are being repeated how often for how many people? And when it does happen what is wrong with using a plain old class?
If you make a class, you have to make an instance of that class to invoke a method, giving it a useless name in the process
class Section[A]
def foo(x: A): Unit = ???
new Section().foo(5)
vs
with [A]:
def foo(x: A): Unit = ???
foo(5)
I agree that the motivation is weak, particularly for type parameters. There’s a reasonable argument for using parameters since they can get quite repetitive and they exist to make call sites less boilerplate-y, so why not have declaration sites be less boilerplate-y too?