Skolemization of existentially typed expressions

Question

In Scala, the following expression raises a type error:

val pair: (A => String, A) forSome { type A } = ( { a: Int => a.toString }, 19 )
pair._1(pair._2)

As mentioned in SI-9899 and this answer, this is correct according to the spec:

I think this is working as designed as per SLS 6.1: "The following skolemization rule is applied universally for every expression: If the type of an expression would be an existential type T, then the type of the expression is assumed instead to be a skolemization of T."

However, I do not fully understand this. At which point is this rule applied? Does it apply in the first line (i.e., the type of pair is a different one than given by the type annotation), or in the second line (but applying the rule to the second line as a whole would not lead to a type error)?

Let's assume SLS 6.1 applies to the first line. It is supposed to skolemize existential types. We can make the in the first line a non-existential type by putting the existential inside a type parameter:

case class Wrap[T](x:T)
val wrap = Wrap(( { a: Int => a.toString }, 19 ) : (A => String, A) forSome { type A })
wrap.x._1(wrap.x._2)

It works! (No type error.) So that means, the existential type got "lost" when we defined pair? No:

val wrap2 = Wrap(pair)
wrap2.x._1(wrap2.x._2)

This type checks! If it would have been the "fault" of the assignment to pair, this should not work. Thus, the reason why it does not work lies in the second line. If that's the case, what's the difference between the wrap and the pair example?

To wrap up, here is one more pair of examples:

val Wrap((a2,b2)) = wrap
a2(b2)

val (a3,b3) = pair
a3(b3)

Both don't work, but by analogy to the fact that wrap.x._1(wrap.x._2) did typecheck, I would have thought that a2(b2) might typecheck, too.

Answer 1

I believe I figured out most of the process how the expressions above are typed.

First, what does this mean:

The following skolemization rule is applied universally for every expression: If the type of an expression would be an existential type T, then the type of the expression is assumed instead to be a skolemization of T. [SLS 6.1]

It means that whenever an expression or subexpression is determined to have type T[A] forSome {type A}, then a fresh type name A1 is chosen, and the expression is given type T[A1]. This makes sense since T[A] forSome {type A} intuitively means that there is some type A such that the expression has type T[A]. (What name is chosen depends on the compiler implementation. I use A1 to distinguish it from the bound type variable A)

We look at the first line of code:

val pair: (A => String, A) forSome { type A } = ({ a: Int => a.toString }, 19)

Here the skolemization rule is actually not yet used. ({ a: Int => a.toString }, 19) has type (Int=>String, Int). This is a subtype of (A => String, A) forSome { type A } since there exists an A (namely Int) such that the rhs is of type (A=>String,A).

The value pair now has type (A => String, A) forSome { type A }.

The next line is

pair._1(pair._2)

Now the typer assigns types to subexpressions from inside out. First, the first occurrence of pair is given a type. Recall that pair had type (A => String, A) forSome { type A }. Since the skolemization rule applies to every subexpression, we apply it to the first pair. We pick a fresh type name A1, and type pair as (A1 => String, A1). Then we assign a type to the second occurrence of pair. Again the skolemization rule applies, we pick another fresh type name A2, and the second occurrence of pair is types as (A2=>String,A2).

Then pair._1 has type A1=>String and pair._2 has type A2, thus pair._1(pair._2) is not well-typed.

Note that it is not the skolemization rule's "fault" that typing fails. If we would not have the skolemization rule, pair._1 would type as (A=>String) forSome {type A} and pair._2 would type as A forSome {type A} which is the same as Any. And then pair._1(pair._2) would still not be well-typed. (The skolemization rule is actually helpful in making things type, we will see that below.)

