# 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? – Andrej Bauer 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? – Andrej Bauer 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