1
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • $\begingroup$ What is the question? $\endgroup$
    – Andrej Bauer
    Jan 17, 2014 at 20:04
  • $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Jan 17, 2014 at 20:05
  • $\begingroup$ *"What is the relation between a type system and a program?" is much too broad of a question. $\endgroup$
    – D.W. ♦
    Jan 17, 2014 at 22:21

2 Answers 2

Reset to default
3
$\begingroup$

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!

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ Maybe it is better to explain what is "well-typed". I think maybe he is missing the point of being well-typed programs. $\endgroup$
    – alim
    Sep 22, 2017 at 8:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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