Correct terminology in type theory: types, type constructors, kinds/sorts and values

Question

In an answer to a previous question, a small debate started about correct terminology for certain constructs. As I did not find a question (other than this or that, which is not quite the right thing) to address this clearly, I am making this new one.

The questionable terms and their relationships are: type, type constructor, type parameter, kinds or sorts, and values.

I also checked Wikipedia for type theory, but that didn't clarify it much either.

So for the sake of having a good reference answer and to check my own understanding:

• How are these things defined properly?
• What is the difference between each of these things?
• How are they related to each other?

Answer 1

Alright, let's go one by one.

Values

Values are the concrete pieces of data that programs evaluate and juggle. Nothing fancy, some examples might be

• 1
• true
• "fizz buzz foo bar"

Types

A nice description for a type is "a classifier for a value". A type is a little bit of information about what that value will be at runtime, but indicated at compile time.

For example if you tell me that e : bool at compile time, and I'll know that e is either true or false during runtime, nothing else! Because types classify values nicely like this, we can use this information to determine some basic properties of your program.

For example, if I ever see you adding e and e' when e : int and e' : String, then I know something is a bit off! In fact I can flag this and throw an error at compile time, saying "Hey, that doesn't make any sense at all!".

A more powerful type system allows for more interesting types which classify more interesting values. For example, let's consider some function

f = fun x -> x

It's pretty clear that f : Something -> Something, but what should that Something be? In a boring type system, we'd have to specify something arbitrary, like Something = int. In a more flexible type system, we could say

f : forall a. a -> a

That is to say "for any a, f maps an a to an a". This let's us use f more generally and write more interesting programs.

Moreover, the compiler is going to check actually satisfying the classifier we've given it, if f = fun x -> true then we have a bug and the compiler will say so!

So as a tldr; a type is a compile time constraint on the values an expression can be at runtime.

Type Constructor

Some types are related. For example a list of integers is very similar to a list of strings. This is almost like how sort for integers is almost like sort for strings. We can imagine a sort of factory that builds these almost-the-same types by generalizing over their differences and building them upon demand. That's what a type constructor is. It's kind of like a function from types to types, but a little more limited.

The classic example is a generic list. A type constructor for is just the generic definition

 data List a = Cons a (List a) | Nil

Now List is a function which maps a type a to a list of values of that type! In Java-land I think these are perhaps called "generic classes"

Type Parameters

A type parameter is just the type passed to a type constructor (or function). Just like in the value level we'd say foo(a) has a parameter a just like how List a has a type parameter a.

Kinds

Kinds are a bit tricky. The basic idea is that certain types are similar. For example, we have all the primitive types in java int, char, float... which all behave as if they have the same "type". Except, when we're speaking of the classifiers for types themselves, we call the classifiers kinds. So int : Prim, String : Box, List : Boxed -> Boxed.

This system gives nice concrete rules about what sort of types we can use where, just like how types govern values. It'd clearly be nonsense to say

 List<List>

or

 List<int>

In Java since List needs to be applied to a concrete type to be used like that! If we look at their kinds List : Boxed -> Boxed and since Boxed -> Boxed /= Boxed, the above is a kind error!

Most of the time we don't really think about kinds and just treat them as "common sense", but with fancier type systems it's something important to think about.

A little illustration of what I've been saying so far

 value   : type : kind  : ...
 true    : bool : Prim  : ...
 new F() : Foo  : Boxed : ...

Better Reading Than Wikipedia

If you're interested in this sort of thing, I'd highly recommend investing a good textbook. Type theory and PLT in general is pretty vast and without a coherent base of knowledge you (or at least I) can wander around without getting anywhere for months.

Two of my favorite books are

• Types and Programming Language - Ben Pierce
• Practical Foundations of Programming Languages - Bob Harper

Both are excellent books that introduce what I've just talked about and much more in beautiful, well explained detail.

Answer 2

How are these things defined properly?

They are properly defined by rigid, academic mathematical backing, providing strong assertions as to what they are, how they work, and what is guaranteed.

But programmers largely don't need to know that. They need to understand the concepts.

Values

Let's start with values, since everything builds from there. Values are the data used in computing. Depending on the approach, they're the values that everyone is familiar with: 42, 3.14, "How now brown cow", the personnel record for Jenny down in Accounting, etc.

Other interpretations of values are symbols. Most programmers understand these symbols to be the "values" of an enumeration. Left and Right are symbols for the enum Handedness (ignoring ambidextrous people and fish).

Regardless of the implementation, values are the different things that the language works with to perform calculations.

Types

The problem with values is that not all calculations are legal for all values. 42 + goat doesn't really make sense.

This is where types come into play. Types are metadata that define subsets of values. The Handedness enum above is a good example. This type says "only Left and Right may be used here". This allows programs to determine very early that certain operations will result in error.

Another practical use to consider is that under the hood, computers work with bytes. The byte 42 might mean the number 42, or it might mean the character *, or it might mean Jenny from Accounting. Types also (in practical use, not theoretical so much) help define the encoding for the underlying collection of bytes used by computers.

Kinds

And here's where we start going a little out there. So, when a programming language has a variable that refers to a type, what type does it have?

In Java and C# for example, it has the type Type (which has the type Type, which has... and so on all the way down). This is the concept behind kinds. In some languages, you can do a bit more useful things with a Type variable than Java and C#. Once that happens it becomes useful to say "I want a value that is a Type, but is also some kind of IEnumerable<int>". Ta-da! Kinds.

Most programmers can think of kinds like Java and C# generic constraints. Consider public class Foo<T> where T: IComparable{}. In a language with kinds, the T: kindOf(IComparable) variable declaration becomes legal; not just a special thing you can do in class and function declarations.

Type Constructors

Perhaps unsurprisingly, type constructors are simply constructors for types. "But how do you construct a type? Types just are.". Eh... not so much.

Also unsurprisingly, it's pretty difficult to build all of the different useful subsets of values any computer program will ever use. Type constructors work to help allow programmers to "build" those subsets in meaningful ways.

The most ubiquitous example of a type constructor is an array definition: int[4]. Here you're specifying 4 to the type constructor, which uses the value to build you an array of ints with 4 entries. If you specified a different input type, you'd get a different output type.

Generics are another form of type constructor, taking another type as their input.

In many languages there is a type constructor like P -> R to build a type that represents a function that takes type P and returns type R.

Now, the context will determine if a "function that returns a type" is a type constructor or not. In my (admittedly limited) experience, the line is "can you use this type at compile time?". Yes? Type constructor. No? Just a function.

Type Parameter

So you remember the parameters passed to Type Constructors? They're commonly known as Type Parameters, since the common form of a Type Constructor is Type[param] or Type<param>.