Answering the subtype question

Language Design
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 Types and Programming Languages.

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.

2 Likes
13

I’m reading through On Decidability of Nominal Subtyping with Variance as was suggested (by smarter). Can someone explain to me what “head constructor” means? The term appears in Section 1, in the contributions subsection. The quote is: “class hierarchies are restricted so that a type may not have multiple supertypes with the same head constructor”

14

I think it just means that you can’t extend the same class twice.

1 Like
15

Thanks, and what does it mean that “a type system is undecidable”? Does this mean that the subtype procedure is undecidable? Or is it more subtle that that? For example, are there type systems for which the subtype relation is decidable yet the type membership question is sometimes undecidable. I cannot image that in the type systems I’m familiar with because the type member question is the same as singleton type subtype question in all the cases I am aware of.

16

Where did you see that expression used? I would guess people might use that as a shortcut to say something like “any algorithm that tells you whether an expression typechecks or not in this type system is undecidable”

17

Minor quibble: undecidability does not qualify algorithms, but problems. So a more correct formulation would be: “there cannot be an algorithm that can always tell you whether an expression type checks or not in this type system.”

2 Likes
18

What does “an expression type checks” mean in a non-statically typed language which still has a type system? Perhaps it means being able to determine whether a type is inhabited?

19

It doesn’t mean anything at all AFAIK. A dynamic language checks values (not expressions) against runtime types.

Note: languages like Julia actually have a full type system at runtime, but it’s used to do multiple dispatch by doing some subtyping checks at runtime.

20

For example in “Java Generics are Turing Complete” paper by Radu Grigore, he says in the Related Work section: Java’s type system is not only undecidable, but also unsound. Many other languages have undecidable type systems: Haskell with extensions (…) OCaml (…), C++, and Scala, to name a few. It is often the case that undecidable type systems are fun playground for metaprogramming…