# Is type-checking “syntactic” or “semantic”?

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?

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.

(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 it’s inferences with what the programmer asserts to be true.

• What is your definition of semantics that makes you classify type checking as semantics? Is there actually a well-defined distinction between syntax and semantics? – user56834 Dec 29 '19 at 14:26
• @user56834 of course there is; I’m not operating from formal definitions at the moment, but: a syntactically well-formed program is one whose representation (e.g., code) belongs to the language of (textually) valid programs. These are often languages decided by a context-free grammar, though need not be. Syntax has everything to do with the text itself, to me. A semantically well-formed program, otoh, is one about which we can prove certain formal properties that we have decided make programs valid; the list in the quote you gave has examples. It has to do with properties of the code’s meaning – D. Ben Knoble Dec 29 '19 at 14:32