Algebraic Data Types in Swift

An algebraic data type is a type that’s the union of other data types. That is, it’s a type that may be one of several other types. Here’s how we would implement a linked list as an algebraic data type in Swift:

enum LinkedList<Element> {  
    case empty
    indirect case node(data: Element, next: LinkedList)
}

This defines an enum called LinkedList that might either be .empty or a .node that points to another LinkedList. There are three interesting things to note. The first is that we’ve created a generic data type, so the type of Element is declared by the consumer of LinkedList. The second is that the .node case uses LinkedList recursively, and must therefore be marked with indirect. The third is that since the .empty case has no parameters, the parenthesis may be omitted.

Here’s how we define instances of LinkedList:

let a: LinkedList<Int> = .empty  
let b: LinkedList<Int> = .node(data: 1, next: .node(data: 2, next: .empty))  

To work with an algebraic data type, we deconstruct it using pattern matching. Here’s how we would print a LinkedList:

enum LinkedList<Element>: CustomStringConvertible {  
    '' // cases omitted for brevity
    var description: String {
        switch self {
        case .empty:
        return "(end)"
        case let .node(data, next):
        return "(data), (next.description)"
        }
    }
}

let b: LinkedList<Int> = .node(data: 1, next: .node(data: 2, next: .empty))

print("b: (b)") // => b: 1, 2, (end)  

We’ve implemented the CustomStringConvertible protocol so that we can use string interpolation to print LinkedList instances. While it is possible in Swift to pattern match using an if case statement, the switch is preferable because the compiler will warn us if we’ve forgotten to handle a case. This safety is one big advantage that algebraic data types have over their classical counterparts. In a traditionally implemented linked list, you would have to remember to check if the next pointer was null to know if you were at the end. This problem gets worse as the number of cases increase in more complex data structures, such as full binary range trees with sentinels.

Note that since the description instance variable only has a getter, we do not need to use the more verbose syntax:

var description = {  
    get {
        // etc
    }
    set {
        // etc
    }
}

Our print function was useful, but in order to do interesting things we need to be able to modify algebraic data types. Rather than mutate the existing data structure, we’ll return a new data structure that represents the result after the requested operation. Since we’re not going to mutate the original data structure, we’ll follow the Swift 3 naming convention of using a gerund for our methods. Here’s how we would add an .inserting method to LinkedList:

enum LinkedList<Element>: CustomStringConvertible {  
    // cases and "description" omitted for brevity
    func inserting(e: Element) -> LinkedList<Element> {
        switch self {
            case .empty:
            return .node(data: e, next: .empty)
            case .node:
            return .node(data: e, next: self)
        }
    }
}

let c = b.inserting(e: 0)  
print("c: (c)") // => c: 0, 1, 2, (end)  

The key is that we’re returning a new LinkedList that represents the result after the insertion. Notice how in the .node case, we do not need to pattern match on .node(data, next) because data and next are not needed in order to construct the new .node; we can simply use self as the next: node.

Finally, let’s implement the classic “reverse a linked list” interview question using our algebraic data type:

enum LinkedList<Element>: CustomStringConvertible {  
    // cases, "description", and "insert" omitted for brevity
    func appending(_ e: Element) -> LinkedList<Element> {
        switch self {
            case .empty:
            return .node(data: e, next: .empty)
            case let .node(oldData, next):
            return .node(data: oldData, next: next.appending(e))
        }
    }

    func reversed() -> LinkedList<Element> {
        switch self {
            case .empty:
            return self
            case let .node(data, next):
            return next.reversed().appending(data)
        }
    }
}

print("reversed c: (c.reversed())") // => reversed c: 2, 1, 0, (end)  

I’ll leave it as an exercise to the reader to figure out what the running time for this algorithm is.

Here’s the Playground on GitHub

Isomorphisms Explained

I haven’t seen a good introduction to isomorphisms since they came into vogue last year, so I decided to write one.

Here goes!

A Parallel Postulate

Try defining “distance”. Most of us would say something like “how far two things are from each other”. Unfortunately, that makes answering a question like “how far is Alice from Bob” very difficult because there are several perfectly valid answers: Ten meters. One thousand centimeters. If Alice is ten meters away from Bob, is Bob negative ten meters away from Alice? Can I measure a zig-zag line from Alice to Bob?

