What is the relation between syntax and type theory?

Question

Type theory and syntax are similar, in that they are inductive rules that determine whether a particular string of symbols is "correctly specified" in some sense.

There is a difference between syntax and type theory. Syntax in programming languages for example, concerns things that do not concern type theory, such as the fact that the statement if import microsoft.(false ==== 5) then import is "syntactically nonsense". This is not a type error, but a syntax error.

But I'm unsure what the relation is.

I normally think of syntax and type systems as follows: Let $L$ be the set of possible strings of some symbol set $S$. A particular syntax inductively specifies a subset $T\subseteq L$ of "terms" in $L$. e.g. a program is not well-specified if it is not in $T$. A particular type system then makes an additional restriction, by inductively specifying a subset $W\subseteq T$ of "well-typed terms".

But given such a syntax and type system, we can always consider a new syntax which is simply the old syntax plus also has the inductive rules of the type system as an additional restriction.

Therefore it is not clear to me why there is a fundamental difference between a syntax and a type system.

Is my intuition correct? Can we see type checking a particular form of syntax checking?

Answer 1

The division line between syntax and additional type checking can indeed be blurred, if so desired, but usually we make a distinction as follows:

• the syntax is described using a formal grammar, preferrably one that is not very complex, such as a context-free gramar, or one that is even simpler than that.

• the typing rules are described using inference rules whose complexity tyically exceeds that of a context-free formal grammar.

In general, a programming language might stratify the task of getting from the source code to the compiled code as follows:

1. Parsing converts the input string to an abstract syntax which represents the input as a tree.

2. Elaboration performs certain simple transformation of input syntax, such as getting rid of syntactic sugar.

3. Type-checking and inference verifies that the program is well-typed, thereby guaranteeing that later stages will not get stuck. It may also augment the input source with extra information about types.

4. Several phases of compilation may follow, each translating from its input to a simpler language. The final language may be machine code, or byte code, or in general some intermediate code.

5. The program is executed.

While you may consider merging some of these phases together, and sometimes that is a good idea, it is in general better to keep them separate. From a conceptual point of view parsing is very different from type checking. After all, these two phases serve different purposes: one is just a translation from strings to trees, while the other one statically analyzes the structure of the program in order to detect possible errors and to aid further compilation.

An example of merging different phases is "just in time" compilation: we run a program in an "interpreted" mode so that there is no delay because of compilation, and at the same time we perform on-the-fly compilation of those parts of the code in which the program is spending most of the time. I believe some browsers do that with Javascript.