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?


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.

  • $\begingroup$ Two questions: (1) if I understand from your answer, it is correct that we COULD formulate a formal grammar that has the type system incorporated in it, so that type checking is done DURING parsing. Is that right? And (2) if it is right, then I don't understand your statement that "From a conceptual point of view parsing is very different from type checking". $\endgroup$ – user56834 Apr 22 at 20:20
  • $\begingroup$ Formal grammars are defined so that it may take an arbitrary Turing machine to recognize a language (the so-called Type 0 grammars of Chomsky hierarchy). So essentially you can stick whatever you like into a grammar. However a grammar only recognizes whether a given string belongs to a language (it builds the parse tree), whereas the type-checking phase may compute additional data (types of expressions and other annotations of the code) in addition to accepting/rejecting a program. $\endgroup$ – Andrej Bauer Apr 22 at 20:35
  • $\begingroup$ And most importantly, from an engineering point of view, it is a bad idea to try to perform type checking during parsing. This will lead to convoluted and inflexible code, bugs, and general increase in the entropy of the universe. $\endgroup$ – Andrej Bauer Apr 22 at 20:36
  • $\begingroup$ In practice, most parsers work on type 2 grammars, leaving anything that requires context or memory for a later pass. Type 0 and 1 grammars are not very convenient. That would include, for example, type unification. $\endgroup$ – rici Apr 22 at 22:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.