To avoid ambiguity, a mathematician would use a definition like “Distance is the minimum number of one meter rulers, laid end-to-end, needed to touch both A and B”. It’s interesting how fragile yet robust these definitions are. Remove any piece of the definition and it falls apart. The word “minimum” ensures that the shortest path from A to B is measured. The use of one meter rulers ensures that distance is always an integer (no decimals or fractions). The answer will always be a positive number because you can’t have a negative number of rulers.

Now let’s change our perspective. We zoom really far out and see that Alice and Bob are on opposite sides of the Earth. Well, now “distance” depends on whether we are allowed to lay rulers through the center of the Earth. What if Alice and Bob were on the surface of a balloon? If we defined distance as the smallest angle between them from the center of the balloon, we’d have a unique answer even if the balloon inflates or deflates.

Here’s the main takeaway: the word “distance” doesn’t have any inherent meaning. Its meaning depends on our perspective, and if we are creative enough with our perspective, multiple meanings can exist at the same time. Keep this idea in mind, as it will return in the conclusion of this post.

I’m going to explain three types of isomorphism in this post, in order of complexity. The first is Graph Isomorphism. The second is Group Isomorphism. The third is Gödel Numbering.

Graph Isomorphism

I find that I learn best when the same thing is explained in at least two different ways. We’re going to start with graph isomorphisms because we can approach them both visually and theoretically.

A graph is a tuple (V, E) of a set of vertices V and a set of edges E. An edge is a tuple (Vi, Vj) where Vi and Vj are vertices. The vertices Va and Vb are adjacent if and only if there exists an edge (Va, Vb).

The graphs G and H are isomorphic if there is an isomorphism between them. An isomorphism between G and H is a bijection that maps vertices in G to a vertices in H such that if two vertices are adjacent in G, the vertices that they are mapped to are also adjacent in H.

It’s easier to understand this with pictures. Two graphs are isomorphic if you can arrange their vertices and edges in such a way that they look exactly the same.

graph-isomorphism-1-1-1-2.png

Figures 1.1 and Figures 1.2 are isomorphic. You can verify this visually by rotating the second figure ninety degrees clockwise and verifying that it looks exactly the same as the first figure. The other way is to define a function f(x) that meets the strict requirements we laid out above. Here is such a function f(x):

f(1) = d
f(2) = b
f(3) = c
f(4) = a

We now verify that this function meets our requirements. The first rule is that f(x) must be a bijective function. Bijective functions are also called bijections. A bijection is both injective and surjective. Injective functions map every member of their input set to a unique member of their output set. Surjective functions map at least one member of their input set to every member of their output set. Take a moment to understand this with the help of the following diagram, and then convince yourself that f(x) is a bijection.

graph-isomorphism-function-types.png

The second and final rule is that vertices that were adjacent in 1.1 must be adjacent in 1.2 after going through f(x). For succinctness, we’ll write “Vertex 1 is adjacent to vertex 2 and vertex 3” as 1 ADJ 2, 3. Convince yourself that f(x) preserves adjacency with the help of the table below.

1 ADJ 2, 3    => d ADJ b, c
2 ADJ 1, 3    => b ADJ d, c
3 ADJ 1, 2, 4 => c ADJ d, b, a
4 ADJ 3       => a ADJ c

That’s all there is to it. Simple? Not quite. Can you tell if these two graphs are isomorphic?

graph-isomorphism-1-3-1-4.png

As it turns out, it’s pretty difficult to figure out if two graphs are isomorphic once they get large enough. How about these two?

graph-isomorphism-1-5-1-6.png

There is no easy way to tell if two graphs are isomorphic. Figures 1.3 and 1.4 are isomorphic, but look nothing alike. Counting degrees (the number of edges each vertex has) does not work either — figures 1.5 and 1.6 both have degrees 2, 2, 3, 3, yet they are not isomorphic. Why is that? In order to prove that two graphs are not isomorphic, you need to show that no isomorphism could possibly exist between them. This is easy if their vertex degrees do not match, but as we just saw, it is possible for vertex degrees to match when no isomorphism is possible.

For more about graph isomorphism, I recommend this blog post by Jeremy Kun.

Group Isomorphism

Groups are a tuple (S, P) where S is a set of things and P is a function P(a, b) that operates on things a and b in S and returns something else. Two groups (G, *) and (H, +) are isomorphic if there is an isomorphism between them. The * and + are just symbols for operations on elements in the groups. They don’t necessarily mean multiplication or addition, though it is less confusing to choose a symbol that makes sense for whatever you’re doing.

