I like the proposal’s spirit!
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 given
s 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.