type checking requires testing the equivalence of runtime expressions
Quick prerequisite here: testing the equivalence of runtime expressions is, in general, undecidable for languages with straightforward recursion. (see: eq(PDA)) Thus, for Scala to be a dependently-typed language, we must clarify an ambiguity in this definition:
type checking requires testing the pessimistic equivalence of runtime expressions
Which is to say, the type checker will attempt to check the equivalence of runtime expressions, and in the cases where it fails, it will assume not-equal. In order to prevent this definition from being completely vacuous, let's further assume that there must exist at least one case (perhaps trivial) where the compiler is able to perform this runtime equivalence checking, and thus its equality check produces True.
Scala's rules in this area are more pessimistic than perhaps they could be, but they do still apply. Specifically, the following two rules are in play:
- If two expressions are the same stable name (either a
valor a parameter), or if they are stable references to the same stable name, they are considered equivalent - If two expressions are the same primitive literal value, they are considered equivalent
Another way of looking at this is that Scala is capable of testing runtime expression equivalence through the E-Var and E-Primitive rules (for each primitive), and not through anything else. Extension mechanisms such as macros can enhance this equivalence mechanism considerably, vastly widening the set of evaluation rules which may be considered (see: fthomas/refined).
The critical point though is that the mechanism exists and is part of the type checker, despite the fact that it is (out of the box) only limited to two evaluation forms. The fact that all other evaluation forms are considered "not equal" is beside the point: no inductive language can decide expression equivalence for all evaluation forms.
Thus, it is accurate to call Scala a "dependently-typed language", though it would also be accurate to say that its mechanisms for dependent-typing are extremely limited (two forms!) and also very unpleasant to work with.