Some kinds of Anything

[subtyping] [polymorphism]

In type systems with polymorphism and subtyping, there are four different meanings that the phrase "any type" could have:

  • Top type

    The top type is a supertype of every type. Any value can be turned into a value of type , but given a value of type there's not much you can do with it.

  • Bottom type

    The bottom type is a subtype of every type. A value of type can be turned into a value of any type, but there's no way to construct a value of type . (If there is, the type system is broken. See Eventually, nothing for one example).

  • Universal type α.  ∀α . ; \dots

    A value of a universal type α.φ(α)∀α. φ(α) can be used at type φ(X)φ(X), for any type XX. To construct one, the value must typecheck with an unknown abstract type αα.

  • Existential type α.  ∃α . ; \dots

    A value of an existential type α.φ(α)∃α. φ(α) can be constructed from a value of type φ(X)φ(X), for any type XX. To use one, the use must typecheck with an unknown abstract type αα.

There are a couple of relationships between these types:

  • =α.α⊥ = ∀α. α

    is the type that can be used at any type, but cannot be constructed.

  • =α.α⊤ = ∃α. α

    is the type that can be constructed from any type, but cannot be used.

In some systems, these relationships extend to more complicated types as well, for instance with a covariant type List[A]\n{List}[A] of immutable lists with elements of type AA:

  • List[]=α.List[α]\n{List}[⊥] = ∀α. \n{List}[α]

    The elements of a single list ll cannot simultaneously be of every possible type αα. Such a list must be empty, which is the same thing as being a list of .

  • List[]=α.List[α]\n{List}[⊤] = ∃α. \n{List}[α]

    If a list contains elements of an unknown type αα, then there is nothing useful we can do with them. The situation is the same as if we had a list of .

The extent to which languages implement these rules varies. Sometimes1, they are used to justify converting List[]List[⊥] to α.List[α]∀α.List[α]. Sometimes2, they are used to justify considering those two as different spellings of the same type. Other times, they are not used, but are definable in the language.

However, if implementing these rules it is crucial to keep track of variance. Consider the type α.(List[α]Int)∃α. (\n{List}[α] → \n{Int}): this is a function that accepts lists of some particular unknown type. It could be, for instance, the sum\n{sum} function of type List[Int]Int\n{List}[\n{Int}] → \n{Int}.

It is unsound to treat this the same as List[]Int\n{List}[⊤] → \n{Int}, as that would allow us to pass a list of, say, strings to the sum\n{sum} function. In fact, since all of the occurrences of αα are contravariant (that is, to the left of a single function arrow), this type is equivalent to List[]Int\n{List}[⊥] → \n{Int}.

Scala supports subtyping and polymorphism, and several versions of the language34 had this soundness issue, where α.φ(α)∃α. φ(α) was converted to φ()φ(⊤) (spelled φ(Any)φ(\n{Any}) in Scala), without regard for the variance of φφ.

// Counterexample by Paul Chiusano
/* The 'coinductive' view of streams, represented as their unfold. */
trait Stream[+A]
case class Unfold[S,+A](s: S, f: S => Option[(A,S)]) extends Stream[A]

object Stream {
  def fromList[A](a: List[A]): Stream[A] = 
    Unfold(a, (l:List[A]) =>,l.tail)))

/* If I have a Stream[Int], and I match and obtain an Unfold(s, f),
   the type of (s,f) should be (S, S => Option[(A,S)]) forSome { type S }.
   But Scala just promotes everything to Any: */
val res0 = Stream.fromList(List(1,2,3,4))
val res1 = res0 match { case Unfold(s, f) => s }
// res1: Any = List(1, 2, 3, 4)

/* Notice that the type of s is Any.
   Likewise, the type of f is also wrong, it accepts an Any: */

val res2 = res0 match { case Unfold(s, f) => f }
// res2: Any => Option[(Int, Any)] = <function1>

/* Since f expects Any, we can give it a String and get a runtime error: */

res0 match { case Unfold(s, f) => f("a string!") } // crashes

Relaxing the Value Restriction, Jacques Garrigue (2004)


Polymorphism, subtyping, and type inference in MLsub, Stephen Dolan and Alan Mycroft (2017)