Using Existentials in Inner Functions

[Kevin Meredith]

After reading this series, I thought of the following.

$scala

Welcome to Scala 2.12.0-M3 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_51).

Type in expressions for evaluation. Or try :help.

Given the two functions:

    scala> def f1[A](x: Option[A]): Option[A] = {

         |   def g(y: Option[_]): Option[_] = y

         |   g(x)

         | }

    <console>:13: error: type mismatch;

     found   : Option[_$2] where type _$2

     required: Option[A]

             g(x)

              ^

and

    scala> def f2[A](x: Option[A]): Option[A] = {

         |   def g(y: Option[_]) = y

         |   g(x)

         | }

    <console>:13: error: type mismatch;

     found   : Option[Any]

     required: Option[A]

             g(x)

              ^

My understanding is that the first function specifies a return type of `Option[A]`, but the usage of the 

existential, `Option[_]` means that we can't prove a returned `Option[A]`. 

Is that true? If it's a weak or unclear explanation, please provide an answer.

For the second case, why is `Option[Any]` inferred as the return type? Why wasn't it `Option[_]`?

[Erik Osheim]

So, as far as I understand it, _ means "there is some precise type
that exists but I can't name" whereas A gives it a name, and Any just
punts on the issue.

In your first example, there is no way to prove that the existential
type of the return value is related to the input value at all. To do
so would require paramterizing the method so you could mention the
same type twice by name.

In the second example, I think the reason there is that inference is
unlikely to want to infer an existential type. From the compiler's
point-of-view, it has an Option and no meaningful information about
its type parameter, so converting an existential to Any makes a
certain amount of sense. But that's just totally a guess about what's
going on there.

-- Erik

> --
> You received this message because you are subscribed to the Google Groups "Typelevel Users & Development List" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to typelevel+...@googlegroups.com.
> To post to this group, send email to type...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/typelevel/df0ea125-9cc7-412f-ad85-b973e0e4da5b%40googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Robert Norris]

On Jan 25, 2016, at 2:22 PM, Erik Osheim <er...@plastic-idolatry.com> wrote:

> In the second example, I think the reason there is that inference is
> unlikely to want to infer an existential type.

Note that invariant and contravariant holes remain existential (but distinct; input and output types are not the same).

scala> def g(x: List[_]) = x
g: (x: List[_])List[Any]

scala> def g(x: Set[_]) = x
g: (x: Set[_])scala.collection.immutable.Set[_]

scala> def g(x: Function1[_, _]) = x
g: (x: Function1[_, _])Function1[_, Any]