by Stephen Compall on Jul 30, 2015
technical
This is the sixth of a series of articles on “Type Parameters and Type Members”. If you haven’t yet, you should start at the beginning, which introduces code we refer to throughout this article without further ado.
In a subtyping language such as Java or Scala, first-class existentials are a helpful ally for modeling values and methods that abstract over subtypes in different ways. In a language with mutation, such as Java or Scala, existentials help deal with certain kinds of state changes without violating type safety.
But values, themselves, never change types. When you first practice with existentials, the Java and Scala compilers seem to become veritable minefields of type errors—do something slightly different in your code, and everything falls apart. But this is just about nothing being a free lunch: the wide variety of values meeting any given existential type, combined with the possibility for mutation, means a sound typechecker must be very conservative about what it permits when using those values.
So, in this article, we’ll explore some of these type error pitfalls, see why it’s perfectly reasonable for the compilers to complain about these pieces of code, and fix the errors using the equivalence rules we’ve learned about in previous articles. This is a big topic, so in the next article, we’ll talk about taking advantage of the freedoms that the compilers are concerned about in this one.
Let’s say you have a list of strings, strs: List[String]. But you
want that value to change: you want it to be a List[Int] instead.
Maybe every value in the list parses to an integer and you want to
“map in place”; maybe you want to use -1 for every string that can’t
be parsed.
Generic systems like those of Java, Scala, and the ML family don’t let you do this for a few reasons.
First, with regard to structures like List, let’s suppose we are
adding this feature to the type system, and that the list has type
List[String] before replacement, and List[Int] after. What type
does it have when we’re halfway done? The type system requires us to
guarantee that there are no strings, only ints, left once we’re
done; how do we track our progress? Remember that vague promises of
“I tested the code” are meaningless to the type system; you have to
prove it mathematically. This is a solvable problem, but the known
solutions far complicate the type system beyond the design goals of
these languages: the cost is far too high for the benefit.
Second, let us suppose that we’ve solved the first problem. Or, let us suppose that we introduce a structure for which this isn’t a problem.
final case class OneThing[T](var value: T)
There, no chance of “halfway done” there! But something else happens.
val strs: OneThing[String] = OneThing("hi")
strs.value = 42
// won't compile, just a thought experiment
Now, presumably, completely aside from the value, the variable strs
has changed types to OneThing[Int]. Not just the value in it, the
variable itself. OK, so what if that variable came from someplace
else?
def replaceWithInt(ote: OneThing[_]): Unit =
t.value = 42
val strs: OneThing[String] = OneThing("hi")
replaceWithInt(strs)
// also won't compile, thought experiment
Now, the type of replaceWithInt must contain a note that “by the
way, the type of ote, and any variables that refer to it, and any
variables that refer to those variables, and so on until it stops,
will change as a result of this call”.
This is a problem of aliases, all the locations that may refer to a value. If you change the type of the value, you also have to update every reference to it, at compile time! This is the type system; your promise that you have no other references is not good enough. You have to prove it.
As with the previous problem, the known solutions to this problem would complicate the type systems of Java and Scala beyond their design goals. In a sense, this aspect of their type systems can be considered to encourage functional programming. A type-changing map that builds a new list of the new type, or what have you, instead of mutating the old one, is trivial in the Java/Scala generics systems. There are no chances of aliasing problems, because no one could possibly have an unknown reference to the value you just constructed. This is a even more obvious design choice in the ML family languages, which make no secret of favoring functional programming.
We saw earlier that a simple get from a
List<?>, followed by adding that value right back to the same list,
didn’t work, but if we took that xs and passed it to a
type-parameterized version, everything worked fine. Why is that?
If you have a mutable variable of an existential type, the
existentialized part of the type may have different [type] values at
different parts of the program. Let’s use
the StSource from the projection post.
Note that the S member is existential, because we did not bind it.
var mxs: StSource[String] = StSource(0)(x => (x.toString, x + 1))
// at this point in the program, the S is Int
val s1 = mxs.init
// now I'm going to change mxs
mxs = StSource("ab")(x => (x, x.reverse))
// at this point in the program, the S is String
mxs.emit(s1)
TmTp6.scala:14: type mismatch;
found : tmtp6.Tmtp4Funs.s1.type (with underlying type tmtp4.StSource[String]#S)
required: _2.S where val _2: tmtp4.StSource[String]
mxs.emit(s1)
^
And it’s good that this happens, because the value we got from init
is definitely incompatible with the argument type to emit.
If we don’t want to track when this happens—and we certainly can’t decide, in all cases, when a mutable variable such as this has been overwritten so as to change its existentials, given the freedoms afforded by Java—how can we treat a mutable variable with existentials as safe? The type system makes a simplifying assumption: every reference to the variable gets fresh values to fill in the existentials.
If it helps, you can think of a mutable variable as an immutable
variable that wraps its type with an extra layer. In fact, that’s
what scalac does when you capture a var.
So mxs is, in a sense, of type Ref[StSource[String]], where
trait Ref[T] {
def value: T
def update(t: T): Unit
}
So, by substitution, the variable mxs is really a pair of functions,
() => StSource[String] and StSource[String] => Unit. The “getter”
returns StSource[String]; each time you invoke that getter, you
might get an StSource[String] with a different S member, because
the forSome effectively occurs inside the body, as described in
the substitutions of “Nested existentials”.
Of course, this means you can take advantage of this in your own
designs, to get some of the behavior of a type-changing value
mutation. The use of variable references to delineate existentials
means that, even when we replace mxs above, the behavior of the
variable in the context of an instance hasn’t really changed, so
nothing about the containing value’s type has changed. We thus
preserve our property, that values never change types.
When you make a single reference, it has to be consistent; subsequent
mutations have no effect on the value we got from that reference. So
we can pass that reference somewhere that asserts that this doesn’t
happen in its own context, such as a type-parameterized
≡m method. If you have a mutable variable
of type List<T>, even if you don’t know what T is, you know that
any updates to that variable will keep the same T.
If I change the variable to final in Java, and remove mutation, I
shouldn’t have this problem anymore. Surprisingly, I do; this is what
happened in
the original copyToZero example,
where the argument was declared final. I assume that this is just a
simplifying assumption in javac, that the extra guarantee of
unchanging existentials offered by final isn’t understood by the
compiler.
In the case of Scala, though, when you are using existential type
members, Scala can understand the implications of an immutable
variable, declared with val.
val imxs: StSource[String] = StSource(0)(x => (x.toString, x + 1))
val s1 = imxs.init
// you can do whatever you want here; the compiler will stop you from
// changing imxs
imxs.emit(s1)
It can’t pull off this trick for type parameters, having just as much trouble as Java there. So this is another reason for our original rule of thumb.
The benefit we get from
passing copyToZeroP’s argument to copyToZeroT
is that we name the existential for the single reference to the
argument that we make. We name it T there, for the scope of its
invocation.
Likewise, in Scala, each val introduces, while it is in scope, each
existential member it has, as a type name. There are
a lot of rules in Scala
for exactly when this happens, but you may want to simply experiment.
We got a hint of what that name is
when we used StSource existentially in the REPL.
Here’s the previous example again, with a type annotation for s1.
val imxs: StSource[String] = StSource(0)(x => (x.toString, x + 1))
val s1: imxs.S = imxs.init
imxs.emit(s1)
We have gained convenience, not power, with this path-dependent types feature; we can always pass into a type-parameterized local method, with only the inconvenience of having to write out the whole polymorphic method and call dance. Moreover, this is nowhere near a solution to the type projection problem; there are too many things that a type parameter can do that we can’t with this feature. But we’ll dive into that in a later post.
There is another little corner case in method equivalence to consider.
def copyToZeroNP(xs: => PList[_]): Unit
def copyToZeroNT[T](xs: => PList[T]): Unit
These method types are not equivalent! That’s because copyToZeroNP
can be called with a by-name that evaluates to a list with a
different element type each time; copyToZeroNT doesn’t allow this.
def time: PList[_] = {
val t = System.currentTimeMillis
if (t % 2 == 0) PCons("even", PNil())
else PCons(66, PNil())
}
copyToZeroNP(time) // ok
copyToZeroNT(time) // not ok
In effect, => is like a type constructor; we can think of these
arguments as byname[PList[_]] and byname[PList[T]]. So we have
exactly the same problem as we had with
plenLength and plenLengthTP.
Unfortunately, Scala currently accepts this, where it shouldn’t.
The difference between these two methods gives us a hint about working
with existentials: if we can shift the scope for a given existential
outside the function that keeps giving us different types on every
reference, we might have an easier time working with it, even if we
can’t change it to a val; maybe it needs to be lazy and not saved,
for example. So, despite the occasional convenience of path-dependent
types, type parameterized methods are still your best friends when
working with existential types.
In the next article, “To change types, change values”, we’ll look at some programs that make use of the two kinds of “type changing” discussed above. After that, we’ll finally talk about methods that return values of existential type, rather than merely taking them as arguments.
This article was tested with Scala 2.11.7.
