What is a type system?

Question

Background

I am designing a language, as a side project. I have a working assembler, static analyser, and virtual machine for it. Since I can already compile and run non-trivial programs using the infrastructure I've built I thought about giving a presentation at my university.

During my talk I mentioned that the VM provides a type system, was asked "What is your type system for?". After answering I got laughed at by the person asking the question.

Thus, even though I am almost certainly going to lose reputation for asking this question, I turn to Programmers.

My understanding

As I understand them, type systems are used to provide additional layer of information about entities in a program, so that the runtime, or the compiler, or any other piece of machinery, knows what to do with the strings of bits it operates on. They also help maintain contracts - the compiler (or code analyser, or runtime, or any other program) can verify that at any given point the program operates on values programmers expect it to operate on.

Types can also be used to provide information to those human programmers. For example, I find this declaration:

function sqrt(double n) -> double;

more useful than this one

sqrt(n)

The former gives plenty of information: that the sqrt identifier is a function, takes a single double as input, and produces another double as output. The latter tells you that it is probably a function taking a single parameter.

My answer

So, after being asked "What is your type system for?" I answered as follows:

The type system is dynamic (types are assigned to values, not to variables holding them), but strong without surprising coercion rules (you can't add string to integer as they represent incompatible types, but you can add integer to floating point number).

The type system is used by the VM to ensure that operands for instructions are valid; and can be used by programmers to ensure that parameters passed to their functions are valid (i.e. of correct type).
The type system supports subtyping and multiple inheritance (both features are available to programmers), and types are considered when dynamic dispatch of methods on objects is used - VM uses types to check by what function is a given message implemented for given type.

The follow-up question was "And how is type assigned to a value?". So I explained that all values are boxed, and have a pointer pointing to a type definition structure which provides information about name of the type, what messages it responds to, and what types it inherits from.

After that, I got laughed at, and my answer was dismissed with the comment "That is not a real typesystem.".

So - if what I described does not qualify as a "real typesystem", what would? Was that person right that what I provide cannot be considered a typesystem?

Answer 1

That all seems like a fine description of what type systems provide. And your implementation sounds like a reasonable enough one for what it's doing.

For some languages, you won't need the runtime information since your language doesn't do runtime dispatch (or you do single dispatch via vtables or another mechanism, so don't need the type information). For some languages, just having a symbol/placeholder is sufficient since you only care about type equality, not its name or inheritance.

Depending on your environment, the person may have wanted more formalism in your type system. They want to know what you can prove with it, not what programmers can do with it. This is pretty common in academia unfortunately. Though academics do such things because it's pretty easy to have flaws in your type system that allow things to escape correctness. It's possible they spotted one of these.

If you had further questions, Types and Programming Languages is the canonical book on the subject and can help you to learn some of the rigor needed by academics, as well as some of the terminology to help describe things.

Answer 2

I like @Telastyn's answer especially because of the reference to academic interest in formalism.

Allow me to add to the discussion.

What is a type system?

A type system is a mechanism for defining, detecting, and preventing illegal program states. It works by defining and applying constraints. The constraint definitions are types, and, the constraint applications are usages of types, e.g. in variable declaration.

Type definitions typically support composition operators (e.g. various forms of conjunction, as in structures, subclassing, and, disjunction, as in enums, unions).

The constraints, usages of types, sometimes also allow composition operators (e.g. at least this, exactly this, either this or that, this provided that something else holds).

If the type system is available in the language and applied at compile time toward the objective of being able to issue compile-time errors, it is a static type system; these prevent many illegal programs from compiling let alone running, hence it is preventing illegal program states.

(A static type system stops a program from running whether or not it is known (or undecidable) that the program will ever reach that unsound code it is complaining about. A static type system detects certain kinds of nonsense (violations of the declared constraints) and judges the program in error before it ever runs.)

If a type system is applied at runtime, it is a dynamic type system that prevents illegal program states: but by stopping the program in mid run, instead of preventing it from running in the first place.

A fairly common type system offering is to provide both static and dynamic features.

Answer 3

Oh man, I am excited to try to answer this question as best I can. I hope I can get my thoughts properly in order.

As @Doval mentioned and the questioner pointed out (albeit rudely), you do not really have a type system. You have a system of dynamic checks using tags, which is in general much weaker, and also much less interesting.

The question of "what is a type system" can be quite philosophical, and we could fill a book with different viewpoints on the matter. However, as this is a site for programmers, I'll try to keep my answer as practical as possible (and really, types are extremely practical in programming, despite what some may think).

Overview

Let's start with a seat-of-the-pants understand of what a type system is good for, before diving into the more formal underpinnings. A type system imposes structure on our programs. They tell us how we may plug various functions and expression together. Without structure, programs are untenable and wildly complex, ready to cause harm at the slightest mistake of the programmer.

Writing programs with a type system is like driving a care in mint condition - the brakes work, the doors close safely, the engine is oiled, etc. Writing programs without a type system is like riding a motor cycle without a helmet and with wheels made out of spaghetti. You have absolutely no control over your.

To ground the discussion, let's say we have a language with literal expression num[n] and str[s] that represent the numeral n and the string s, respectively, and primitive functions plus and concat, with the intended meaning. Clearly, you don't want to be able to write something like plus "hello" "world" or concat 2 4. But how can we prevent this? A priori, there is no method to distinguish the numeral 2 from the string literal "world". What we would like to say is that these expressions should be used in different contexts; they have different types.

Languages and Types

Let's step back a bit: what is a programming language? In general, we can divide a programming language into two layers: the syntax and the semantics. These are also called the statics and the dynamics, respectively. It turns out that the type system is necessary to mediate the interaction among these two parts.

Syntax

A program is a tree. Don't be fooled by the lines of text you write on a computer; these are just the human-readable representations of a program. The program itself is an Abstract Syntax Tree. For example, in C we might write:

int square(int x) { 
    return x * x;
 }

That is the concrete syntax for the program (fragment). The tree representation is:

     function square
     /     |       \
   int   int x    return
                     |
                   times
                  /    \
                 x      x

A programming language provides a grammar defining the valid trees of that language (either concrete or abstract syntax may be used). This is usually done using something like BNF notation. I would assume you've done this for the language you've created.

Semantics

OK, we know what a program is, but it's just a static tree structure. Presumably, we want our program to actually compute something. We need semantics.

Semantics of programming languages is a rich field of study. Broadly speaking, there are two approaches: denotational semantics and operational semantics. Denotational semantics describes a program by mapping it into some underlying mathematical structure (e.g. the natural numbers, continuous functions, etc). that provides meaning to our program. Operational semantics, on the contrary, defines a program by detailing how it executes. In my opinion, operational semantics are more intuitive to programmers (including myself), so let's stick with that.

I won't go through how to define a formal operational semantics (the details are a bit involved), but basically, we want rules like the following:

1. num[n] is a value
2. str[s] is a value
3. If num[n1] and num[n2] evaluate to the integers n_1$ and $n_2$, thenplus(num[n1], num[n2])` evaluates to the integer $n_1 + n_2$.
4. If str[s1] and str[s2] evaluates to the strings s1 and s2, then concat(str[s1], str[s2]) evaluates to the string s1s2.

Etc. The rules are in practice a lot more formal, but you get the gist. However, we soon run into a problem. What happens when we write the following:

concat(num[5], str[hello])

Hm. This is quite a conundrum. We have not defined a rule anywhere for how to concatenate a number with a string. We could attempt to create such a rule, but we intuitively know that this operation is meaningless. We don't want this program to be valid. And thus we are led inexorably to types.

Types

A program is a tree as defined by a language's grammar. Programs are given meaning by execution rules. But some programs are unable to be executed; that is, some programs are meaningless. These programs are ill-typed. Thus, typing characterizes meaningful programs in a language. If a program is well-typed, we can execute it.

Let's give some examples. Again, as with the evaluation rules, I will present typing rules informally, but they can be made rigorous. Here are some rules:

1. A token of the form num[n] has type nat.
2. A token of the form str[s] has type str.
3. If expression e1 has type nat and expression e2 has type nat, then the expression plus(e1, e2) has type nat.
4. If expression e1 has type str and expression e2 has type str, then expression concat(e1, e2) has type str.

Thus, according to these rules, there is plus(num[5], num[2]) is has type nat, but we cannot assign a type to plus(num[5], str["hello"]). We say a program (or expression) is well-typed if we can assign it any type, and it is ill-typed otherwise. A type system is sound if all well-typed programs can be executed. Haskell is sound; C is not.

Conclusion

There are other views on types. Types in some sense correspondg to intuitionistic logic, and they can also be viewed as objects in category theory. Understanding these connections is fascinating, but it is not essential if one merely wants to write or even design a programming language. However, understanding types as a tool for controlling program formations is essential to programming language design, and development. I have only scratched the surface of what types can express. I hope you think they are worthwhile enough to incorporate into your language.