Scala lists with existential types: `map{ case t => ... }` works, `map{ t => ... }` doesn't?

Question

Suppose that we have defined an existential type:

type T = (X => X, X) forSome { type X }

and then defined a list of type List[T]:

val list = List[T](
  ((x: Int) => x * x, 42),
  ((_: String).toUpperCase, "foo")
)

It is well known [1], [2] that the following attempt to map does not work:

list.map{ x => x._1(x._2) }

But then, why does the following work?:

list.map{ case x => x._1(x._2) }

Note that answers to both linked questions assumed that a type variable is required in the pattern matching, but it also works without the type variable. The emphasis of the question is more on Why does the { case x => ... } work?.

Football

Answer 1

(My own attempt to answer the question; Should be not too wrong, but maybe a bit superficial.)

---

First, observe that

list.map{ x => x._1(x._2) }
list.map{ case x => x._1(x._2) }

is essentially the same as

list map f1
list map f2

with

val f1: T => Any = t => t._1(t._2)
val f2: T => Any = _ match {
  case q => q._1(q._2)
}

Indeed, compilation of f1 fails, whereas f2 succeeds.

We can see why the compilation of f1 has to fail:

1. t is of type (X => X, X) forSome { type X }
2. Therefore, the first component t._1 is inferred to have the type (X => X) forSome { type X }.
3. Likewise, the second component t._2 is inferred to have the type X forSome { type X }, which is just Any.
4. We cannot apply an (X => X) forSome { type X } to Any, because it actually could turn out to be (SuperSpecialType => SuperSpecialType) for some SuperSpecialType.

Therefore, compilation of f1 should fail, and it indeed does fail.

---

To see why f2 compiles successfully, one can look at the output of the typechecker. If we save this as someFile.scala:

class O {
  type T = (X => X, X) forSome { type X }

  def f2: T => Any = t => t match {
    case q => q._1(q._2)
  }

  def f2_explicit_func_arg: T => Any = t => t match {
    case q => {
      val f = q._1
      val x = q._2
      f(x)
    }
  }
}

and then generate the output of the typechecker with

$ scalac -Xprint:typer someFile.scala 

we obtain essentially (with some noise removed):

class O extends scala.AnyRef {
  type T = (X => X, X) forSome { type X };
  def f2: O.this.T => Any = ((t: O.this.T) => t match {
    case (q @ _) => q._1.apply(q._2)
  });
  def f2_explicit_func_arg: O.this.T => Any = ((t: O.this.T) => t match {
    case (q @ _) => {
      val f: X => X = q._1;
      val x: X = q._2;
      f.apply(x)
    }
  })
}

The second f2_explicit_func_arg version (equivalent to f2) is more enlightening than the shorter original f2-version. In the desugared and type-checked code of f2_explicit_func_arg, we see that the type X miraculously reappears, and the typechecker indeed infers:

f: X => X
x: X

so that f(x) is indeed valid.

---

In the more obvious work-around with an explicitly named type variable, we do manually what the compiler does for us in this case.

We could also have written:

type TypeCons[X] = (X => X, X)
list.map{ case t: TypeCons[x] => t._1(t._2) }

or even more explicitly:

list.map{ case t: TypeCons[x] => {
  val func: x => x = t._1
  val arg: x = t._2
  func(arg)
}}

and both versions would compile for very much the same reasons as f2.

Football

I really wish I understood why it is that the pattern match does this in a way that the regular type inference doesn't. I know that a generic helper function can do the same thing: def helper[S](q: (S => S, S)) = q._1(q._2). I've seen a discussion on that somewhere, though I can't recall where. – Waterlogged

@JoePallas I'm not sure how the helper function is supposed to help here, at least list map helper doesn't work. I'm also not sure on what level you would like to have the explanation for "why": I hope I've managed to make it clear enough why the list.map{x => ...} shouldn't work in any imaginable language. The argument that prohibits list.map{x => ...} falls apart as soon as one introduces additional pattern matching step, so there are no "theoretical" reasons why it shouldn't work. Indeed, practically, Scala manages to attach more type information to the matched variable. – Football

@JoePallas [... continued ...] "Why does Scala manage to infer all kind of useful constraints on the types of variables used in pattern matching?" I don't know how to answer it, because 1) I don't know enough about the internals of Scala's pattern matching or type inference 2) I don't know how far I have to decompose the explanation for the "why" until someone else takes all the tiny sub-arguments for granted, as axioms. – Football

@AndreyTyukin Try list.map(helper(_)) or list.map(t => helper(t)). – Shirlyshiroma

@AlexeyRomanov Yes, right this works, thanks! A comment under your answer here tells exactly that. But it seems to work for a different reason than the pattern matching: you are applying an universally quantified function to an existentially quantified argument, which totally makes sense. Is there some common theme between the generic helper function and the pattern matching that helps explain the "type X miraculously reappears"-part better? – Football

I remember there was some information about that in the Typelevel blog, but I don't remember where exactly. typelevel.org/blog/2015/07/13/type-members-parameters.html should be a starting point. – Shirlyshiroma

@AlexeyRomanov I've read the article (at least most of it) a few times, I'm afraid that it is also a bit too far away from the concrete topic of the question, and that it probably won't provide an answer for the "Why?" that is less vague than "Scala has a powerful type system, it can infer lot of stuff". I guess I will take solace in the quote "Scala is large enough that very few understand all of it", and accept my own scribblings as an answer. Will reaccept if someone provides an answer that is roughly as detailed, and contributes something what I didn't know. – Football

@AndreyTyukin By "starting point" I mean it's the first post of a pretty long series and if I remember correctly, there's something which is close to this question in one or more of the posts. – Shirlyshiroma

@AlexeyRomanov Yes, that's what I was thinking of. It's in the second post of the series. "When we call the type-parameterized variant to implement the existential variant … we are just helping the compiler … both scalac and javac manage to infer that the type T should be the (otherwise unspeakable) existential." – Waterlogged