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.
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) ?
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.
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?
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?
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”
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.
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”
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.”
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…