Search code examples
scalatype-systemsexistential-type

Type of T forSome{type T}


I am going through drmacvier blog about existential types in Scala. After reading it I was experimenting with types and I am checking the equality of types in the following manner as given in rnduja blog.

def implicitly[A](implicit a: A) = a

// To check equality of two types
class =:=[A, B]
implicit def equalTypeInstance[A] = new =:=[A, A]
def type_==[A, B](implicit ev: A =:= B = null) = ev != null

// To check subtype relation between two types
class <:<[-A, +B]
implicit def subTypeInstance[A] = new <:<[A, A]
def type_<[A, B](implicit ev: A <:< B = null) = ev != null

The first thing I checked was this:

type_==[Any, T forSome{type T}] // true

what I could not understand is T forSome{type T} is satisfied by any type but why is its type Any. Assuming, since Any is common ancestor of all possible types it makes sense that they are are equal. In the similar way I was able to reason about.

type_==[Array[Any], Array[T forSome{type T}]] // true
type_==[List[Any], List[T forSome{type T}]] // true

I was not able to get this right with the same reasoning.

type_==[Array[Any], (Array[T] forSome{type T})] // false
type_==[List[Any], (List[T] forSome{type T})] // true

what am I missing here ? Is my way of reasoning flawed ?


Solution

  • what I could not understand is T forSome{type T} is satisfied by any type but why is its type Any

    Any value (not any type) has some type (at least type Any). So it has type T for some type T. But this means it also has type T forSome { type T }. So any value of type Any has type T forSome { type T } (and vice versa).

    For the first two comparisons: if A is equal to B, then F[A] should be equal to F[B], whatever F is. You've just checked that Any and T forSome {type T} are equal, so... But you simply can't use the same reasoning for the other two cases: what would A, B and F be?

    Array[Any] is not the same as Array[T] forSome { type T }, because let's say you have a value

    val array: Array[String] = Array("a")
    

    Then it has type Array[T] forSome { type T } (do you understand why?):

    val arrayForSome: Array[T] forSome { type T } = array // compiles
    

    but

    val arrayOfAny: Array[Any] = array
    

    doesn't compile (because Array is invariant). So clearly Array[T] forSome { type T } and Array[Any] are different: a value can have one of these types without having the other.