Dominique Unruh - 3 months ago 16

Scala 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`

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`

`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`

`wrap`

`pair`

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)`

`a2(b2)`

Answer

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 `val`

s and `var`

s. 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.