Answering the subtype question

#1

Can someone explain how the subtypep question is answered within the Scala compiler, and presumably in user-land within Scala macros. I.e. given two type specifiers how do we determine whether one type is a subtype of the other? My guess is that this question is not always answerable in Scala 2, but is in Scala 3. Although I might be mistaken.

Is there a function/API for this? Or does every application have to write code to answer the question for itself?

Why do I ask? It is because my PhD research topic dealt with computing with types in dynamic languages, specifically with Common Lisp whose type system is modeled by a lattice. There is function built into Common Lisp called SUBTYPEP, which answers the question whether one type is a subtype of another. I would like to generalize my research topic to include a larger class of type systems. Since Scala 3’s type system is based on a type lattice, it is an interesting possibility to pursue.

I can’t imagine, however, generalizing to a type system for which the subtype question is not answerable.

#2

You can find the implementation here: https://github.com/scala/scala/blob/v2.13.0/src/reflect/scala/reflect/internal/tpe/TypeComparers.scala#L266

And you can access this functionality at runtime via the reflection API:

scala> import scala.reflect.runtime.universe._
import scala.reflect.runtime.universe._

scala> typeOf[String{ def foo: Int }] <:< typeOf[Any { def foo: AnyVal }]
res0: Boolean = true

Or at compilation time via implicit search:

scala> implicitly[String{ def foo: Int } <:< Any { def foo: AnyVal }]
res1: String{def foo: Int} <:< Any{def foo: AnyVal} = generalized constraint

Or even

scala> def a: String{ def foo: Int } = ???
a: String{def foo: Int}

scala> def b: Any { def foo: AnyVal } = a
b: Any{def foo: AnyVal}
1 Like
#3

Thanks for the link. I notice that isSubType has type (Type,Type,Depth)=>Boolean. Does this mean that the question is always answerable. Or does it return false both on the case of not-a-subtype and also cannot-determine? I.e., does isSubType(A,B) always return the negative of isSubType(B,A) ?

#4

I am not personally aware of a case where it doesn’t (other than when A == B). Scala’s type system is a lattice so if there were another such case then I believe that would be a bug.

#5

Are you suggesting that A is not considered a subtype of itself? Because one way to figure out that two types are the same is to ask whether each is a subtype of the other. Or to ask whether two types intersect, one may ask whether their intersection is a subtype of the empty set. And of course any subtype of the empty set is identically the empty set.

#6

No, I was suggesting that every type is a subtype of itself so then both isSubType(A,B) and isSubType(B,A) return true when A and B are the same type.

#7

Yes, soundness requires the subtype checker to not produce false positives, but false negatives are unavoidable in general.

No, trivial example: both Int <:< String and String <:< Int are false.

#8

Ahh, of course neither Int nor String is a subtype of the other.

#9

So am I correct that false does not mean that A is not a subtype of B, but rather it means that it cannot be proven that A is a subtype of B. The common lisp SUBTYPEP function distinguishes these two cases. The CL function unfortunately does not distinguish between “did not manage to prove” and “cannot prove”.

Can I have an example of a false negative which is unavoidable? Is it unavoidable for performance reasons, or is it actually no possible to determine?

#10

Yes.

See http://www.cis.upenn.edu/~bcpierce/papers/variance.pdf, https://arxiv.org/pdf/1605.05274.pdf. If you’re interested in learning more, I suggest reading https://www.cis.upenn.edu/~bcpierce/tapl/.

#11

I read this book a few years ago. It was actually a motivation to learn Scala when I noticed the notation in Scala was very similar to the Pierce notation. I thought learning scala would help me understand the book better, which is no easy task. So perhaps we’ve reached metacircularity? To understand either, you must understand the other?

1 Like
#12

I prefer to think of it as an iterative algorithm: you go back and forth refining your understanding each time, working your way up from a basic intuition to deep internalization.

1 Like