Why does Array[T forSome { type T; }] mean Array[Any]

existential-type, scala, type-systems

Solution

The difference lies in when the type system decides what T is.

Maybe the best answer is, try using those two types in some code, see what happens, and try to figure out why. But I'll try to explain some type theory first. In this case:

Array[T forSome { type T; }]

where the `forSome` is inside the `[]` brackets, each element by itself just has to somehow be explained as `T forSome { type T; }`. OK, so an `Int` is a `T` for some type `T`, so you can put an `Int` in the array. A `String` also is a `T` for some type `T`, and because the choice `forSome` applies to only one element at a time, you get to say `T` is `String` this time instead of `Int`, so you can put the `String` in the array even though it already contains an `Int`.

On the other hand, while we can choose `T` independently for any element of the array, the type of the array itself has already been chosen: it is the type of array that can hold anything. It can't be an `Array[Int]` or an `Array[String]`.

But in this case:

Array[T] forSome { type T; }

the type `T` is decided just once, outside the array. The array could actually be an `Array[Int]`, and `Array[String]`, or an `Array[Any]`. But once the type `T` is chosen, all elements of the array have to be consistent with that type.

OK, now let's try some code. Here's an example:

scala> var a = Array(1,2);
a: Array[Int] = Array(1, 2)

scala> def first(z : Array[T] forSome { type T }) = z(0);
first: (z: Array[_])Any

scala> def firstany(z : Array[T forSome { type T }]) = z(0);
firstany: (z: Array[T forSome { type T }])Any

scala> first(a);
res0: Any = 1

scala> firstany(a);
error: type mismatch;
 found   : Array[Int]
 required: Array[T forSome { type T }]
       firstany(a);
                ^

Why the error? Because the array `a` has the type `Array[Int]`, which can contain only things of type `Int`. That's certainly an `Array[T] forSome {type T}`, because all the type system needs to do is choose Int as the type T. Therefore `first(a)` is OK. But as explained above, an `Array[T forSome { type T }]` cannot be an `Array[Int]`, so `firstany(a)` is an error.

But the following is OK, because an `Array[Any]` is an `Array[T forSome { type T }]`:

scala> var b = Array(1, "x");
b: Array[Any] = Array(1, x)

scala> firstany(b);
res1: Any = 1

Problem

I'm reading the article "Existential types in Scala", and found something I can't understand: ``` Array[T] forSome { type T; } Array[T forSome { type T; }] ``` They look almost identical, but they're in fact very different. The first is the type of all arrays, whatever their type parameter. The second is Array[Any]. Why are they so different, and especially, why does the second one mean `Array[Any]`?

Original source