Add support for lazy (explicit|implicit) parameters

[milessabin]

#1998 makes implicit parameters consistent with explicit parameters by allowing implicit parameters to also be by-name. This change was motivated in Dotty (and work in progress on Scala 2) to support the same sort of type level programming use cases which are currently enabled by shapeless's Lazy type.

However, the bynamity of a parameter prevents it from being stable which means that the following,

trait Foo {
  type Out
  def out: Out
}

object Test {
  implicit def bar(implicit foo: => Foo): foo.Out = foo.out
}

doesn't compile (either in Dotty or Scala 2 with by-name implicit support) because the by-name argument foo is not stable,

lazy-implicits-7.scala:12: error: stable identifier required, but foo found.
  implicit def bar(implicit foo: => Foo): foo.Out = foo.out
                                          ^
one error found

This pattern is very important in implicit-based type level programming, so this would be a disappointing limitation. By contrast, shapeless's Lazy captures the value in a stable context and hence supports the following with vanilla Scala 2,

implicit def bar(implicit foo: Lazy[Foo]): foo.value.Out = foo.value.out

Currently the following is a workaround with by-name implicits which compiles both on my Scala 2 branch and with Dotty,

trait Foo {
  type Out
  def out: Out
}

object Foo {
  type Aux[Out0] = Foo { type Out = Out0 }
}

object Test {
  implicit def bar[T](implicit foo: => Foo.Aux[T]): T = foo.value
}

ie. we use the Aux pattern to avoid the need for a stable value. This is clumsy however, and the additional type parameter (which typically must be inferred) can make it hard to express methods which also require explicit type arguments.

So, whilst by name implicits get us close be being able to replace shapeless's Lazy macro, it's not quite there.

It was proposed in the discussion on #1998 to use the lazy modifier on method parameters to express by-need (ie. at most once) evaluation semantics. If such parameters could participate in stable paths (at least modulo the restrictions described here and the issues enumerated in the Scala 2 ticket) then a lazy implicit parameter would more or less exactly replicate the semantics of shapeless's Lazy.

[ghost]

Hey, Miles, what is the status of this issue?

[milessabin]

No recent progress as far as I'm aware. I'll come back to it when I have time.

[ghost]

I may have some time to contribute (actually, I am writing library code where the feature would be very useful). But I'm not sure if I'm the right kind of person to contribute (it has been some time since I've been involved in similar stuff).

[odersky]

I have a potential fix for this. The program can be compiled if we change the definition of bar to

implicit def bar(implicit foo: => Foo & Singleton): foo.Out = foo.out

See #3773. WDYT?

[ghost]

does "foo: => Foo & Singleton" indeed mean that foo is evaluated by need and at most once?
that would be great indeed

[odersky]

does "foo: => Foo & Singleton" indeed mean that foo is evaluated by need and at most once?
that would be great indeed

No, it just means that the actual argument to foo is required to be stable. E.g. you can't pass a var. Note that a notion of "eval at most once" would not help with dependent types. #50 and #1050 show that taking dependent types of lazy vals is in general unsound - we need to guarantee that the argument is evaluated.

So it seems this would not in general solve the problem of lazy implicits because the inferred arguments to lazy implicits are most often not stable. It actually looks quite hard to find a good solution that maintains soundness.

[odersky]

In fact #3005 does not seem to be a useful fix for the problem. And I don't know what a sound solution would look like. I am leaving this open for a while in case others have ideas, but if not we will close with stat:revisit.

[milessabin]

@odersky I can't quite tell from the discussion on #50 what the current consensus on lazy vals in paths is. Are they ever allowed? If so, under what circumstances?

[odersky]

@milessabin Lazy vals are allowed in paths, but they must be final and their type must be a concrete class. Here are some test cases. The code in dotc is in class CheckRealizable.

class C { type T }

class Test {

  type D <: C

  lazy val a: C = ???
  final lazy val b: C = ???
  val c: D = ???
  final lazy val d: D = ???

  val x1: a.T = ???  // error: not a legal path, since a is lazy & non-final
  val x2: b.T = ???  // OK, b is lazy but concrete
  val x3: c.T = ???  // OK, c is abstract but strict
  val x4: d.T = ???  // error: not a legal path since d is abstract and lazy

}

So on third thought, yes, this could actually still allow many important use cases.

[milessabin]

Suppose we used the same criteria for lazy parameters? They can be viewed as effectively final and we can restrict types to those that are concrete in the same sense as class C.

[Blaisorblade]

@milessabin Was there any change here? I'm studying realizability right now, so this is good time to discuss it.

Suppose we used the same criteria for lazy parameters? They can be viewed as effectively final and we can restrict types to those that are concrete in the same sense as class C.

That currently makes sense to me.

[Blaisorblade]

BTW, I think there are two questions here:

• support lazy params at all (add lazy parameters scala/bug#240), which has also other use cases;
• make them stable. At first sight, it seems this is done by not changing SymDenotations.isEffectivelyFinal or anything in CheckRealizable, though this needs testing — it's felicitous that the proposed logic is so close to the existing one that it needs no changes.

Beware I need to talk again to somebody who understands realizability here (that is, @odersky).

[milessabin]

I've not done any more on this recently. I'd be very happy to pick this up in Scala if Dotty decides in favour of supporting lazy parameters.

[dcsobral]

Is there some sort of SIP for this in Dotty?

[milessabin]

The way we left it was that @odersky needed to rule on the stability issue.