# How is a type system related to a progam?

Lambda calculi of various forms are formal systems. They consist of abstract syntax (for terms and for types, if present), judgments (typing judgments and equations), and rules of inference. They are not programming languages (unless we prescribe operational semantics) and neither is it the case that a type system equals a program that checks types. So I think this whole question is a bit misdirected, still. Of course, an important aspect of a type system is how to implement it on a computer, which brings in questions about algorithms, etc. But a priori, the type system has none of that.

I understand most of this, but I cannot wrap a logical understanding around:

neither is it the case that a type system equals a program that checks types.

My understanding of a type system is that it is a set of rules in a formal system used to determine if a type is valid in a context and that those rules, via implementation, are used to establish the validity of a use of a type in a context in a programming language.

However the statement has me thinking there is no connection, or that there is more meaning to the statement but I don't see the details to separate a type system from a program or make a logical connection between the two so that the statement makes sense.

What is the relation between a type system and a program?

• What is the question? Jan 17 '14 at 20:04
• Given that $\lambda$-calculus predates programming by some decades, how can it be suprising that there is more to $\lambda$-calculi than type checking in a programming language? Jan 17 '14 at 20:05
• *"What is the relation between a type system and a program?" is much too broad of a question.
– D.W.
Jan 17 '14 at 22:21

Your understanding that a type system is a set of rules in a formal system is right, but the rest is a bit garbled. The purpose of the type system is to delineate which terms or programs make sense. It is up to the language designer to decide which programs "make sense". There is no claim that the language specifies all programs that make sense. When somebody proposes a new type system, they are saying, "here are more programs that make sense and our type system captures them."

Andrej is saying one shouldn't equate the type system with the type checker (which is a program).

There is nothing too deep about it. Merely that the type system, i.e., the set of rules, stand independently of any particular implementation. One could even devise type systems that are undecidable, i.e., no possible type checking program exists. Admittedly such type systems may not be of much practical use, but nobody denies that they are type systems in the first place!

The relation between a type system and a program: A type system determines which programs are well-typed.

If that's not the answer you were looking for, you'll need to do a better job of posing the precise question that you want answered.

• Maybe it is better to explain what is "well-typed". I think maybe he is missing the point of being well-typed programs.
– alim
Sep 22 '17 at 8:42