Taking extensions further

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 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.

1 Like

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?

11 Likes

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?

1 Like

It would be interesting to get some data on cases where this proposal would make a difference enough to justify the costs.

IMO there are other features that are compatible with Scala (syntax and spirit) and might be worth considering, for example:

  1. Handling of M Unit values in do expressions:
def run = for
  printLine("Hello! What is your name?")
  n <- readLine
  printLine("Hello, " + n + ", good to meet you!")
  1. Automatic insertion of M Unit when needed:
def read(log: Bool) = for
  name <- readLine
  if log then 
    printLine(s"read: $name")
  yield name