Is type-checking "syntactic" or "semantic"?

Question

On the wikipedia page on compilers, it says:

Semantic analysis adds semantic information to the parse tree and builds the symbol table. This phase performs semantic checks such as type checking (checking for type errors), or object binding (associating variable and function references with their definitions), or definite assignment (requiring all local variables to be initialized before use), rejecting incorrect programs or issuing warnings. Semantic analysis usually requires a complete parse tree, meaning that this phase logically follows the parsing phase, and logically precedes the code generation phase, though it is often possible to fold multiple phases into one pass over the code in a compiler implementation.

I was somewhat surprised that type checking is categorized as semantics rather than syntax. Usually my impression is that types are called syntactic objects. Is type checking syntactic or semantic?

Answer 1

Although I personally would describe type analysis as semantic, this question seems to start with the assumption that there is a clear, formally-definable dividing line between "syntax" and "semantics".

I don't think that is the case; even if most of us would put type-correctness into one category and missing parentheses into the other one, there is a fuzzy area in the middle where the answer is much less clear.

Consider, for example, the common case of a language which requires identifiers to be declared in the scope in which they are used. Clearly, then, the following is an error: (leaving aside the precise syntax of the language)

function ilog2(a:int) => int
  if a > 0 then
    let log:int = 0
    while a > 1
      a = a / 2
      log = log + 1
    end
  end
  return log
end

Many people would argue that the use of log in the return statement is a semantic error, since it has to do with the set of definitions in the outer scope of the function. On the other hand, it is quite feasible to construct a grammar (not a context-free grammar, but a grammar nonetheless) which rejects this program. It's not a coincidence that this scoping rule is called "lexical scoping" rather than, for example, nested semantic scoping.

A context-sensitive grammar can accomplish that in a straight-forward fashion by scanning backwards (and forwards, if declarations are allowed to follow use) skipping over inner scopes until it finds a declaration for the used identifier. Of course, that's not a very efficient algorithm but it's reasonable to assume that there are more efficient ways to implement such a grammar.

Even more generally, in the lengthy discussions which lead to the formalism of Algol 68, Adriaan van Wijngaarden proposed a syntactic formalism (link taken from this Wikipedia article) powerful enough to not just encompass declarations, but also to encompass static type checking. Although not everyone will agree with the judgement, van Wijngaarden's proposal was considered readable enough that it was eventually used in the formal definition of Algol 68. In that definition, type agreement (other than discriminated unions) is guaranteed by the grammar, while semantics is reserved for questions like the precise meaning of the + operator.

In retrospect, Van Wijngaarden's formalism turned out to be far too powerful to allow for automated parser generation, but it did spawn a number of simplified and less powerful formalisms, collectively called "attribute grammars", which have the potential to expand the formal power of syntactic descriptions while remaining practical tools for compiler writers. (There are few practical demonstrations, but there is still hope. :-) )

In short, if you consider "syntax" to be intimately linked to a particular syntax formalism (and hence to a particular parsing algorithm), then you will probably be able to make a clear distinction between syntax and semantics, but it might turn out to be a different distinction made by someone using a different parsing algorithm. So it's hard to see how write universal and non-overlapping definitions of syntax and semantics.

Answer 2

(From my limited experience) I would certainly call type-soundness a semantic property of a program, rather than a syntactic one.

In some dynamic languages (e.g., lisp, python sans type annotations & mypy, etc.), there is no syntax for types (and the semantic verification of type soundness is done at runtime in these languages).

In some static languages (such as SML), one can omit almost all syntactic type information; the program fails to compile if it does not type check. This is a semantic analysis because it requires type-inference, and there are not (necessarily) types in the text of the program. Of course, the programmer can (and arguably should) add type information to parts of the program; the same type-checker attempts to unify its inferences with what the programmer asserts to be true.

Answer 3

Terms such as "syntax", "semantics", and "pragmatics" were borrowed from linguistics. Linguists are trying to understand a natural phenomenon: human language. Theories about grammar and denotation are models of that natural phenomenon.

Computer scientists are not so constrained, in that their job (in this context) is to define artificial languages formally such that both humans and machines can understand them.

The job of lexical analysis, syntax analysis, and semantic analysis (wherever you draw the line) is to limit the number of valid program texts from $\Sigma^*$ down to whatever strings make sense. Where you draw the line is somewhat arbitrary.

I suspect that the question is really about how errors are reported, and this is something that distinguishes natural languages from programming languages.

Error reporting is a neglected area of language design, and is usually treated as an implementation detail. Programmers spend a lot of their time reading messages from a compiler explaining why their alleged program is not valid, so this is probably the most important part of the user interface of a compiler.