The rules for group isomorphisms look similar to those for graph isomorphisms:

  1. There is a bijection P that maps elements in A to elements in B
  2. P preserves group operations P(a * b) = P(a) + P(b)

There isn’t a great way I know of to visualize this, so we’ll work through a few examples to understand what’s going on.

Degrees and Radians

Let’s show that angles in degrees and angles in radians are isomorphic under addition. Define the function P(d) = d * PI / 180. This function converts angles in degrees to angles in radians. We’re going to show that it’s an isomorphism. First we need to show that it is a bijection using a proof by contradiction. I’m only going to do this part of the proof for this example because it is quite lengthy and fairly obvious.

Show That P Is Injective

  1. Assume that P is not injective. That implies that at least one of the following is true:
    1. P is not defined for some input. This is not possible since P accepts all real numbers as input, and never divides by zero.
    2. P maps two inputs to the same output. Assume that this is possible. This implies that there exists some x and y where x != y such that P(x) = P(y). Substitute to get x * PI / 180 = y * PI / 180. Simplify to get x = y. This is a contradiction, so P cannot map two inputs to the same input.
  2. Since neither of the above is true, P must be injective.

Show That P Is Surjective

Assume that P is not surjective. That implies that there is a real number y such that there is no real number x where P(x) = y. Substitute to get x * PI / 180 = y. Rearrange to get x = y * 180 / PI. We now have a function C(y) that always returns a real number x that satisfies the equation P(x) = y for all y.

Show That P Preserves Group Operations

We need to show that P(a + b) = P(a) + P(b), where + stands for addition.

P(a + b) = (a + b) * PI / 180
         = (a * PI / 180) + (b * PI / 180)  // via the distributive property
         = P(a) + P(b)  // substitute back into definition of P

Phew, that’s it! We’ve shown that angles in degrees and angles in radians are isomorphic under addition.

Odds And Evens

Are odd integers are isomorphic to even integers under addition? Let’s give it a shot with this function: P(x) = x + 1. As you can see, given an odd number, it returns an even number. To show that it is an isomorphism, we first need to show that it is a bijection. You can do this now, or just take my word for it so we can move on.

Let’s look at whether this function preserves addition.

P(1 + 3) = P(4) = 5
P(1) + P(3) = 2 + 4 = 6

Oops, we’ve found a counterexample that violates rule number two. Can you think of a different way of mapping the odds to the evens that will preserve addition? Is there an operator besides addition that would work with the same mapping function?

Gödel Numbering

This is a very special sort of isomorphism that links formal systems with number theory. Formal systems are systems of thought. They have an alphabet, a grammar, a set of axioms, and a set of inference rules.

Formal systems let you encode statements like “5 is prime” in strings like ~Ea:Eb:(SSa*SSb)=SSSSS0, and prove the statement by using strict rules to manipulate strings. We’re going to start with a simple formal system and work our way up.

The EASY System

The EASY system is so named because it has four symbols in its alphabet: E, A, S, and Y. The grammar for this system says that “All Es appear before As, all As appear before Ss, and all Ss appear before Ys”. In other words, they appear in the order EASY.

A formula is a string made with the formal system’s alphabet. These are strings: EASS, SSSS, EY. These are not strings: XKCD, KISS, JUMP.

A formula is well-formed if it obeys the formal system’s grammar. ESYY and AAA are well-formed formulas. YES and EYES are not.

Let’s introduce some axioms and inference rules. Axioms are well-formed formulas that form the basis of all other theorems of the system. The EASY system has one axiom, A. It also has the following inference rules:

  1. A => AYY
  2. AYYY => S
  3. AS => E
  4. SY => EA

Using these inference rules, we can derive more theorems from the axioms:

A
AYY (Rule 1)
AYYYY (Rule 1)
AYYYYYY (Rule 1)
SYYY (Rule 2)
EAYY (Rule 4)
EAYYYY (Rule 1)
EASY (Rule 2)

All of these formulas are theorems because they can be derived from the formal system’s axioms using its inference rules. Note that formulas might not be well-formed, and well-formed formulas might not be theorems. This distinction is important! EY is a well-formed formula of the EASY system, but is it a theorem? Try deriving it from the axiom using the inference rules. How can you be sure that it isn’t a theorem?

The question “is EY a theorem of the EASY system” can be generalized to “is X a theorem of the Y system”. As Y gets more powerful, the questions we can ask get more interesting. The EASY system does not appear to do anything remotely useful because it is not isomorphic to something else we already know about. This is important: meaning is something that humans attach to formal systems. Formal systems are rather dumb systems of thought based on mechanically manipulating strings using pedantic rules. Let’s look at a formal system that we can attach some meaning to.