So, why does Scala refuse to understand that the two instances of pair actually are of type (A=>String,A) for the same A? I do not know a good reason in case of a val pair, but for example if we would have a var pair of the same type, the compiler must not skolemize several occurrences of it with the same A1. Why? Imagine that within an expression, the content of pair changes. First it contains an (Int=>String, Int), and then towards the end of the evaluation of the expression, it contains a (Bool=>String,Bool). This is OK if the type of pair is (A=>String,A) forSome {type A}. But if the computer would give both occurrences of pair the same skolemized type (A1=>String,A1), the typing would not be correct. Similarly, if pair would be a def pair, it could return different results on different invocations, and thus must not be skolemized with the same A1. For val pair, this argument does not hold (since val pair cannot change), but I assume that the type system would get too complicated if it would try to treat a val pair different from a var pair. (Also, there are situations where a val can change content, namely from unitialized to initialized. But I don't know whether that can lead to problems in this context.)

However, we can use the skolemization rule to make pair._1(pair._2) well-typed. A first try would be:

val pair2 = pair
pair2._1(pair2._2)

Why should this work? pair types as (A=>String,A) forSome {type A}. Thus it's type becomes (A3=>String,A3) for some fresh A3. So the new val pair2 should be given type (A3=>String,A3) (the type of the rhs). And if pair2 has type (A3=>String,A3), then pair2._1(pair2._2) will be well-typed. (No existentials involved any more.)

Unfortunately, this will actually not work, because of another rule in the spec:

If the value definition is not recursive, the type T may be omitted, in which case the packed type of expression e is assumed. [SLS 4.1]

The packed type is the opposite of skolemization. That means, all the fresh variables that have been introduced inside the expression due to the skolemization rule are now transformed back into existential types. That is, T[A1] becomes T[A] forSome {type A}.

Thus, in

val pair2 = pair

pair2 will actually be given type (A=>String,A) forSome {type A} even though the rhs was given type (A3=>String,A3). Then pair2._1(pair2._2) will not type, as explained above.

But we can use another trick to achieve the desired result:

pair match { case pair2 =>
  pair2._1(pair2._2) }

At the first glance, this is a pointless pattern match, since pair2 is just assigned pair, so why not just use pair? The reason is that the rule from SLS 4.1 only applied to vals and vars. Variable patterns (like pair2 here) are not affected. Thus pair is typed as (A4=>String,A4) and pair2 is given the same type (not the packed type). Then pair2._1 is typed A4=>String and pair2._2 is typed A4 and all is well-typed.

So a code fragment of the form x match { case x2 => can be used to "upgrade" x to a new "pseudo-value" x2 that can make some expressions well-typed that would not be well-typed using x. (I don't know why the spec does not simply allow the same thing to happen when we write val x2 = x. It would certainly be nicer to read since we do not get an extra level of indentation.)

After this excursion, let us go through the typing of the remaining expressions from the question:

val wrap = Wrap(({ a: Int => a.toString }, 19) : (A => String, A) forSome { type A })

Here the expression ({ a: Int => a.toString }, 19) types as (Int=>String,Int). The type case makes this into an expression of type (A => String, A) forSome { type A }). Then the skolemization rule is applied, so the expression (the argument of Wrap, that is) gets type (A5=>String,A5) for a fresh A5. We apply Wrap to it, and that the rhs has type Wrap[(A5=>String,A5)]. To get the type of wrap, we need to apply the rule from SLS 4.1 again: We compute the packed type of Wrap[(A5=>String,A5)] which is Wrap[(A=>String,A)] forSome {type A}. So wrap has type Wrap[(A=>String,A)] forSome {type A} (and not Wrap[(A=>String,A) forSome {type A}] as one might expect at the first glance!) Note that we can confirm that wrap has this type by running the compiler with option -Xprint:typer.

We now type

wrap.x._1(wrap.x._2)

Here the skolemization rule applies to both occurrences of wrap, and they get typed as Wrap[(A6=>String,A6)] and Wrap[(A7=>String,A7)], respectively. Then wrap.x._1 has type A6=>String, and wrap.x._2 has type A7. Thus wrap.x._1(wrap.x._2) is not well-typed.

But the compiler disagrees and accepts wrap.x._1(wrap.x._2)! I do not know why. Either there is some additional rule in the Scala type system that I don't know about, or it is simply a compiler bug. Running the compiler with -Xprint:typer does not give extra insight, either, since it does not annotate the subexpressions in wrap.x._1(wrap.x._2).

Next is:

val wrap2 = Wrap(pair)

Here pair has type (A=>String,A) forSome {type A} and skolemizes to (A8=>String,A8). Then Wrap(pair) has type Wrap[(A8=>String,A8)] and wrap2 gets the packed type Wrap[(A=>String,A)] forSome {type A}. I.e., wrap2 has the same type as wrap.

wrap2.x._1(wrap2.x._2)

As with wrap.x._1(wrap.x._2), this should not type but does.

val Wrap((a2,b2)) = wrap

Here we see a new rule: [SLS 4.1] (not the part quoted above) explains that such a pattern match val statement is expanded to:

val tmp = wrap match { case Wrap((a2,b2)) => (a2,b2) }
val a2 = tmp._1
val b2 = tmp._2

Now we can see that (a2,b2) gets type (A9=>String,A9) for fresh A9, tmp gets type (A=>String,A) forSome A due to the packed type rule. Then tmp._1 gets type A10=>String using the skolemization rule, and val a2 gets type (A=>String) forSome {type A} by the packed type rule. And tmp._2 gets type A11 using the skolemization rule, and val b2 gets type A forSome {type A} by the packed type rule (this is the same as Any).

Thus

a2(b2)

is not well-typed, because a2 gets type A12=>String and b2 gets type A13=>String from the skolemization rule.

Similarly,

val (a3,b3) = pair

expands to

val tmp2 = pair match { case (a3,b3) => (a3,b3) }
val a3 = tmp2._1
val b3 = tmp2._2

Then tmp2 gets type (A=>String,A) forSome {type A} by the packed type rule, and val a3 and val b3 get type (A=>String) forSome {type A} and A forSome {type A} (a.k.a. Any), respectively.

Then

a3(b3)

is not well-typed for the same reasons as a2(b2) wasn't.