It was early 2013. I just dropped out of college. I gathered my friends to start building a game for iOS. We were not great at it, and eventually the project fell apart. Among many completely unimportant things that nonetheless bugged my mind was one unsatisfaction with the type system of Objective-C or any other language I knew at the time. It took me more than 10 years to untangle this problem and unexpectedly find a solution in the middle of the night.
The problem that my formalism-obsessed brain noticed can be stated this way: We have a 2D world where our protagonist moves. To describe its position, we define a 2D vector type. But how do you capture the fact that this vector is related to this particular world and not some other graphics system’s plane or some unrelated coordinate system? From this question, you might figure I was the kind of software engineer who prematurely worries about all the completely unimportant things. I do somewhat better nowadays, thank you.
The way it is stated, the problem is not worth the effort to invent any solution. What it does is open a peephole into the universe of similar problems in software engineering. So, let’s explore an array of increasingly sophisticated problems and see if any type system offers a solution.
Lambda cube
To arrange known type systems in a structure, Henk Barendregt introduced the lambda cube. Its vertices are known type systems. Moving along the edges of this cube adds abstractions to the type system. Half of this cube can be observed in popular contemporary programming languages. So that is where we will begin.
Problem statement
The idea could very well be translated into any field. But for the sake of clarity, I have to pick some specific case. Imagine you’re building a simple image manipulation program, similar to Microsoft Paint. Such a program might have many types that it works with, but I will talk about only a particular subset: pairs of coordinates. Such a type is used for so many things including the obvious—point on a canvas—but also: mouse pointer position relative to window, relative to screen.
Base
The base case of a type system can be observed in languages like Pascal. It is known as simply typed lambda calculus. It allows for functions on values but not on types. Let’s see how such a type system helps us in our case. For clarity the code is in C++.
struct point { int x; int y; }Such a type already has a flaw: it is ambiguous on what the coordinate system is in the very general sense. Let’s make it a bit better:
struct point { unsigned int left; unsigned int top; }Now we can declare procedures that work with this type.
void drawPoint(point canvasPoint, color pencilColor);
point canvasPoint(point mouseWindowPoint);
void canvas_MouseClick_Handler(point mouseWindowPoint);You might be able to see the problem here. The type allows for a naïve mistake:
void canvas_MouseClick_Handler(point p) {
drawPoint(p, c);
}It is a good idea to use type system to check for this kind of mistakes:
struct canvasPoint: point {}
struct windowPoint: point {}
struct screenPoint: point {}Now procedures’ signatures can be changed:
void drawPoint(canvasPoint p, color pencilColor);
canvasPoint canvasPoint(windowPoint mouse);
void canvas_MouseClick_Handler(windowPoint mouse);This was a simple stuff. Though some developers might be reluctant to building such an elaborate tree of types, it obviously gives some useful compile-time checks without any runtime overhead. Let’s not waste any more time here and travel further on our lambda cube.
Polymorphism and generic types
It is a well established abstraction now but it has to be mentioned that Lambda cube distinguishes the two modifications of type system: adding terms that depend on types—polymorphism—and adding types that depend on types—generic types.
One trick that some of you might not expect is to use generic type to distinguish types of coordinates for our program. You might think of something like this:
template <typename T>
struct point { T left; T top; }Here you see a type that is parametrized over format of coordinates. But instead I would like you to consider this:
template <typename T>
struct point { unsigned int left; unsigned int top }
typedef point<Screen> screen_point;
typedef point<Window> window_point;
typedef point<Canvas> canvas_point;Now, you see, it is a type of point that can be parametrized over where it could be used. This way point on a screen could not be used where point inside canvas is expected.
If only this trick would allow us to also distinguish between points inside different windows. For that we will explore another face of Lambda cube in part 2.
Slash_Three 