Arithmetic

Before we can express statements like “5 is prime” we need to be able to do some basic math. Let’s create a new formal system, the POES system.

The alphabet of our new system is S, 0, p, e.

The grammar of this system is {x}p{y}e{z}. The placeholders that look like {x} represent any string that starts with S and ends with 0.

The axiom of this system is 0p0e0

The rules of our system are:

1. {x}p{y}e{z}  => S{x}p{y}eS{z}

2. {x}p{y}e{z}  => {x}pS{y}eS{z}

Now let’s derive some theorems from the axiom:

0p0e0
S0p0eS0 (Rule 1)
S0pS0eSS0 (Rule 2)

This formal system looks nothing like the EASY system, but it works the exact same way. You have a set of axioms, and you can derive theorems from those axioms by applying some rules.

Although it is based on the same principles as the EASY system, the POES system is more interesting because it happens to be isomorphic to a tiny part of number theory. Here’s how you can interpret theorems of this system:

  • 0 means zero
  • S means “successor of” (so SSSSS0 means five)
  • p means “plus”
  • e means “equals”

An example:

0p0e0      =>  0+0=0
S0p0eS0    =>  1+0=1
S0pS0eSS0  =>  1+1=2

If you were given a string S0p0e0, would you be able to tell if it was a theorem of the system? It fits the grammar of the system, but in order to tell if it is a theorem, we need to show that we can derive it from the axioms. Now that you know that this system models addition, you might be tempted to say “no way, because 1+0 does not equal 0”. However, that would be using human intuition to work outside the system. You can’t jump to conclusions in a formal system; you have to mechanically prove that a string is a theorem by starting from an axiom and applying rules until you get the same string.

Is it possible to show that a string is not a theorem of a formal system?

Logic

In order to express a statement like “five is prime”, we need a more powerful formal system. One such system is Typographical Number Theory, or TNT. Explaining the entire system is beyond the scope of this post, but I’ll explain how to understand the example string from the beginning of this section.

~Ea:Eb:(SSa*SSb)=SSSSS0

From the left: ~ means “not”. E{x}: means “exists {x}”. a and b are simply variables in the statement. * means

“multiply”, and the parenthesis () are just for grouping.

Put together, this string says “There do not exist a and b such that (2 + a) * (2 + b) = 5”. In other words, five is prime.

It bears repeating that strings by themselves have no meaning. We find meaning in strings through isomorphism. The meaning in TNT comes from propositional calculus and number theory. However, you do not need to know any of that to work with this formal system.

It takes practice in order to turn statements like “16 is a power of 2” into TNT, but it can be done. The more complex the thought, the larger the resulting string. For example, you could try to prove Fermat’s Last Theorem by turning it into a gigantic string of TNT, and trying to derive it from the axioms.

Here is Ray Toal’s summary of TNT if you would like further reading.

Gödel Numbering

We’re finally ready to understand a very special type of isomorphism. Earlier we saw how otherwise meaningless strings like S0pS0eSS0 can acquire meaning through isomorphism. Now we’ll see how these strings can acquire an additional layer of meaning through a second isomorphism.

Computers store strings by encoding them into numbers. One popular encoding is ASCII. In ASCII, the lowercase letter a is encoded as the number 97. Assuming that we stay within the ASCII character set, we can encode any string into a number. Here is how the string S0pS0eSS0 can be encoded as the number 83,048,112,083,048,101,083,083,048:

S   0   p   S   0   e   S   S   0
083 048 112 083 048 101 083 083 048

Recall that we derived this string from an axiom of the POES system using inference rules. I’ve reproduced the proof below, this time with the ASCII encoding of each step.

0p0e0       048,112,048,101,048
S0p0eS0     083,048,112,048,101,083,048
S0pS0eSS0   083,048,112,083,048,101,083,083,048

Hey, this looks like the beginning of an isomorphism! We have two sets of things, and a way of mechanically converting between them. Specifically, we have a bijection between strings of a formal system and natural numbers.

To complete the isomorphism, we also need to convert our inference rules so that they work on numbers.

Gödel’s key insight was that each step of a formal system is isomorphic to some sequence of arithmetic operations. You can multiply by ten to shift a string to the left, or divide by ten to shift a string to the right. You can add to insert new characters, and subtract to remove old ones.

