# Unstable type expressions

[mutation]

Types can be passed around as first-class values in several languages, either directly (particularly in languages with dependent types and universes) or as part of another structure (e.g. first-class modules in OCaml, abstract type members in Scala).

This means that it is possible to have a type expression $T$ that depends on a value: if some boolean $b$ is false, then $T = \n{Int}$, but if it's true then $T = \n{String}$. In languages with mutation, there can even be a type expression $T$ where $T ≠ T$, because $T$ yields two different types when evaluated twice.

The risk is that if the type system does not perfectly track dependency of types on values, or the presence of side-effects in type expressions, then you may end up with two incompatible values both claiming to be of type $T$.

The problem was noticed by Russo1, in his thesis introducing first-class modules to Standard ML, where he gave a counterexample showing that the naive approach was unsound. The issue later reappeared in Scala2.

(* Counterexample by Claudio Russo *)
module F = functor (X:sig val b:bool end)
unpack
if X.b then
pack struct
type t = int
val x = 1
fun y n = -n
end
as sig
type t
val x : t
val y : t -> t
end
else
pack struct
type t = bool
val x = true
fun y b = if b then false else true
end
as sig
type t
val x : t
val y : t -> t
end
end
as sig
type t
val x : t
val y : t → t
end
module A = F (struct val b = true end)
module B = F (struct val b = false end)
val z = A.y B.x

// Counterexample by Vladimir Reshetnikov
trait A {
type T
var v : T
}

object B {
def f(x : { val y : A }) { x.y.v = x.y.v }

var a : A = _
var b : Boolean = false
def y : A = {
if(b) {
a = new A { type T = Int; var v = 1 }
a
} else {
a = new A { type T = String; var v = "" }
b = true
a
}
}
}

// B.f(B) causes a ClassCastException


There are two standard fixes:

• Syntactically restrict expressions appearing in types

The syntax of type expressions can be limited to constructions whose value cannot change. See paths in ML-family languages and stable identifiers in Scala.

This can lead to some surprises, because valid syntax then depends on context. For instance, in OCaml, anonymous module parameters are possible in module definitions but not type expressions:

module X = struct type t = int end
module FX = F (X)                           (* ok *)
type t1 = (F (X)).t                         (* ok *)
module FX = F (struct type t = int end)     (* ok *)
type t2 = (F (struct type t = int end)).t   (* error *)


(Anonymous module parameters also cause other surprises: see the avoidance problem)

• Restrict effects of expressions appearing in types

If the language statically tracks effects, either directly with a type-and-effect system or via encoding all effects in an IO monad, then it is possible to check that only pure expressions are used in types.

There is an additional wrinkle here: some effect systems track mutation but allow nontermination to count as "pure". Depending on the exact system, allowing a possibly-nonterminating expression into the type language may be unsound because of a type-level version of the eventually, nothing problem.

1

Fig 7.12 on p. 270 of Types For Modules, Claudio Russo (1998)