More Types

← → November 15, 2016

In the last chapter, we looked at the evaluation semantics of symbolic computation – how to evaluate expressions down to values. We saw that we could go in either direction – replacing values with expressions that evaluated to them, and simplifying expressions closer to their values. Now that we are armed with the basics of working with symbolic computation, we’ll look at moving our constructions on annotations into constructions on types.

Recall that we decided to use values and types as “primitives” in our new system of symbolic computation. What this means is that values and types are fundamental, not just some janky thing tacked on as we went with machine diagrams to express more power as we needed it. The idea is that the rules behind our types (collectively know as our type system) are powerful enough for anything we’d ever possibly want to do with them. In fact, we’ll show a little later that our type system is just as powerful (what does this mean?) as the values and computations they annotate.

It is for this reason that we are spending so much effort on developing our type system. While it is hard to believe right now, our type system will eventually be where we’ll be doing the majority of our reasoning. Our type system will be so powerful that for the most part, there will only ever be a single (easily found) machine that can possibly have that type.

The idea is that the more powerful our type system is, the more nuanced things we can say with it. In the same way that there’s only one person you think of given a description of a “jolly old man, who wears red, gives presents away once a year, and lives in the northern hemisphere”, with a little practice you’ll only be able to see a single machine whose type is : a -> b -> a.

As a little inspiration, if you, gentle reader, have managed to get this far in the book, and still consider yourself to be a “non-technical” type, take heart! Reasoning by way of the type system is indeed a powerful art, and one that most professional computer scientists have yet to come across, let alone master. Unfortunately for them, this is a skill that would make their day-to-day jobs tremendously easier, if only they knew it. I tell you this not to belittle them, but to inspire you. It’s not a particularly difficult topic, and if you can manage to hold on just a little longer, you’ll have the tools under your belt in order to compete with the best of them I tell you this not to belittle them, but to inspire you. It’s not a particularly difficult topic, and if you can manage to hold on just a little longer, you’ll have the tools under your belt in order to compete with the best of them. This is absolutely not hyperbole.

Product Types

The first construction on types we’ll revisit is the product type. A product type is what you get if you are audacious enough to “glue” two types together. We’ve already seen an example of a product type, :2 in our multiwire annotations, which corresponded to the type (Bool, Bool). We used the same notation when describing annotations, so none of this should be revelationary new material to you,

Conceptually, (Bool, Bool) is two booleans glued together, but allowing either of them to vary independently of the other. The product of Bool with Bool, as we have seen, has four values:

(Off, Off) : (Bool, Bool)
(Off, On ) : (Bool, Bool)
(On, On ) : (Bool, Bool)
(On, Off) : (Bool, Bool)

A neat fact is that a product is formed by gluing two types together, and that a product of two types is itself a type. This means that we can glue products together indiscriminately. For example, we can make ((Bool, Bool), Bool), by gluing a (Bool, Bool) together with a Bool. There are exactly eight values with this type:

((Off, Off), Off) : ((Bool, Bool), Bool)
((Off, On ), Off) : ((Bool, Bool), Bool)
((On, On ), Off) : ((Bool, Bool), Bool)
((On, Off), Off) : ((Bool, Bool), Bool)
((Off, Off), On ) : ((Bool, Bool), Bool)
((Off, On ), On ) : ((Bool, Bool), Bool)
((On, On ), On ) : ((Bool, Bool), Bool)
((On, Off), On ) : ((Bool, Bool), Bool)

In general, a product of (m, n) (for any types m and n you choose), has a number of values equal to the number of values m has, times the number of values that n has. That’s why when we take the product of Bool (two values) with itself, we get four values. In some sense, then, the product of two types can be considered a form of “multiplication” between two types. In fact mathematicians sometimes use the word “product” to mean “multiplication”.

This is just the first in a long string of spooky coincidences between grade-school arithmetic and the dark mysteries behind computation.

As a good rule of thumb, you should associate a product type with the idea of “and”, as in, if you need one type and another, what you really are looking for is a product of the two. Or three. Or four.

Speaking of taking products of more than two types, it’s informative to note that it doesn’t matter in which order you multiply the numbers from left to right or from right to left – \(2\times (3\times 4) = (2\times 3)\times 4 = 24\). Because of this fact, we’re allowed to drop the parentheses when multiplying several numbers together: \(2\times 3\times 4 = 2\times (3\times 4) = (2\times 3)\times 4 = 24\), and because of that fact, we can safely conclude that parentheses don’t matter when writing out product types. That is to say that ((Bool, Bool), Bool) is the same type as (Bool, (Bool, Bool)), which then must be the same as (Bool, Bool, Bool) for exactly the same argument as in our multiplication example.

The Unit Type

Are you as tired of reading about Bools as I am writing about them? Let’s spice up our type ecosystem a little, even if it’s with an unbelievably dull type. Say “hello” to what might be the silliest type:

