Back in Business and Better than Ever

← → November 17, 2016

In the last few chapters, we’ve been building something I like to call “higher-order machinery” – things that are not machines themselves, but are useful for building machines. The majority of our higher-order machinery took the form of developing our type system – a framework we’ve built in order to describe the interfaces to our machines, and to help us reason about how we can connect machines together. As we saw in the last chapter, having a developed type system also afforded us the capability to make more semantically meaningful machines.

We’ve taken quite a detour, but it’s finally time to get back to our stated task at hand: building a computer. Before we get started in earnest, let’s begin by moving all of our existing machinery from machine diagrams to symbolic computations. We’ll quickly work our way back through the material we’ve already covered. Try to follow along with each construction, and if you feel up to the challenge, try your hand at converting one on your own.

Simple Adding

The first interesting machine we made was Add, a machine which added three wires together, and output both the “sum” and the “carry” of those three wires.

add1 : Bool -> Bool -> Bool -> (Bool, Bool)
add1 a b cin = (sum, carry)
  where
    sum   = xor (xor a b) cin
    carry = or (or (and a b)
                   (and a cin))
               (and b cin)

How much easier was that than our machine diagrams? It takes a little chasing to keep everything in your head, but you have to admit it certainly takes up less space.

I pulled a fast one on you there – did you see it? I said that add1 a b c = (sum, carry), but what are sum and carry? Keep looking! They’re defined right afterwards. This convention bears a little explaining, so I’ll get to it. But I promise to keep it short.

In order to simplify our symbolic computations, we can abstract away complicated patterns and give them a more meaningful name. The way we do this is by writing equality definitions after the word where. Everything in this “where block” has access to the function’s bindings (in this case a, b, and cin), so all of the as (for example) refer to the same input value coming into the add1 machine.

The carry expression, however, is a bit of a doozy. Whenever possible, I will attempt to line up sub-expressions so that it’s clear what’s going on without needing to count parentheses. This extra spacing has absolutely no meaning in the symbolic computation whatsoever, it’s entirely to aid human comprehension. An interesting question is a “who would be comprehending this, if not humans?” and the answer, of course, is that before the end of this book, we will have “closed the loop” and have written a computer program capable of “understanding” the exact symbolic computations that make it up. But we’re not there yet.

Adding Nybbles

Let’s move forwards and work on migrating our Add4 machine to a symbolic computation. Recall that Add4 was four Add machines running in “parallel”, each one receiving the “carry” output from the previous machine.

type Nybble = (Bool, Bool, Bool, Bool)

add4 : Nybble -> Nybble -> Nybble
add4 (a1, a2, a3, a4) (b1, b2, b3, b4) = (s1, s2, s3, s4)
  where
    (s1, c1) = add1 a1 b1 Off
    (s2, c2) = add1 a2 b2 c1
    (s3, c3) = add1 a3 b3 c2
    (s4, c4) = add1 a4 b4 c3

Before we start with the analysis, let’s take a look at a little more notation first. We have this definition in our “where block”: (s1, c1) = add1 a1 b1 Off, which uses a technique we’ll call destructuring or pattern matching. Destructuring makes bindings to “smaller pieces” of a large value. Because the output of each invocation of add1 is a product type, we somehow need to pull out the individual Bools inside of that type. This is exactly what destructuring does.

We’re also pulling apart the products of Bools as our inputs to add4, because we’ve said that add4 takes Nybbles, and that type Nybble = (Bool, Bool, Bool, Bool). So the way you should read all of this is that add4 tears apart the individual Bools it’s given, pairs each of them up, moves the “carries” between add1 machines, and then gives you back a product of the “sums”.

Notice how closely all of this logic reflects the original machine diagram:

However, if you’ll recall, the complexity of this diagram the first time around gave us the willies and was the inspiration behind our developing of the multiwire concept.

Indeed, our symbolic computation for add4 is itself pretty hairy, and very mechanical. You can imagine we might want to make an add8, and while there’s nothing difficult about constructing such a machine, it would certainly be tedious and error-prone.

Types to the Rescue

We solved this problem the first time around by using multiwires, and (although we didn’t know it then) using polymorphism. We said that the semantics of two multiwires with the same annotation (ie. two values with the same type) being expanded into a single machine would “make a copy” of the machine for each wire in the multiwire. To refresh your memory, we drew this diagram:

So how can we do this with a symbolic computation? Well, polymorphism is the first thing that comes to mind. It solved our problem last time, so it’s a reasonable thing to try here.

Unfortunately, there’s a problem, and that’s that our new type system is stronger than the notion of annotations on multiwires. A “polymorphic” multiwire was a multiwire where we didn’t care how many wires were in it. However, as we’ve seen, there are more types than just Bool and products of Bool, so when we say “a polymorphic type”, we have far more possibilities than we ever did for “polymorphic multiwires”.

In other words Maybe Nat is a valid instance for a type variable, but Maybe Nat is not a valid multiwire.

