In another question about Lambda Calculus, Andrej Bauer made the comment: Lambda

Question

In another question about Lambda Calculus, Andrej Bauer made the comment:

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?

Explanation / Answer

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!

Related Questions

Navigate

• Browse (All)
• Browse I
• Subjects

Integrity-first tutoring: explanations and feedback only — we do not complete graded work. Learn more.