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) ?

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.

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 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.

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.â€ť

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?

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.

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â€¦