At the end of the day, what this means is that using any particular type is too specific in order to define an add machine that works for any size of inputs, but a polymorphic type is too general. What we really want is some restriction on which polymorphic types we’re allowed to use.

Or, maybe what we want is a polymorphic type which describes exactly what we need. Let’s take a look at what we can come up with.

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

How should this be interpreted? Well, we can read it like so:

List a is a type, polymorphic in a, whose values are either Nil (nothing; an empty list) or a Construction of an a combined with some other List a.

Similarly to Nat, List a is defined in terms of itself. Let’s look at a few values of type List Bool to get a feel for this new type of ours.

Nil : List Bool
Cons On Nil : List Bool
Cons Off Nil : List Bool
Cons On (Cons On Nil) : List Bool
Cons On (Cons Off Nil) : List Bool
Cons Off (Cons On Nil) : List Bool
Cons Off (Cons Off Nil) : List Bool
… and so on

At its essence, a List a is nothing but some number of as glued together into a product. The “some number” part of that description is the important part – this is exactly the semantic we want for our add machine!

Adding Lists

We now have all the tools necessary for describing add. We’ll start with its type annotation:

add : List Bool -> List Bool -> List Bool

This is very reminiscent of add1 : Bool -> Bool -> Bool and add4 : Nybble -> Nybble -> Nybble, which is a good sign. Based on syntactical evidence alone, so far we have yet to go wrong. We’ll continue. What we want is a way to “peel” off the first element in each list, and use those values as inputs to add1.

add : List Bool -> List Bool -> List Bool
add (Cons a as) (Cons b bs) = something

We use pattern matching (aka. destructuring) to pull off the head (first thing) of each of our lists. However, once we have taken off the heads, we are left with the “tails” – the remainder of the things in the list, although this might be Nil if the list only had one element in it to begin with. We bind the heads of the lists to a and b, and the tails of the lists to as and bs, which should be pronounced like the plurals of “a” and “b”.

We’d like to pass a an b directly into add1, but there’s a problem, and that’s that we don’t yet have a cin. Unfortunately, we don’t have an obvious place to pull one in from, so we cheat and make a lemma machine, one that takes a cin as input:

add' : List Bool -> List Bool -> Bool -> List Bool
add' (Cons a as) (Cons b bs) cin = something
  where
    (sum, carry) = add1 a b cin

We’d now like to output add1 a b cin, but we can’t! Why not? Because it doesn’t have the correct type! We want to output a List Bool, but the only List Bools that we have are as and bs, and we haven’t actually done anything with those, so they are unlikely to be the “correct” thing to give back.

Looking at our old machine diagram again provides a clue for what to do:

You’ll notice that there is a wire connecting the output of Add to the input of Add. If we look back at the tools we have available to us in add' to produce a List Bool, we notice that add' itself outputs a List Bool. And so that’s where we’re going to get ours from.

add' : List Bool -> List Bool -> Bool -> List Bool
add' (Cons a as) (Cons b bs) cin = Cons sum (add' as bs carry)
  where
    (sum, carry) = add1 a b cin

Hold on. What? Well, we compute add1 a b cin, and then take the sum of that, and Construct it with the result of calling add' as bs carry. This has the effect of “peeling off” one Bool at a time from our List Bools. It computes the sum and carry of adding them together, uses the sum as a part of the output List Bool, and uses the carry as the cin for the next time around.

The clever reader will be wondering “how does this thing ever stop?” The answer of course is “when we run out of inputs”, but the clever reader is correct – our solution so far doesn’t yet cover that. Recall that when we make a function table, we need to describe the output for every possible input. But we haven’t yet described what happens if you have an empty list. In that case, obviously we won’t have one of the wires we need to compute an add1, so the only meaningful List Bool we can give back is Nil. Capiche?

Our final solution, then is:

add' : List Bool -> List Bool -> Bool -> List Bool
add' (Cons a as) (Cons b bs) cin = Cons sum (add' as bs carry)
  where
    (sum, carry) = add1 a b cin
add' _ _ _ = Nil

This final line full of underscore says “for any other input, we just want to give back Nil.” Remember that our original Add4 machine simply “dropped” the final carry, and we decide to do that here as well. It’s probably poor mathematics, but we’re worried more about consistency right now.

To now tie a pretty bow around the whole thing, we remember that this add' machine is a lemma, and in fact what we wanted was in fact add. We can define add in terms of add':

add : List Bool -> List Bool -> List Bool
add as bs = add' as bs Off

where we just supply the initial cin binding for add'.

It’s crazy to believe, but all of this stuff we’ve made actually works! add is now a general purpose adder – capable of computing sums of numbers arbitrarily large.

In the next chapter, we’ll do a few more examples of moving our machine diagram circuitry into symbolic computations.

Exercises

Evaluate the expression add (Cons On (Cons Off Nil)) (Cons On (Cons On Nil)) by hand to get a feel for how this construction actually works.

← →