type Unit = Unit

This should be read as “Unit is a type with one value, also called Unit”. Naming the type and its value both Unit seems like an odd choice – like it’s prone to lead to misunderstandings. When I say Unit, how do you know whether I’m talking about the type or the value?

Good news! It doesn’t matter. Because Unit is a type with only value, and all values must uniquely belong to a single type, this means whenever we have a Unit value, its type must be Unit, and whenever we have the type Unit, we know what its value must be. There’s no room for error, because there’s no room for choice. It’s kind of zen if you think about it.

So what’s Unit good for, if it presents no choices? Well, nothing really. Unit represents knowledge you already know. It’ll come into play in a second, but only in the sense that it allows us to build things that aren’t Units.

Note that because multiplying anything by 1 results in the thing you started with, taking a product with Unit doesn’t do anything. You can take products with Unit until the cows come home – (Bool, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit, Unit) is literally exactly the same thing as just a lonely Bool.

Sum Types

If product types should remind us of and, the curious reader will wonder what kinds of types reminds us of or. Sum types are the answer to that question.

Intuitively, a sum type is asking “do I have something of type a, or something of type b?” Let’s take a look at an example to help drive the point home.

type Strange = CouldBe   Bool
             | Otherwise Unit

Such a strange thing should be read as so: “Strange is a type whose values might be Bools, or they might be Unit. If they’re Bool, we’ll prefix them with CouldBe, and if they’re Unit we’ll prefix them with Otherwise”.

We’ll dig into this in a second, but sometimes a list of values is worth a thousand words.

CouldBe On : Strange
CouldBe Off : Strange
Otherwise Unit : Strange

This list comprises all of the values of type Strange. We need to use the prefixes to distinguish values inside a sum type from their counterparts outside of them. For example On is of type Bool, but CouldBe On is of type Strange. Remember, all values must be of a single, unique type. And so without these prefixes, we’d be unable to distinguish between a Bool and a Strange when talking about values.

Going forward, we will call these prefixes as value constructors, because they construct values of the sum type out of values from the type being summed.

If you’re quick, you’ve probably noticed that Strange has three values, and is a sum of a type with two values, and a type with one value. Indeed, calling such a thing a “sum type” is particularly telling. As an exercise, determine if sum types always add together the values of their underlying types.

An interesting thing to note is that sum types and Unit are somehow more parsimonious than Bools. Consider this alternative definition of Bool:

type AlternateBool = SumOn  Unit
                   | SumOff Unit

Because we’ve shown earlier how knowing something is Unit tells you no more than you knew before, so this definition is equivalent to having dropped the Units altogether. As such, we can reason that Bool is nothing more than a sum of Unit with itself, where all of the information being stored about values comes from the value constructors themselves.

Void

We have one more “interesting-not-interesting” type to look at today. Notice that there is nothing that stops me from making a “group” containing all of the federal holidays on which there is a tradition to give me billions of dollars worth of gifts. This doesn’t mean that such a group contains any actual holidays

Likewise, we can declare a type which has no values. Such a thing is usually called Void, and is declared like this:

type Void

Notice how there is no equals sign after this. We’re saying that there is such a thing as a Void type, but haven’t listed any values for it.

A quick aside to programmers: if you’re familiar with the void “type” in languages like C, Java or similar languages, the thing you call void is not the same as this Void type we have just declared. What you call void is in fact the Unit type. There is no such thing as a real Void in most programming languages. End aside.

Maybe you can squint and see how Unit is a useful type, but even then, it’s certainly going to be a strain to see how Void could possibly be useful. It’s not really.

Void’s main purpose is for filling out our roster of “interesting” types. In many ways, it’s a counterpart to Unit. Because Void has zero values, it has some interesting properties. The first is that any type summed against Void is equivalent to the type itself, since there is no way to ever get into the other value constructor. This is consistent with our understanding that sum is addition – adding 0 to any number is still the number you started with.

Additionally (no pun intended), Void interacts strangely with product types. Because product types multiply values, taking a product with Void is always just Void. Why is this? Well in order to construct a product value, you need a value from each of the component types. But there are no values of Void, so you can’t get one, so you can’t construct any values of the product type.

And so we can say that the relationship between Void and Sum is the same as that between Unit and Product, which is that “nothing happens when you combine them”.

But you might persevere – “what good is this Void thing?” It’s not really, for our purposes, but it will be in a few chapters when we decide to look at why our type system is powerful. As something to whet your appetite, try to find a machine that has this interface:

Hint: don’t look very hard.

In the next chapter we’ll look at how to represent polymorphism in our type system, and then get back to practical matters at hand and continue working towards building a computer.

Exercises

Work a few examples of sum types to prove to yourself that they add together the number of values in their component types.

← →