For example, one of the inference rules of the EASY system was A => AYY. If we encode A` as 1 and Y as `2, then this rule could be expressed as “If x is equal to 1, and x is an EASY number, then x*100 + 2*10 + 2 is an EASY number”.

This strategy works even for more complex rules. Recall that the rules of the POES system are:

1. {x}p{y}e{z}  => S{x}p{y}eS{z}

2. {x}p{y}e{z}  => {x}pS{y}eS{z}

The trick to translating more complex inference rules is to use multiple variables and constraints. For example, rule two can be translated into this:

  1. If j*10^(m+9) + 112*10^(m+6) + p*10^(m+3) + 101*10^m + n is a POES number where the following is true:
    • n < 10^m
    • p < 10^3
  2. then j*10^(m+15) + 112*10^(m+12) + 83 * 10^(m+9) + p*10^(m+6) + 101*10^(m+3) + 83*10^m + n is a POES number

Let’s see this rule in action!

Input string and number:
  S0p0eS0  =>   83,048,112,048,101,083,048

Fit the components of the input formula:
                         83,048 => n
                    101,000,000 => 101*10^m where m=6
                 48,000,000,000 => p*10(m+3) where p=48
            112,000,000,000,000 => 112*10^(m+6)
     83,048,000,000,000,000,000 => j*10(m+9) where j=83,048

Verify that the conditions are true:
  n < 10^m   =>  83,048 < 10^6  =>  true
  p < 10^3   =>  48 < 10^3      =>  true

Create the components of the output formula:


             83,048,000,000,000,000,000,000,000 => j*10^(m+15)
                    112,000,000,000,000,000,000 => 112*10^(m+12)
                         83,000,000,000,000,000 => 83*10^(m+9)
                             48,000,000,000,000 => p*10^(m+6)
                                101,000,000,000 => 101*10^(m+3)
                                     83,000,000 => 83*10^m
                                         83,048 => n


Sum it all up to get:
   83,048,112,083,048,101,083,083,048  =>  S0pS0eSS0

It takes some practice, but the key is this: we can take any formal system and talk about it using the natural numbers and simple arithmetic — even TNT! What a wonderful new type of isomorphism. What can we do with it?

A Strange Loop

Can TNT make statements about itself? For example, can we create a string of TNT that says “S is a theorem of TNT”?

Using Gödel numbering, we can! To make things easier to follow, we’ll define two operations, tnt2nt and nt2tnt. They stand for “TNT to Number Theory” and vice versa.

The operation tnt2nt represents the tedious work of converting from formal systems to number theory. For example, tnt2nt('S0p0eS0') would spit out the number 83,048,112,048,101,083,048, and tnt2nt(Rules) would spit out the arithmetic equivalents of the inference rules. Remember that axioms are strings, so you can also pass them through tnt2nt().

The operation nt2tnt represents the far more difficult task of converting statements of number theory into TNT. For example, nt2tnt('Five is a prime number') would produce ~Ea:Eb:(SSa*SSb)=SSSSS0. nt2tnt('Four is an even number') would produce Ea:SS0*a=SSSS0. We can even use nt2tnt() to turn “There exist numbers a, b, and c where c < 10^b such that a = 101*10^(b+3) + 99*10^b + c” into a massive string of TNT. Note the similarity of this string to the previous example!

With these two operations defined, we now have a way to create TNT strings that talk about TNT:

  1. S is a theorem of TNT
  2. The string S can be derived from axioms A following the rules R
  3. The number tnt2nt(S) can be produced from the numbers tnt2nt(A) with the arithmetic operations tnt2nt(R)
  4. nt2tnt('The number tnt2nt(S) can be produced from the numbers tnt2nt(A) with the arithmetic operations tnt2nt(R)')

This mind-blowing result is what happens when you have not one, but two isomorphisms working together. We’ve created a string of TNT that talks about number theory, and through number theory, talks about other TNT strings.

In Conclusion

To summarize: an isomorphism is a bijection that preserves relationships.

  • When graphs are isomorphic to each other, the bijection is between vertices, and adjacency is preserved.
  • When groups are isomorphic to each other, the bijection is between items, and group operations are preserved.
  • The POES system is isomorphic to a tiny piece of number theory, where the bijection is between strings like 0pS0eS0 and formulas like a+b=c, and the properties of addition are preserved.
  • Formal systems and number theory are isomorphic to each other, where the bijection is between strings and natural numbers, and inference rules are preserved.