This is a follow up on a brief discussion at https://github.com/lampepfl/dotty-feature-requests/issues/83.
Implicit function types are a very interesting way to express dependencies and provide language support for a concept of a type level set of dependencies where we can seamlessly reorder or partially eliminate dependencies. However, the way the compiler attempts to “eagerly” evaluate implicit function types can make them unergonomic to use.
For example, a naive encoding of ZIO in Dotty could be:
type ZIO[-R, +E, +A] = (given R) => Either[E, A]
We could then write:
val x: ZIO[String, Nothing, Int] = ???
However, if we then want to use this like a normal value we need explicit type ascription with each assignment to avoid the compiler attempting to immediately resolve the implicit.
val y: ZIO[String, Nothing, Int] = x // okay
val z = x // does not compile: no implicit argument of type String was found
Is there a way that we could defer trying to evaluate the implicit function and just carry the dependency along with us?
The challenge seems to be developing a set of rules for when the compiler should attempt to resolve the implicit versus carrying it along as an implicit function type.
It seems like we could have a rule along the lines of “don’t require the implicit if there is no appropriate implicit value in scope and the code type checks appropriately with maintaining the implicit function type”. This would I think be pretty seamless, though it would create some risk of accidentally resolving the implicit early if there was an unanticipated implicit in scope.
An alternative would be to require some action to more explicitly resolve the implicit, like a type ascription to a non-implicit value or passing it to a function that demands the result type instead of an implicit function type.
My concern is that the most interesting applications of implicit function types involve dependencies that we want to carry along for a long time, possibly until the very end of our program, so if we require a type ascription on every statement to prevent us from doing that it is going to make them unattractive for this use case they are very well suited to.
Thank you for your consideration.