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 Russo¹, 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 Scala².

(* 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.