Types and Lambda Calculus

Most programmers are familiar with λ-calculus. It’s one of the most widely used tools in theoretical computer science and logic. It’s the basis of many programming languages, including Lisp, Haskell, ML, and Scala. It’s had a strong influence on many other programming languages that aren’t strictly based on it, including Java, C++, and Javascript.

Motivation: the Problem

Modern programmers love the λ-calculus. A lot of the mathematicians who worked in what became computer science also loved it. But if you go back to its roots, there was a problem.

The λ-calculus in its non-typed form, as it was originally defined, was inconsistent.

Haskell Curry eventually reduced the paradox to something quite simple:

 r = (\lambda x. ((x x) \Rightarrow y))

That is a function which returns y if (x x) is true.

To see the paradox, we need to change how we think of λ-calculus. Most people today who know λ-calculus are programmers, and we think of it primarily as something like a programming language. But the roots of λ-calculus were laid before computers as we know them existed. At the time, λ-calculus was a tool used by logicians. To them it wasn’t a computing machine, it was a logical model of computation.

When we look at the expression (r r) \Rightarrow y, what we see is executable logic that reads as “If applying r to r returns true, then return y”. And by using computational reasoning, we’d conclude that (r r) is a non-terminating computation, because to get the value of (r r), we need to evaluate (r r), and then apply r to that result. But to logicians like Haskell Curry, it read is “The statement (r r) implies y”. Rendered into simple english, it’s a statement like: “If this statement is true, then my hair is purple”. It’s purely a logical implication, and so even though we can’t actually evaluate (r r), in logical terms, we can still say “This is a well-formed logical statement, so is it true?”.

Is that true? Suppose it is. If it’s true, then that means that it says that whatever y is must be true. Without knowing what y is, we can’t be sure if this is a true statement.

Suppose that it’s false. If (r r) is false, that means that the implication (r r) must be true, because FOPL says that if the antecedent of an implication is false, the entire implication is true.

It’s clearer when you look at the english: If this sentence is true, then my hair is purple”. My hair isn’t purple, which means that the statement can’t be true. But if the statement isn’t true, then the implication is true, so the statement is true. We’re caught in a self-reference loop, just like what we saw in Russell’s paradox.

This was considered a very bad thing. It’s a bit subtler than the problem with naive set theory. In set theory, we had an unambiguous inconsistency: we had a set that was well-defined under the axioms of set theory, and without any question, that set was inconsistent. Here, we’ve got an expression which might be consistent, and then again, it might not. It depends on what the consequent – the “my hair is purple” part – of the implication is. If it’s something true, then we’re fine. If it’s not, then we’re stuck.

The problem is, no matter what you put into that “my hair is purple” part, you can use this to produce a proof that it’s true, even if it isn’t. And that’s a fundamental inconsistency, which can’t be tolerated.

Curry’s paradox meant that the logicians working with λ-calculus had a problem that they needed to solve. And following the fashion of the time, they solved it using types. Much like ST type theory attempted to preserve as much of set theory as possible while fixing the inconsistency, typed λ-calculus tried to fix the inconsistency of λ-calculus. The basic approach was also similar: the typed λ-calculus introduced a stratification which made it impossible to build the structures that led to inconsistency.

In ST, the solution was to build a logical system in which it was impossible to express self-reference. In λ-calculus, the basic goal was the same: to eliminate self-reference. But in λ-calculus, that restriction is stated differently. What the type system in λ-calculus does is make it impossible to construct a statement that is a fixed-point combinator.

If we look carefully at the paradoxical statement up above, it’s not really pure λ-calculus. It relies on the fact that we’re defining a function named r, and then applying r to itself using the name r. But that’s just syntactic sugar: in fact, r can’t reference r. You need some tool to let you apply an expression to itself: that tool is called a fixed-point combinator. The most common fixed-point in λ-calculus is the Y combinator, which underlies how recursive computations usually work in λ-calculus.

The way that the simply typed λ-calculuss gets around the Curry paradox is by making it impossible to build a well-typed fixed-point combinator. Without that, you can’t build the self-referential constructs that cause the inconsistency. The downside is that the simply typed λ-calculus, without a fixed point combinator, is not Turing complete. The evaluation of every simple typed λ-calculus expression will eventually terminate.

(As an aside: this isn’t really a problem in practice. The self-referential expressions that cause the Curry paradox turn into non-terminating computations. So they don’t produce a paradox; they just don’t produce anything. Logical inconsistencies don’t produce results: they’re still an error, instead of terminating with an inconsistent result, they just never terminate. Again, to the logicians at the time, the idea of non-termination was, itself, a deep problem that needed a solution.)

The Solution: Stratification by Types

The way that the simply typed λ-calculus fixed things was by creating a stratification using types. The type system created a restriction on the set of statements that were valid, well-formed logical statements. That restriction made it impossible to express a fixed point combinator or a general recursive computation of any kind.

It’s helpful to once again refer back to ST. In ST, we started the type of atoms at level 0. To get to level 1, we defined predicates over level-0 objects, and the set of objects that matched the predicate was a level-1 type. Then we could define predicates over level-1 objects, and the set of level-1 types that satisfied the predicate was a level-2 type, and so on. In the simply typed λ-calculus, we do the same thing, but with functions: we can build functions that operate on primitive atoms (also called base values), or on other functions. When we define a function, it must be assigned a type, and that type must be something at a lower level than the function being defined. You can’t ever pass a function to itself, because the function is an object at a higher level than the type of its parameter.

We start with base types. Every simply-typed lambda calculus starts with a collection of primitive atomic values. The set of atomic values is partitioned into a collection of types, which are called the base types. Base types are usually named by single lower-case greek letters: So, for example, we could have a type \sigma which consists of the set of natural numbers; a type \tau which corresponds to boolean true/false values; and a type \gamma which corresponds to strings.

Once we have basic types, then we can talk about the type of a function. A function maps from a value of one type (the type of parameter) to a value of a second type (the type of the return value). For a function that takes a parameter of type \gamma, and returns a value of type \delta, we write its type as “\gamma \rightarrow \delta“. The “\rightarrow” is called the function type constructor; it associates to the right, so \gamma \rightarrow \delta \rightarrow \epsilon is equivalent to \gamma \rightarrow (\delta \rightarrow \epsilon).

In every function declaration, we need to specify the type of the parameters and the type of the result. So:

  1. \sigma \rightarrow \sigma is a function which takes natural number as a parameter, and returns a natural number as a result.
  2. (\sigma \rightarrow \sigma) \rightarrow \sigma is a function which takes a \sigma \rightarrow \sigma function as a parameter, and produces a natural number as a result.

As usual in λ-calculus, we don’t have multi-parameter functions – all functions are curried, so a function like addNatural would be a function that takes a natural number as a paramater, and returns a function that takes a natural number and returns a natural number. So the type of addNatural is \sigma \rightarrow \sigma \rightarrow \sigma.

How does this get around the self-reference problem? A function like the one in the Curry paradox takes an object of its own type as a parameter. There’s no way to write that in a type system. It’s a significant restriction which makes it impossible to write general recursive expressions – it limits us to something close to primitive recursion, but it avoids the inconsistency. All valid expressions written with this system of types in place is guaranteed to terminate with a consistent result.

Extending λ-calculus with types

Now, it’s time to get at least a little bit formal, to see how we integrate a stratified type system into the lambda calculus. There’s two facets to that: the syntactic, and the analytic. The syntactic part shows how we extend λ-calculus to include type declarations, and the analytic part shows how to determine whether or not an expression with type declarations is valid.

The syntax part is easy. We add a “:” to the notation; the colon has an expression or variable binding on its left, and a type specification on its right. It asserts that whatever is on the left side of the colon has the type specified on the right side. A few examples:

\lambda x: \nu . x + 3
This asserts that the parameter, x has type nu, which we’ll use as the type name for the natural numbers. (In case it’s hard to tell, that’s a greek letter “nu” for natural.) There is no assertion of the type of the result of the function; but since we know that “+” is a function with type \nu  \rightarrow \nu \rightarrow \nu, we can infer that the result type of this function will be \nu.
(\lambda x . x + 3): \nu \rightarrow \nu
This is the same as the previous, but with the type declaration moved out, so that it asserts the type for the lambda expression as a whole. This time we can infer that x : \nu because the function type is \nu \rightarrow \nu, which means that the function parameter has type \nu.
\lambda x: \nu, y:\delta . \text{if}\hspace{1ex} y\hspace{1ex} \text{then}\hspace{1ex} x * x \hspace{1ex}\text{else} \hspace{1ex} x
This is a two parameter function; the first parameter has type ν, and the second has type δ. We can infer the return type, which is ν. So the type of the full function is ν → δ → ν. This may seem surprising at first; but remember that λ-calculus really works in terms of single parameter functions; multi-parameter functions are a shorthand for currying. So really, this function is: λ x : ν . (λ y : δ . if y then x * x else x); the inner lambda is type δ → ν; the outer lambda is type ν → (δ → ν).

To talk about whether a program is valid with respect to types (aka well-typed), we need to introduce a set of rules for checking the validity of the type declarations. Using those rules, we can verify that the program is type-consistent.

In type analysis, we’ll talk about judgements. When we can infer the type of an expression using an inference rule, we call that inference a type judgement. Type analysis allows us to use inference and judgements to reason about types in a lambda expression. If any part of an expression winds up with an inconsistent type judgement, then the expression is invalid. If we can show that all of the components of an expression have consistent type judgements, then we can conclude that the expression is well-typed, meaning that it’s valid with respect to the type system.

Type judgements are usually written in a sequent-based notation, which looks like a fraction where the numerator consists of statements that we know to be true; and the denominator is what we can infer from the numerator. In the numerator, we normally have statements using a context, which is a set of type judgements that we already know;it’s usually written as an uppercase greek letter. If a type context includes the judgement that x : \alpha, I’ll write that as \Gamma :- x : \alpha.

Rule 1: Type Identity

\frac{\mbox{}}{x : \alpha :- x: \alpha}

This is the simplest rule: if we have no other information except a declaration of the type of a variable, then we know that that variable has the type it was declared with.

Rule 2: Type Invariance

\frac{ \Gamma :- x:\alpha, x != y}{\Gamma + y:\beta :- x:\alpha}

This rule is a statement of non-interference. If we know that x:\alpha, then inferring a type judgement about any other term cannot change our type judgement for x.

Rule 3: Function Type Inference

\frac{\Gamma + x:\alpha :- y:\beta}{\Gamma :- (\lambda x:\alpha . y):\alpha \rightarrow \beta}

This statement allows us to infer function types given parameter types. Ff we know the type of the parameter to a function is \alpha; and if, with our knowledge of the parameter type, we know that the type of term that makes up the body of the function is \beta, then we know that the type of the function is \alpha \rightarrow \beta.

Rule 4: Function Application Inference

\frac{\Gamma :- x: \alpha \rightarrow \beta, \Gamma :- y:\alpha}{\Gamma :- (x y): \beta}

This one is easy: if we know that we have a function that takes a parameter of type \alpha and returns a value of type \beta, then if we apply that function to a value of type \alpha, we’ll get a value of type \beta.

These four rules are it. If we can take a lambda expression, and come up with a consistent set of type judgements for every term in the expression, then the expression is well-typed. If not, then the expression is invalid.

So let’s try taking a look at a simple λ-calculus expression, and seeing how inference works on it.

\lambda x y . y x

Without any type declarations or parameters, we don’t know the exact type. But we do know that “x” has some type; we’ll call that “α”; and we know that “y” is a function that will be applied with “x” as a parameter, so it’s got parameter type α, but its result type is unknown. So using type variables, we can say “x:α,y:α→β”. We can figure out what “α” and “β” are by looking at a complete expression. So, let’s work out the typing of it with x=”3″, and y=”λ a:ν.a*a”. We’ll assume that our type context already includes “*” as a function of type “ν→ν→ν”, where ν is the type of natural numbers.

  • “λ x y . y x) 3 (λ a:ν . a * a)”: Since 3 is a literal integer, we know its type: 3:ν.
  • By rule 4, we can infer that the type of the expression “a*a” where “a:ν” is “ν”, and *:ν→ν→ν so therefore, by rule 3 the lambda expression has type “ν→ν”. So with type labelling, our expression is now: “(λ x y . y x) (3:ν) (λ a:ν.(a*a):ν) : ν→ν”.
  • So – now, we know that the parameter “x” of the first lambda must be “ν”; and “y” must be “ν→ν”; so by rule 4, we know that the type of the application expression “y x” must be “ν”; and then by rule 3, the lambda has type: “ν→(ν→ν)→ν”.
  • So, for this one, both α and β end up being “ν”, the type of natural numbers.

So, now we have a simply typed λ-calculus. The reason that it’s simply typed is because the type treatment here is minimal: the only way of building new types is through the unavoidable \rightarrow constructor. Other typed lambda calculi include the ability to define parametric types, which are types expressed as functions ranging over types.

Programs are Proofs

Now we can get to the fun part. The mantra of type theory is the program is the proof. Here’s where we get our first glimpse of just what that really means!

Think about the types in the simple typed language calculus. Anything which can be formed from the following grammar is a λ-calculus type:

  • type ::= primitive | function | ( type )
  • primitive ::= α | β | δ | …
  • function ::= type→type

The catch with that grammar is that you can create type expressions which, while they are valid type definitions, you can’t write a single, complete, closed expression which will actually have that type. (A closed expression is one with no free variables.) When there is an expression that has a type, we say that the expression inhabits the type; and that the type is an inhabited type. If there is no expression that can inhabit a type, we say it’s uninhabitable. Any expression which either can’t be typed using the inference rules, or which is typed to an uninhabitable type is a type error.

So what’s the difference between inhabitable type, and an uninhabitable type?

The answer comes from something called the Curry-Howard isomorphism. For a typed λ-calculus, there is a corresponding intuitionistic logic. A type expression is inhabitable if and only if the type is a provable theorem in the corresponding logic.

The type inference rules in λ-calculus are, in fact, the same as logical inference rules in intuitionistic logic. A type \alpha \rightarrow \beta can be seen both as a statement that this is a function that maps from a value of type \alpha to a value of type \beta, and as a logical statement that if we’re given a fact \alpha, we could use that to infer the truth of a fact \beta.

If there’s a logical inference chain from an axiom (a given type assignment) to an inferred statement, then the inferred statement is an inhabitable type. If we have a type \alpha \rightarrow \alpha, then given a inhabited type \alpha, we know that \alpha \rightarrow \alpha is inhabitable, because if \alpha is a fact, then \alpha \rightarrow \alpha is also a fact.

On the other hand, think of a different case \alpha \rightarrow \beta. That’s not a theorem, unless there’s some other context that proves it. As a function type, that’s the type of a function which, without including any context of any kind, can take a parameter of type α, and return a value of a different type β. You can’t do that – there’s got to be some context which provides a value of type β – and to access the context, there’s got to be something to allow the function to access its context: a free variable. Same thing in the logic and the λ-calculus: you need some kind of context to establish “α→β” as a theorem (in the logic) or as an inhabitable type (in the λ-calculus).

What kind of context would make a type \alpha \rightarrow \beta inhabitable? A definition of a valid function that takes an α, and returns a β. If such a function exists, then that function is a proof of the inhabitility of the type. Literally, the program is the proof.

The Constructivist Roots of Type Theory

This post started off as an introduction to a post about the simply typed lambda calculus. It got a bit out of control – but reading it over, I think that it’s valuable background. So I’ve made it into its own post.

ST type theory is an interesting idea, but it’s mostly interesting as a historical curiosity and background. Type theory started with things like ST, but it turned into something very different. You can see the roots in ST, but modern type theory takes a completely different approach. ST is an axiomatic foundation for a stratified version of type theory. Modern type theory, in contrast, has constructed a universe of mathematics that, rather than being based on an axiomatic foundation of first order predicate logic, is based almost entirely on ideas of computability and computation.

The core of the modern version of type theory is the intuitionistic type theory of Per Martin-Lof, and it’s part of the constructionist school of math.

Like ST type theory, constructivism can also been seen as a reaction to paradox and inconsistency. Some mathematicians decided that the right way to approach the problem of paradox was to build a better, stronger axiomatic foundation. That effort let to things like ST type theory, ZFG/NBG set theory, and the principia mathematica. But others thought that that approach was wrong.

The axiomatic approach ends up with things like the axiom of choice in its foundation. And the axiom of choice leads directly to results that seem to be completely nonsensical. For example, the classic Banach-Tarski paradox.. Banach-Tarski says that there’s a way of taking a sphere the size of an orange, cutting it into some very odd slices, and then reassembling those slices into two oranges exactly the same size as the original. On the face of it, that’s ridiculous!

The key to Banach-Tarski is that it’s built on an operation that’s impossible in reality. It’s exploiting the boundaries of a theory. You start with a sphere. That’s an object on which metrics like “volume” are well-defined. You’re “cutting” it – not really cutting, but actually subdividing it – into pieces. Those pieces are objects where the metrics no longer work. You’ve broken the metric. And then, you’ve got objects for which the entire concept of volume no longer makes any sense, and you reassemble them into new objects – and those new objects are, once again, objects where the volume metric works.

From one point of view, you’ve done something that makes sense. You started with a topological space with meaningful metrics. A topological space is just a set with a bunch of cute structural properties – the neighborhood relationships. Those structural properties in turn have higher order structure properties, which can be used to define metrics like distance and volume. So the original sphere has a meaningful volume. But still, mathematically, it’s just a set with neighborhood relationships.

Since it’s just a topological space, you can divide it into sub-spaces – that is, subsets which retain structural properties. They’re still topological spaces, but now, the neighborhood relations, because of the way that you divided the original set, no longer have the properties that you need to define metrics. They’re not metric spaces.

When you recombine them, you can combine them into two new topological spaces that do have the properties that you need to define metrics – so volumes are, once again, meaningful. But in that process, you’re redefining the metrics, and so they can be redefined in any way that you want, producing any results that you want.

There’s a pretty strong argument that that entire process is an abuse of the underlying axioms. It only works because you can destroy the metric, and then recreate it. When you state what’s going on clearly, it seems like it’s cheating. But according to the standard axiomatic set-theory based math, everything that happens is completely legal. It’s ridiculous and non-sensical, and it produces a result that looks like it must be obviously wrong, but according to the axioms, it’s just fine.

The problem of cheating on the metrics is bad, but it’s not all that’s wrong with Banach-Tarski according to the constructivists. B-T says that you can cut a spherical metric space into pieces. Only you really can’t – it’s all just a clever sleight-of-hand! You can’t describe or specify how to cut the original sphere into pieces. There is no shape, no structure, no process that you can use to actually cut the sphere. The axioms say that such a cut exists, but the actual method of cutting is not just unknown, but essentially unknowable.

The constructivists argue that that’s rubbish. How can you argue that it exists, but we can’t produce it, we can’t find it, we can’t study it. According to the constructivists, it exists only as an artifact of a flawed system. It’s meaningless to say that something exists if it only exists in an unreachable theoretical ether.

The constructivists say that things like Banach-Tarski and the Russell paradox are part of the same basic problem: defining things not by how they can be created, but by how they can be described using some fuzzy airy-fairy gibberish derived from axioms. The solution isn’t to find a better set of axioms, but to find a fundamentally different way of doing things.

The constructivist method says that the way to do math is to build things. That the only way you can really consider a statement to be true is if you have concrete proof: the only way to prove that something exists is to show a concrete example of it. The only way to prove that something is false is with a specific counterexample.

That leads to an absolutely fascinatingly different way of doing math, which is what we’ll see in Martin-Lof’s intuitionistic type theory. When you talk about typed programming languages, you’ll hear a mantra: “The program is the proof”. That is literally true. In Martin-Lof’s intuitionistic type theory, the way that you prove things is by, essentially, writing programs! A proof of a fact is a computation. A proof of an existential statement isn’t just some abstract reasoning that shows that it exists – it’s a computation that produces a concrete example. A proof of a universal statement is a metaproof – a program that, given any value, produces a proof specific to that value.

It avoids the basic problem with the axiomatic problem. You can’t have something ridiculous like the set of all sets that don’t include themselves, because the only way to show that a set exists is to show a process to create it – and there’s no way to create a paradoxical set! You don’t get nonsense like Banch-Tarski, because the division of the spherical topological space into the non-metric subspaces is impossible: you can’t show a process that produces it. In the world of intuitionism and constructivism, existence proofs that don’t produce concrete examples don’t exist!

It’s an impressive thing, and it’s really a mind-blowingly different way of understanding what it is to do mathematics.

For introducing Martin-Lof’s type theory, I’m going to be mostly working from the Nordstrom/Petersson/Smith text, with supplementation from many different sources. For the programming language oriented part, I highly recommend Types and Programming Languages by Benjamin Pierce.

Before we really get started, I’m going to back and do some review. I’m going to go start with an introduction to the simply typed lambda calculus, and intuitionistic logic, because they’re both really essentials for understanding what’s coming next. So that will be the next couple of posts.

Administrivia

Quick note: I’m experimenting with showing ads on the blog. In my time with scientopia, I dumped a frankly ridiculous amount of money into keeping things online – it ended up coming to around $4K/year. Obviously, this site is a lot cheaper, since I only need to support the one blog, but still, I’d like to get to the point where it’s self-supporting.

If the ads are annoying, let me know. I’m trying to strike a compromise. I’d like to get some money coming in to cover hosting costs, but I don’t want to degrade the experience of my readers. The way I’ve set it up, the ads shouldn’t have popups, and they shouldn’t have any interactive animations. If you see anything like that, please let me know as soon as possible, and I’ll do my best to get it fixed. At the moment, the visual appearance of the ads is less than idea, but I’ll be tweaking it until it’s reasonable. (For now, things are still in process with Google, so all you see is a big yellowish box as a placeholder; as soon as someone at Google gets around to approving it, that should be replaced by ads.

If ads are offensive, again, let me know. I don’t want to be giving exposure to blatantly offensive rubbish.

If ads are pseudoscience or that sort of thing, I don’t care. I believe that the people who read this blog are intelligent enough to realize what a sham that crap is, and I have no problem taking money from them – every cent they waste buying ads on my blog is a cent that they’re not using for something a lot worse!

The Basics of ST Type Theory (plus Administrivia)

I’ve been writing this blog for a long time. It’s pretty amazing to me to realize just how long – the original version of Good Math/Bad Math started over 9 years ago! I’ve gone through some times when the blog was really busy, and some when it was really slow. Lately, it’s been the latter. Since my mom died a few months back, I’ve been depressed, and finding enough motivation to blog after a full day of work has been difficult. But I’m trying to get back to normal, and start updating the blog at least a couple of times a week.

A few weeks back, one of my blog-friends asked me to write about type theory. Type theory comes up a lot in programming language design, particularly in the functional programming world. If you can’t talk intelligently about quantified types, existential types, dependent types, and similar stuff, you’re largely locked out of discussions.

I’ve taken a couple of weak stabs at type theory over the years, but I’ve never tried to really do it justice. It’s a hard topic, and even though it’s got a lot of overlap with my professional focus, I’ve never been formally trained in it. I’ve never actually taken a course in type theory – I’ve learned it on my own, as I’ve studied programming languages and denotational semantics.

Now seems like a good time to give it a try. It’s a subject that I’m obviously pretty interested in.

To start, I’m going to recycle a couple of old posts. I’ve written about the simplest version of type theory that I know, something called ST. I’m rewriting tha old post here. After that, I’ll rewrite some material about the simply typed lambda calculus, putting into a more type-theoretic framework. Then I’ll move from there into basic type theory, intuitionistic type theory, and the various type system heirarchies, like System-T, System-F, Lambda-cube, etc.

So, today: ST type theory.

I’ve said many times that I’m a programming language guy, and that’s how I approach this stuff. For someone who works on programming languages, types are old hat. They seem like such an obvious idea that it’s hard to conceive of a world in which they aren’t a part of the mathematical background. But in the world of math, they’re a relatively recent invention. (In computer science, they’re ancient history: type theory predates the first real computers.)

The roots of type theory are the same as the roots of axiomatic set theory. The point wasn’t to support anything computational; the point was to try to salvage set theory. Cantor had devised set theory, and once people started to understand it, the mathematical community thought it was the neatest thing ever! Set theory was just wonderful! Except for the part where it was a total inconsistent train wreck.

Mathematicians love set theory. It’s a system on which all of mathematics can be built, using a basis which is simple, using nothing but intuitively clear concepts. That’s lovely. Unfortunately, as we know, simple intuitive ideas often don’t work. Cantor’s set theory had a huge problem: it was inconsistent.

Here’s the problem.

In set theory, you’ve got these collection of things called sets. The main thing that you can do with sets is say, “I’ve got this object here. You’ve got a set. Is my object part of your set?”. For any possible pair of object and set, there can be only one correct answer: either the object is in the set, or it isn’t. There’s no middle ground: there’s no way an can be both in and not in a set.

In Cantor’s version of set theory, you could define a set using logic, in a process called comprehension. He said that if you can write a logical predicate, then there’s a set which contains the collection of objects that satisfy that predicate. Using comprehension, you can define sets that range over sets. For example, you can define the set of all sets with an even number of elements.

The catch is that Cantor didn’t place any restrictions on those predicates. So you can create sets based on predicates that range over themselves. You can define a set which is a member of itself, like the set of all sets.

Using that, you can make up some silly sets. For example: Is the set of all sets that contain themselves a member of itself?

Well, if it is, then it is. If it isn’t, then it isn’t. Both yes and no! The english statement, “the set of all sets that contain themselves”, doesn’t uniquely identify one set. There are two different sets that match that description! There’s one that does contain itself, and there’s one that doesn’t!

We’ve already a problem in a lesser way: even written in careful predicate logic, the definition is ambiguous when it shouldn’t be. But there’s more trouble ahead. If we can define the set of all sets that do contain themselves as a member, then we can also define the set of all sets that do not contain themselves as a member.

Let S = \{ x : x \not\in x\} – that is, it’s the set of all sets that do not contain themselves as a member. Is S \in S?

If S is not a member of itself, then by the definition in the comprehension, it must be a member of itself. But if it is a member of itself, then by that same definition, it can’t be. It can’t be a member of itself. But it also can’t not be a member of itself.

That’s a demonstration of the fundamental inconsistency in Cantor’s set theory, and it’s commonly known as Russell’s paradox. It’s caused by the ability to build unlimited self-referential statements about sets and set membership.

Inconsistency is a big deal in mathematics: if you’re working in an inconsistent system, then every statement is provably true in that system. That’s another way of saying that proving something in an inconsistent system is completely useless, because the proof doesn’t actually tell you that the thing you proved is true!

Using Cantor’s formulation of set theory, I can start with a statement that I know really is true, and I can work out a valid proof to show that it’s true. But I can also start with a statement that I know is false, and I can work out a perfectly valid proof that shows that false statement is true. I can prove that the sum of the integers from 1 to N is \frac{(n)(n+1)}{2}, and I can also prove that 1=2.

Any inconsistenty in a formal system means that the entire system is useless. Russell’s paradox meant that nothing that had been proven with set theory could be trusted! None of the methods of proof that people had come to love from working with set theory could be followed, because the entire basis was inconsistent!

Mathematicians wanted to find a way to preserve as much of set theory as possible, while getting rid of the inconsistency. That led to a lot of different systems. I’ve talked a lot on this blog about axiomatic set theory, which was the most well-known and widely accepted approach to the problem. Type theory is a different one.

What type theory does is start with a notion very similar to sets: collections of objects. The difference is that in type theory, instead of having sets which define collections of objects using logical predicates, in type theory, you have collections called types. The types are highly stratified, in a way that prevents you from creating anything self-referential.

The way that you do that is by building a ladder of types. Any type theory has some collection of primitive atoms. An atom is, as the name suggests, a simple object which isn’t made up of other objects. An atom is just itself – it doesn’t contain anything.

In our ladder of types, we start with the atoms. Atoms are level-0 objects. Using atoms, you can define types, which are collections of atoms. A level-1 type is defined by a predicate over level-0 objects. The level-1 type is, itself, a level-1 object. So a level-1 object is a collection of level-0 objects. A level-1 type can only range over level-0 objects, so it’s impossible for a level-1 object to contain itself. No self-reference paradox can even be written here!

You can continue the process by adding new levels. You can define level-1 predicates (that is, predicates ranging over level-1 types) – and the resulting collection is a level-2 type. And so on: any level-N type is a collection of types from level N-1, defined by a level N-1 predicate.

This produces a strict ladder of types and objects, and no type can contain anything from its own level. Russell’s paradox is averted. But the cost is complexity: most theorems that were provable in set theory are also provable in type theory, but they’re often a lot more complicated, both in how they’re stated, and in how they’re proven.

Of course, as I always say, informal explanations of formal things are always wrong. Formality exists for a reason: it allows us to say things in precise, unambiguous ways. If we want to understand even the simplest bits of type theory, we can’t just stop with the informal explanation: we need to hit the formalisms as well.

We’re going to start with the simplest version of type theory, a system called ST. ST is defined axiomatically. The axioms are, mostly, very similar to the basics of axiomatic set theory – especially to the NBG formulation. In NBG set theory, we have a collection of axioms that define what sets are and how they work. We define set equality with an axiom of extensionality; we define how we can construct new sets using logical predicate via an axiom of comprehension; we define the existence of infinite sets using an axiom of infinity. In ST type theory, we have similar axioms – identity/extensionality, comprehension, and infinity (but as we’ll see, the ST axiom of infinity is strange and back-handed compared to NBG).

The axioms explicitly capture the idea of stratification that I described informally above. In each axiom, I’ll refer to objects of one level using lowercase letters; I’ll write objects of the next higher level by appending a prime-mark to the letters. So if a is a level-1 object, then b would be a level-2 object.

ST has four axiom schemas.

  1. Axiom of Identity: x=y \Leftrightarrow (\forall z

    This is straightforward – it’s an upside-down version of the axiom of extensionality in NBG set theory. If two objects are members of exactly the same collection of types, then they’re equal. Another way of saying that is that two objects are equal if there is no predicate that can distinguish between them.

  2. Axiom of Extensionality:
    \forall x: (x \in y

    This is pretty much an exact copy of the NBG axiom of extensionality, except that it specifies the fact that an object x can only be in a type y that is one level higher than x.

  3. Axiom of Comprehension: If \phi is a Nth-order predicate, then \exists z

    This is very similar to the axiom of comprehension from NBG set theory, modified for the strict stratification of type theory. It says that if there’s a predicate over level-N objects, then the set of level-N objects that satisfy that predicate are a level N+1 type.

  4. Axiom of Infinity:
    There exists a relation, “<”, which ranges over pairs of atoms, and which is total, irreflexive, transitive, and strongly connected, such that \forall x,y: (x \ne y \Rightarrow x < y \lor y < x).

    This axiom is a strange beast. It’s defining the fact that there is an infinitely large type, but it’s doing it in a very backhanded way. In set theory, we were able to use Cantor numbers to define an infinite sequence of sets corresponding to natural numbers – and then using the construction of natural numbers with the other axioms, we could build more expansive sets of numbers – integers, reals, complex, etc.

    But in type theory, we can’t do that. The Cantor numbers are defined by using things that belong not just to different types, but to different type strata. In cantor numbers, the number N+1 is the set of the representation for N. So the cantor-0 is the empty-set, which is level-0. The Cantor-1 is the set containing the empty set, which is level 1. The Cantor 2 is the set containing the Cantor 1 – which is level 2. And so on. The canonical infinite set in axiomatic set theory is an object which can’t exist in type theory, because it’s got members that span multiple levels.

    In ST type theory, there’s no simple constructive way of building an infinite collection like the Cantor numerals which doesn’t violate the stratification of type theory. So type theory needs to go at in a different way.

    The way it does it is by defining a relation between atoms that can only be satisfied by an infinitely large set. The existence of the relation over the type implies that the type must also exist. The relation itself isn’t that hard – what’s hard about it is grasping the full implication of it. The relation is just something that behaves like numeric less-than:

    1. It’s a relation over a pair of values. You can think of it as a function, <: (a, a) \rightarrow \text{Boolean}.
    2. It’s total, meaning that every possible value x \in \text{atoms} appears as both the left and the right parameter of <: so no matter what, for any value x, there is some atom y where x < y, and some atom z where z < x.
    3. It’s irreflexive: so there is no smallest number x, where x < x.
    4. It’s transitive – so if x < y and y < z, then x < z.
    5. It’s strongly connected – so there isn’t a group of free-standing finite pools.

    All of that, together, means that there’s an infinitely large pool of numbers, and that they’ve got enough properties to represent the integers.

ST type theory is, in my opinion, a mixed bag. From the perspective of a programming language guy, we haven’t gotten anything out of it that’s particularly valuable. It’s not particularly expressive. It is a simpler system, axiomatically, than type theory – and that’s nice. But proofs written using this kind of theory as a basis are more complicated – sometimes a lot more complicated – than they’d be in NBG or ZF set theory. The additional effort to understand the set theory axioms has a payoff in making everything easier.

But ST is just a starting point. In fact, most programming language type systems are derived from a very different school of type theory: Per Martin-Lof’s intuitionistic type theory. The basic ideas are similar, but intuitionistic type theory is much more useful in computer science.

Flat Earthers Can’t Do Math!

Running this blog, I regularly check referrers – that is, the sites who’s links to GM/BM actually bring readers to the blog. It’s interesting to see who’s linking, and it helps give me an idea which posts people find most interesting. Also, every once in a while, it gives me something interesting to blog about. Like today. I got linked to by the Flat Earth Society!

The FES is the grand-daddy of hopeless crackpot organizations. They are, in all seriousness, a group of people who believe that the earth is flat. They’ll tell you that the space program is a total fraud. Every picture you’ve seen from space is faked. No one ever went to the moon. Depending on which flat-earther you talk to, satellites are either a fraud, or they’re just great big balloons floating above the earth’s surface. It’s all an eloborate conspiracy for some nefarious reason.

The FES set up a group of forums. And in one of them, someone posted something about that old -1/12 nonsense. It’s the worst misunderstanding/misrepresentation of the idea behind that that I’ve seen so far, and let me tell you, that’s really saying something.

I’ll keep this short so that it might get read.

Analytic continuation allows us to approximate an infinite series as a function. The more terms you add to the series, the more accurately you describe the function. So at the limit, when you have all the terms, that series can be considered equal to that function.

This allows us to assign meaningful numerical values to infinite series, even divergent ones.

For example, the infinite series “1 + 2 + 3 + 4 + 5… ” can be evaluated. However, the result is disturbingly counter-intuitive. If you stop adding terms at any finite point, you’ll have a larger and larger number as the result. However, if you “evaluate this after an infinite number of terms, you’ll find the sum to actually be -1/12.

There are a variety of proofs for this, and this number is demonstrably a meaningful . This result is actually seen in physics. Furthermore this result is a foundation in string theory for the number of required dimensions.

Analytic computation isn’t about converging infinite series. It’s not about adding more and more terms. What he’s describing is, simply, the idea of an infinite series that converges to a value. For example, consider the following:

 1 + \frac{1}{2} + \frac{1}{4} + \frac{1}{8} + \frac{1}{16} + \cdots

That series taken to infinity is equal to 2. You can keep drawing it out. At any point, the sum of the series is less than 2. 1 1/2, 1 3/4, 1 511/512, 1 65535/65536, on and on, forever. But if you keep following it, using the mathematical concept of limits, it’s easy to show that the sum of the full series is exactly 2.

You don’t need to bring analytic continuations into the picture to show that – just limits. In fact, analytical continuations don’t help with solving that problem – they’ve got nothing to do with it.

Analytical continuation is both much simpler (in concept) and much harder (in practice) than convergence of infinite series.

Analytical continuations come into play when we have an partial function for something, which we’re using as an partial solution for the value of something else. There are lots of problems where we don’t know a perfect, total closed-form equation for some function that we’re interested in. But we’ve managed to find a closed-form equation that matches the function we’re interested in a lot of the time. Then, using some pretty hairy complex (in the sense of complex numbers, although it’s also pretty complicated) analysis tricks, we can figure out what the value of the target function should be at places where our partial solution is undefined. So even though the partial solution doesn’t work some of the time, we can use that partial solution to derive the actual solution. That process of using analysis of the partial solution to get at least some of the undefined points where it the partial solution doesn’t work is analytical continuation.

In the case of the infamous -1/12 argument, we’re trying to probe at a really important thing called Riemman’s zeta function. The Zeta function describes fundamental properties of prime numbers. It’s an important deep thing which ends up having a lot of applications when you’re dealing with number theory, topology, and differential equations, among other things. Because of how it describes some fundamental properties, any concrete application of those fundamental properties ends up involving Zeta as well – including things like string theory, which propose a topological structure for the univese.

We don’t know, in general, how to write a simple equation for Zeta. We do know how to write an equation that is a partial subset of the zeta function – a equation that describes a function that works much of the time, but which is not zeta, and which is not defined in some places where zeta is.

Using analytical continuation, we can compute the value of the zeta function in places where the equation that we use for a partial approximation does not work, where that equation cannot and will not ever produce a result.

Using analytical continuation, \zeta(-1) = -1/12. At -1, the equation that we know for computing zeta in some places does not work. At all. But analytical continuation shows us what the value of \zeta is at that point: it does not tell us the value of computing that equation at -1: that’s doesn’t work.

(In terms of physics, the application of this is interesting. The zeta function is used in a lot of places in string theory, and it’s normally “defined” in physics text as being precisely the series that gives us the partial approximation of zeta. So in string theory physics, when you find that series, it’s not actually that series; it’s zeta, which was expanded out into that (technically incorrect) series. Since it’s zeta, you can replace it with zeta. Since zeta(-1)=-1/12, that means that in those physics equations, you can effectively pretend that 1+2+3+4+5+…=-1/12. It isn’t, but a combination of a notational convenience and a shortcut to avoid a long-winded explanation of analytical continuation means that too many physicists are taught to believe that it is.)

So, shocking as it might be: flat earthers – they’re not just wrong about geography!

Functional Programming Comes to the Macintosh! Introducing Swift!

So, Apple just recently announced a new programming language! For people like me, that’s big news. (In case you’re a relatively new reader of this blog, by background I’m not a mathematician. I’m a computer scientist, and I did my PhD in programming language design and implementation. I’m utterly obsessed with programming languages. Last time I set out to count how many language I’d learned, it was over 120, and I’ve at least read the specifications of another 30 or so since then. I don’t claim to be able to program in all of those today – but they’re all things that I have written something in at one time or another. Like I said, this is an obsession for me!)

Before I go into describing swift, I’m going to go through a bit of history. Swift is a hybrid language, in a way that reflects where it came from. To understand that, we need to see where it came from.

Where it came from: a step back into Swift’s history

To understand Swift, you need to know a bit of where it came from.

Since the dawn of OSX, the bulk of software development on the Macintosh has been done in a language caled Objective-C. Objective-C is a lovely programming language (for its time), which never really caught on outside of OSX and it’s predecessor NeXTStep. Swift is a hybrid language, combining object-oriented programming and functional programming; Objective-C, it’s ancestor, was a hybrid between old-fashioned procedural imperative programming and object-oriented programming.

Objective-C dates back to around 1984 or so. Back then, the main programming languages that were used for developing applications were predominantly procedural imperative languages, like Pascal and C. What the “imperative” part of that means is that they’re languages where you specify what you want the computer to do using a sequence of very precise steps. The procedural part means that the main structural principle in those languages is dividing code up into functional elements called procedures or subroutines.

For example, suppose you wanted to implement a binary search tree. In a procedural language, you’d write something like:

typedef struct BinarySearchTreeNode {
    char *value;
    struct BinarySearchTreeNode *left;
    struct BinarySearchTreeNode *right;
} BinarySearchTree;

BinarySearchTree *create_tree(char *str) { ... }

void add_value(BinarySearchTree *tree, char *str) { ... }

void _rebalance(BinarySearchTree *tree) { ... }

Even though you’re implementing a data structure, the fundamental code structure doesn’t reflect that. You’ve got a declaration of a datatype (the struct), and you’ve got a collection of functions. The functions aren’t associated with the declaration, or with each other. The code is organized around the functions, and any connection between the functions and the data structures – or between different functions – isn’t reflected in the structure of the code.

If you think in terms of abstractions: the only abstraction in the procedural version is that one procedure can’t access local variables defined in other procedures. All of the details of the BinarySearchTree data structure are open and accessible to anyone who feels like messing with them. Even operations – like the _rebalance function, which is intended to be only used in the implementation of other BinarySearchTree methods, is callable by anyone who wants to call it.

In the late 1980s, that started to change. The idea of object orientation came onto the scene. In object-oriented programming, you’re still writing imperative code, but the overall organization is based on data structures. You implement a data structure, and associated with it are the operations on that structure. In the object-oriented system, the operations on a data structure effectively became part of the structure itself. Re-writing our example above, in an object-oriented way, the code is similar, but the principle organizational structure changes. Instead of data type declaration and a set of functions that are only related to one another by our understanding, the functions (now called methods) are declared and implemented as part of the data structure.

@interface BinarySearchTree
- init: (NSString)str;
- addKey: (NSString)str withValue: val;
@end

@implementation BinarySearchTree {
  NSString key;
  id value;
}
- init: (NSString)str { ... }
- addNode: (NSString)str { ... }
- rebalance;
@end

Only the implementor of the BinarySearchTree can actually see the internals of the implementation. Rebalance isn’t part of the public interface of the class, and users of the BinarySearchTree can’t access it.

There’s more to object-orientation than this – in particular, there’s an idea called inheritance. Inheritance lets you declare a new data structure as being based on another:

@interface BinaryHeap: BinarySearchTree { }
- (NSString) pop;
- push: (NSString)s;
@end

Inheritance makes it easy to reuse code. To implement a heap, we don’t need to re-implement the binary search tree maintenance methods. We just implement the new methods of BinaryHeap using the BinarySearchTree operations that is inherited by the heap implementation.

Object-orientation seems obvious in retrospect, but back in the late 80s, it was absolutely revolutionary! All of us who’d been programming in old languages were entranced by this new idea, and we wanted to try it!

But there was a problem. When object-oriented programming started becoing popular, most of us were programming in C. We couldn’t just abandon C for some new language, because we relied on tons of existing code, all of which was written in C. For example, back then, I was doing most of my programming on an Amiga. The Amiga UI libraries were all written in C, and if I wanted to write an Amiga program, I needed to use those libraries. I couldn’t just grab Smalltalk and start coding, because Smalltalk couldn’t call the libraries I needed to use.

The way that we started to write object-oriented code was with hybrid languages based on C – languages that contained the familiar C that could interface with our existing systems, but which also had extensions for writing object-oriented programs. There were two main hybrids for C programmers, based on the two main schools of object-oriented programming. There was C++, based on the Simula model of object-orientation, and Objective-C, based on the Smalltalk model. With C++ or Objective-C, you could use object-oriented programming for all of your new code, while still be able to use non object-oriented libraries.

C++ is much more familiar to most people. In the mainstream community, Objective-C never caught on, but C++ became the dominant systems programming language. But Apple, because of OSX’s roots in NeXTStep, embraced Objective-C. If it wasn’t for them, Objective-C would likely have completely disappeared – outside of the Apple world, no one really used it.

Objective-C was an absolutely lovely language for its time. But it was invented around 1984 – it’s an old programming language. Lots of new ideas have come along since the days of Objective-C, and with its roots in C, it’s really hard to make any big changes to Objective-C without breaking existing code.

Now, we’re at the cusp of another big change in programming. Functional programming seems to be becoming the newest rage. The way that functional programming is catching on is very similar to the way that object-orientation did it before: by hybrids. If you look at many of the new, trendy programming languages – such as Scala, Clojure, and Rust – what you find is basically a subset which is the old familiar object-oriented language, and a bunch of functional stuff integrated into it.

With objective-C really starting to look pretty crufty, Apple did the obvious thing: they made a break, and introduced a new hybrid functional/object-oriented language, which they named Swift.

Introducing Swift

In the announcement, they described Swift as “Objective-C without the C”, but I’d describe it more as “Objective-C meets SML”. Swift is a hybrid language in the tradition of Objective-C, but instead of being a hybrid of sprocedural and object-oriented languages, it’s a hybrid of object-oriented and functional languages.

Let’s start with a simple example. In most places, it’s traditional to start with “hello world”, but I think that that’s both boring, and not particularly enlightening. I like to start with the factorial function.

func fact(n: Int) -> Int {
  if n == 0 {
    return 1
  } else {
    return n * fact(n - 1)
  }
}

let x = fact(10)
println("The factorial of 10 is \(fact(10))")

It’s pretty standard for a modern-ish language. The only thing that’s at all unusual is that if you look inside the println, you can see that Swift does string interpolation: if you put \( expression) into a string, then the result of that expression is converted into a string, and inserted into the enclosing string. That’s been common in scripting languages for a long time, but it hasn’t been a standard thing in systems programming languages like Swift. It’s a small thing, but it’s a good one.

The first big surprise in Swift is how you can test that function. In Objective-C, you would have had to create a full program, compile it, and run the executable. That’s not the case in Swift. In Swift, you can open a playground, which is a fully interactive scripting environment. It’s not that Swift comes with an interpreter – a playground is a workspace with fully access to the compiler, and it can compile and evaluate expressions on the fly! The playground isn’t limited to just text – you can create UI elements, interface builder based UIs, interactive games – just put the code into a workspace, and edit it. As the code changes, the moment it becomes syntactically valid, the playground will dynamically compile it using the LCC backend, and execute the generated code for you!

All I can say is: It’s about time! I’ve been seeing toy versions of this kind of interactivity since I was an undergrad in the 1980s. It’s about time that we got that in full blown systems language. Just this one little feature makes me really want to like Swift. And the rest of the language, while not being exceptional, is good enough to make me want to start coding in it.

In terms of syntax, Swift is mostly pretty straightforward. It’s got a clear C heritage, but with a whole lot of cleanups.

The Type System

People like me really care about type systems. Type systems can be controversial – some people love to program with strong types, and others really hate it. I’m very much in the camp that loves it. In my experience, when I’m programming in a language like SML or OCaml or Scala, which have really powerful, expressive type systems, my code very frequently ends up running correctly the first time I execute it. That’s not because I’m some kind of superhuman genius programmer, or because the languages I like somehow prevent me from making mistakes. It’s because in a strong type system, the particular kinds of mistakes that I’m most likely to make are exactly the kinds of things that will show up as a type error. I make just as many mistakes in a strongly statically typed language as I would in a dynamically typed one, but the type system catches them up front, before I can ever run my program. For my way of programming, I like that – I get all of those stupid errors out of the way quickly, so that I can spend my time tracking down the hard stuff.

Swift has a strong type system, in roughly the vein of the SML family of languages. You have the usual array of simple types (String, Int, Float, Character, etc.) In addition, you can create your own data types, and those types can be generic, with type parameters: in any declaration, you can include type parameters in angle brackets. For example, if you wanted to implement a generic list type, you could declare it as:

class List<T> {
  func insert(v: T) { ... }
  ...
}

T is a type parameter. When you declare a variable that can store a list, you need to specify the value of that type parameter:

  var l: List<Int> = ...;

You can also declare constraints on type parameters. A constraint is a way of saying “You can only use a type parameter that meets these requirements”. For example, if you wanted to implement a generic binary search tree, you’d need to be able to compare elements. If you just wrote BinarySearchTree<T>, you wouldn’t be able to use the less-than operator, because not all types can be compared that way. So you need to declare a constraint:

class BinarySearchTree<T: Comparable> { ... }

Now, if you were to try to create BinarySearchTree<Dictionary<String, String>>, you’d get a compile error. You can’t use the less-than operator on dictionaries, so they don’t satisfy the constraints.

The constraints are built using the object oriented features of Swift. Swift allows you to define something called a protocol, which is equivalent to an interface in Java, or a trait in Scala. A protocol just defines a set of methods; when you declare a class, you can declare that it implements a protocol, and the compiler will check that it implements the needed methods. When you write a type T: P, it just means that the type T implements the protocol P.

The main innovation in the type system (at least for a systems programming language) is optional types. In Swift, when you declare a variable using var foo, the variable foo will always contain a value. It can’t be nil. If you want a variable to potentially be empty, you need to explicitly say so, by declaring it with an optional type, which is written as a type-name followed by a question mark, like “var foo: String?“.

When a variable or parameter has an optional type, you can’t just access the value in that variable directly. You need to do something to check if it’s got a value in it or not. The easiest way to do that is using a conditional:

let opt_value: String? = some_function_call()
if let value = opt_value {
  value.do_something()
}

In many cases, you can make the code even simpler, by using option chaining:

let opt_value: String? = some_function_call()
opt_value?.do_something()

The question-mark in an expression does an automatic test-and-dereference. If the value is present, then the following operation is executed. If it’s absent, then the expression returns nil. The thing after the question mark doesn’t have to be a method call – it can also be a subscript, or a field reference. And you can (as the name suggests), chain these things together:

    thing_which_returns_option?.my_foo?.do_something()?[42]

Finally, you can force a dereference of a value directly using !. If you know that an option value is present, and you don’t want to write out a conditional to test it, you can append an explanation point to the end of the expression. It will generate a run-time nil-dereference error if the optional value is empty.

Handling optionality this way works a lot like what I said about static typing before. It doesn’t make errors go away – the errors that would have turned up an null pointer dereferences can still happen in your code. But most of them will be caught in advance by the compiler; and the places where null pointer reference can happen that won’t be caught by the compiler will be easy to find, because they’ll be explicit dereferences of an option, using “!”. (I’ve written about this idea before; see here for details

Object-Orientation in Swift

Let’s move on a bit. I spent a lot of time talking about data structures and object-orientation. Swift’s version of object-orientation is pretty standard for a modern programming language. For example, here’s a sketch of an implementation of a simple tree-based dictionary. (This doesn’t compile yet; it should, but right now, it crashes the compiler.)

class BinarySearchTreeDictionary<T: Comparable, S> {
  let key: T
  let value: S
  var left: BinarySearchTreeDictionary<T, S>?
  var right: BinarySearchTreeDictionary<T, S>?

  init(key: T, value: S) {
    self.key = key
    self.value = value
    self.left = nil
    self.right = nil
  }

  func insert(key: T, value: S) {
    if key > self.key {
      if let l = self.left {
        l.insert(key, value)
      } else {
        self.left = new BinarySearchTreeDictionary<T, S>(key, value)
      }
    } else {
      if let r = self.right {
        r.insert(key, value)
      } else {
        self.right = new BinarySearchTreeDictionary<T, S>(key, value)
      }
    }
  }
}

If you’ve been doing much programming in any modern language, this should mostly look pretty familiar. There are a couple of things that might need explanation.

  • One of the fields of our class is declared with “let”, and two with “var”. As I said in the introduction, Swift is a hybrid between functional and object-oriented programming. The two declaration types reflect that: identifiers declared with “let” are constants, and identifiers declared with “var” are variables. In this binary search tree, we’re not going to try to do in-place rebalancing, so we don’t need the key to be mutable.
  • The type of the left and right fields are option types, as we saw in the previous section.
  • Inside of the implementation of insert, you can see one of the effects of the optional type declaration. You can’t just use an optional value, because it might be nil. There are several ways of using optionals. In this case, we use conditional unwrapping, where you put a constant declaration into the condition of the if statement. If the optional value is present, then the constant is bound, and the body of the conditional is executed.

In Swift, classes are values that are always passed by reference. If you want to implement a class that’s passed by value, you can use a struct. Structs are declared the same way as classes, except that they (obviously) use the struct keyword instead of class. In a struct, by default, all methods are constant: they’re not allowed to modify the structure in any way. If you want a method to be able to modify the structure, you need to explicitly declare that using the mutating keyword. If you declare a method as mutating, you can change anything about it that you want – up to and including entirely replacing it by assigning a new structure value to self!

struct SearchTreeNode<Key: Comparable, Value> {
  mutating func pivot_right() {
    var tmp = self
    self = self.left
    tmp.right = self.right
    self.right = tmp
  }
}

Swift even goes as far as incorporating a bit of aspect-oriented programming in its object system. Aspect-oriented programming is a crazy thing that mostly grew out of object-orientation. The idea of it is that sometimes, you’d like to be able to inject behaviors into your code to add functionality to things like assignments. The way that you do that is by specifying that there’s some action you want to augment, and providing a function containing the code that you want to inject into that action.

For a pretty typical example, you might want to provide a public field in your class, but you want to make sure that no one can assign an invalid value to it, so when someone assigns a value, you provide code to check it for validity.

In Swift, for any field or global variable, there’s a pair of implicit functions that you can define, called willSet and didSet. willSet is called before the assignment happens, and didSet is called after.

For example, if you were implementing a volume control, and you wanted to make sure that no one set the volume higher than a user defined maximum, you could write:

struct VolumeControl {
  var max: Int
  var current: Int {
    didSet(newVolume) {
      if newVolume > max {
        current = max
      }
    }
  }
}

There’s yet another type of object or data structure that you can create with Swift. They’re called enums. From the name, you might think that enums are enumerations. They can certainly be used to implement enumerations, but they’re useful for much more than that. They’re what programming languages geeks like me call algebraic types, or what Scala calls case classes. An enum is any data type whose value can take multiple forms.

Enum types are a bit more limited than I might have liked, but they’re a really nice thing to have. They’re intended to be used for simple, lightweight values that could take several different forms. For example, a few weeks ago, I posted my parser combinator library. In the parser combinators, a parse result could be one of three things: a successful parse (which includes a product value and a parser input containing the unconsumed inputs), a failed parse (which didn’t include anything, but which indicated that the parse failed, but there wasn’t an error), or an error. To implement that in Swift, I’d use an enum:

enum ParseResult<In, Out> {
  case Success(Out, ParserInput<In>)
  case Failure
  case Error(String)
}

The way that you use enums usually comes down to pattern matching:

  val e: ParseResult<In, Out> = parser.parse(original_in)
  switch (e) {
    case .Success(let result, var rest): return other.parse(rest)
    case .Failure: return Failure
    case .Error(let msg): return Error(msg)
  }

Finally, there’s one more kind of data structure: tuples. Tuples are light-weight structures which don’t require a separate declaration of the type. You can just write tuple-values directly, and the type is inferred:

  let tuple = (1, 3, "hi there")

Tuples are a wonderful addition. The main use for tuples is allowing functions to return multiple values. You no longer need to muck about with bunching stuff into untyped lists, or stuffing some of your results into out-parameters. You can just return multiple values.

Functional Programming

The really new stuff in Swift is all functional programming stuff. Functional programming is the new hot thing in programming. For good reason. There’s two main facets to Swift’s version of functional programming: managing mutability, and first-class functions and closures.

Managing Mutability

In programming, you can’t avoid mutable state. It’s a fact. Most of the time, it’s the reason that we’re using a computer. For example, I’m using a program called Atom to write this blog post. There wouldn’t be any point is using Atom if I couldn’t modify the file I’m writing.

But mutable state makes things harder. In a large, complex software system, code which avoids mutating things is usually easier to understand, less prone to errors, less prone to unexpected side effects, and generally easier to interact with.

That’s the driving force behind the new hybrid languages: we want to be able to write functional code when it’s possible. But programming in a purely functional language is frequently really awkward, because you need state – so, in a functional language, you need to find a way to fudge the state in, using Monads, streams, or something else.

The key to using functional programming in a mutable-state world is controlling mutability. That is, you want to be able to glance at some code, and say “This is not going to change anything”, or “This might change stuff”. It’s less about making it impossible to change stuff than it is about making it clear just where stuff could be changed, and making sure that it can’t change unless you specifically declared its mutability. I’m a big fan of keeping things functional whenever it’s reasonable, as I wrote about here”.

Swift does a bunch of things to create that guarantee:

  1. Identifiers are declared with either “let” or “var”. If they’re declared with “let”, then the identifier names a constant which cannot be altered by assignment. If the value of a constant identifier is a struct or enum, its fields cannot be altered by assignment either.
  2. Methods on structs cannot alter the underlying struct unless the method is specifically annotated as “mutating”. Without that annotation in the declaration, the object cannot be altered by any of its methods.
  3. Function parameters are, by default, immutable. To allow a parameter to be changed, you need to specifically annotate it with var or inout in its declaration. If it’s a var, then changes to the parameter will not affect the original value in the caller; they will be made on a local copy.
  4. Structs and enums are passed by value. That means that the structure is (conceptually) copied when it’s passed as a parameter to a function. Unless you annotate the function parameter as an output parameter, the parameter cannot be modified; even if you call a mutating method, the mutation will be on the local copy of the value, not on the caller. (The reason for the “conceptually” up there is that the object is copied lazily; if you try to alter it, the copy happens at the point of the first alteration, so passing complex structures by-value doesn’t incur a copy cost unless you modify it.)

Functions and Closures

The other side of the functional programming support isn’t about restricting things, but about enabling new things. And here Swift really shines. Swift has support for first class functions (function parameter and return values), anonymous functions, curried functions, and full closures.

Swift’s support for first class functions means that functions are just values, like any other value type. A swift function can be assigned to a variable, passed to a function, or returned as the result type of a function.

For example, suppose you wanted to write a generic sort function – that is, a sort function that didn’t just compare values using the standard less-than operator, but which could take any function that a user wanted to do comparisons. In Swift, you could write:

  func sort_generic<T>(list: Array<T>, comparator: (T, T) -> Bool) -> Array<T> {
    ...
    if comparator(v, w) { ... }
    ...
  }

This is something that those of us with experience with Lisp have been absolutely dying to have in a mainstream language for decades.

Closures are a closely related concept. A closure is a function value with one really interesting property. It closes over the environment in which it was declared. To understand what I mean, let’s look at a really simple example, copied from the Swift specification.

func makeIncrementor(amount: Int) -> () -> Int {
  var runningTotal = 0
  func incrementor() -> Int {
      runningTotal += amount
      return runningTotal
  }
  return incrementor
}

This function returns a value which is, itself a function. The interesting thing is that the function can use any variable defined in any of the scopes enclosing its declaration. So the function incrementor can access the amount parameter and the runningTotal variable, even after the makeIncrementor function has returned. Since those are local to the invocation, each time you call makeIncrementor, it creates new variables, which aren’t shared with other invocations.

So let’s look at what happens when you run it:

let f = makeIncrementor(2)
let g = makeIncrementor(5)
f() 2
f() 4
g() 5
f() 6
g() 10

Anonymous functions make it really easy to work with first-class functions. You don’t need to write a function declaration and then return it the way the example above did. Any time you need a function value, you can create it in-place as an expression.

func makeAnonIncrementor(amount: Int) -> () -> Int {
  var runningTotal = 0
  return {
    runningTotal += amount
    return runningTotal
  }
}

If the function anonymous function takes parameters, you declare them before the function body with “in”:

  sort_generic(mylist, { (x: Int, y: Int) -> Bool in return x > y})

Currying, finally, is a shorthand way of writing function values. The idea is that if you have a two-parameter function, you can rewrite it as a one parameter function that returns another one parameter function. That sounds confusing until you see it:

  func add_numbers(x: Int, y: Int) -> Int {
      return x + y
  }

  func curried_add_numbers(x: Int) -> Int -> Int {
    return { (y: Int) -> Int in return x + y }
  }

If I want to add 3+2, I can either call add_numbers(3, 2), or curried_add_numbers(3)(2): they do the same thing.

Swift provides a special way of declaring curried functions:

  func better_curried_add_numbers(x: Int)(y: Int) -> Int {
    return x + y
  }

Pattern Matching

Pattern matching isn’t, strictly speaking, a functional language thing; but it’s an idea that was introduced to most programmers by its inclusion in functional programming languages. The idea is simple: you can write assignments or conditionals that automatically decompose a data structure by matching the structural pattern of that data structure.

As usual, that becomes a lot clearer with an example.

    let (x, y, z) = (1, 2.7, "three")
  

The right hand side of that assignment structure is a tuple with three values. The first one is an integer, the second is a floating point number, and the third is a string. The left-hand side of the assignment has exactly the same structure – so the Swift compiler will match the pieces. That’s equivalent to:

    let x = 1
    let y = 2.7
    let z = "three"
  

That’s particularly useful for multiple return values. Strictly speaking, Swift doesn’t really have multiple return values: every function returns exactly one value. But that one value may be a tuple containing multiple values. So you can write
things like:

  let result, error_core = my_function(parameters)

Pattern matching also happens in switch statements, where each branch of the switch can be a different pattern, as we saw earlier in the ParseResult example.

All of this stuff means that I can write really beautiful functional code in Swift. And that’s a really, really good thing.

The Warts

For the most part, I’ve been saying nice things about Swift. But it’s not all goodness. There are some problems, and some of them are pretty big.

The biggest thing is: no concurrency, no threading, no locks, no message passing. There’s absolutely no mention of concurrency at all. These days, that’s downright shocking. My phone has 4 CPU cores. Every machine that this language is intended to program, from the iPhone to the iPad to the Macintosh, has multiple CPUs, and programs for them need to deal with concurrency. But there’s not a shred of support in the language. That is, to put it mildly, absolutely insane. You can, of course, hack concurrency in via libraries, but most recent languages – Rust and Go come to mind – make concurrency a fundamental goal for a really good reason: concurrency is hard to get right, and concurrency hacks come at a significant cost in efficiency, correctness, and optimizibility. (Even older languages like Java have concurrency deeply embedded in the structure of the language for exactly that reason; leaving it out of swift is just shocking.)

Another big one is exception handling. Again, there’s absolutely nothing in Swift. This is particularly surprising because Objective-C had an exception handling system retrofitted into it. The libraries that Swift needs to be able to interact with use an ugly macro-based exception handling system – why is there nothing for it in Swift?

There are also a fair number of smaller issues:

  • The syntax is decidedly odd at times. Not a big deal. But there are some particular syntactic warts. There’s a range expression, which is fantastic. In fact, there are two, and they’re really hard to tell apart. 1..4 is a shorthand for (1, 2, 3); 1...4 is a shorthand for (1, 2, 3, 4). I predict much pain from off-by-one errors caused by using the wrong one.
  • The different ways of declaring objects have seemingly arbitrary rules. A struct is allowed to have class variables; a class can’t. Why? I have no idea; the limitation is simple stated in the docs as a fact.
  • Optionals aren’t as powerful as they could be. If you look at a language like Scala, optionals are implemented using the same type semantics as anything else: they’re a parametric type, Option[T]. That makes it possible to do a bunch of really nice stuff without needing to have any special cases wired into the language. In Swift, they’re a special case, and limits in the type system make it much harder to do many things. As a result, there’s a bunch of special case syntax for things like “option chaining” and forced deferencing. This isn’t a huge deal, but it’s frustrating.

And the big problem at the moment: the implementation is incredibly buggy. Not just a little bit buggy: virtually every code example in this article crashed the compiler. Obviously, it’s very early days for Swift, so it shouldn’t surprise anyone that the implementation is immature and buggy, but the degree of bugginess is astonishing. Examples from Apple’s own book on Swift crash the compiler! They’re claiming that with the release of OSX Yosemite this fall that you should be able to start writing real applications using Swift. They’ve got a long way to go, and not a lot of time if that’s going to be true.

Conclusion

This article, despite being ridiculously long, still only really scratches the surface of Swift. I haven’t talked about how Swift does arrays and dictionaries, which is really interesting. I haven’t talked much about syntax. I barely touched on pattern matching and options. I didn’t mention the module system at all. I didn’t talk about named parameters, which are a bit weird, but nice. There’s so much more to Swift than I could possible talk about here.

The thing to take away, then, is that overall, Swift is very exciting. Functional/Object-Oriented hybrid programming, with a strong parametric type system, and first-class interactivity in a systems programming language! I’m really looking forward to using it. I’m desperately hoping that Apple will open-source the compiler, because I want to be able to use Swift for lots of things, not just Macintosh programming. I don’t have super-high hopes for it, but it’s definitely possible, and I expect that open-source people are probably already working on a GCC front-end.

As an experiment, I’ve been trying to port my parser combinators to Swift. But at the moment, the Swift compiler chokes on the code. When I manage to debug my code/Apple manages to debug their compiler enough to make it work, I’ll post an update with that code, and more info about what it’s really like to write Swift code.

Don’t worry about playing with guns. You can’t hurt anyone.

Pardon me. Someone is wrong on the internet. I must do something!

Some stupid fucking dumb-ass idiot was playing with a loaded gun. He knew it was loaded. And he grabbed it by the trigger to pick it up. Because, you see, he knew that it’s a persnickety old gun, and the trigger usually jams, so he figured it’d be safe to grab it by the trigger. What could possibly go wrong?

Naturally, it went off, and hit his next door neighbor in the head, killing him. He’d just brought his wife and newborn child home when he was killed by the spectacular stupidity of his neighbor.

The police, discussing the case, said:

“The odds, I’d guess, are 1 in infinity,” said BCSO Maj. Tommy Ford. “This was just tragic.”

Those of us who aren’t mathematical morons know that a “1 in infinity” chance is the probability better known as 0.

You might say that I’m being pedantic. You’d be right. But it’s a stupid statement that tries to minimize the incredible stupidity of what happened here. This wasn’t a crazy freakish chance. A handgun is a device which is specifically designed to be an efficient and effective means for killing people. It is not a toy. Picking up a gun by its trigger is, for all intents and purposes, no different from just randomly aiming the gun and pulling that trigger. The chances of hitting someone aren’t huge, but they aren’t tiny, either.

This wasn’t a super-rare freak accident. This was stupidity and negligence by a jackass. Diminishing it, trying to pretend that it was just freakish is a way of making excuses for the
sub-human scumbag who killed an innocent man. Calling it one-in-infinity – that is, saying that it was impossible even though it wasn’t even particularly unlikely – is just a way of covering up for the fact that our insanely irresponsible way of dealing with deadly weapons kills innocent people.

We do a lot of that in America. Guns are downright sacred here. You can insult Jesus with less repurcussions that insulting a gun owner. A community figure like a local policeman can’t just point out that a gun was used in a horrible, stupid, irresponsible, evil way. Because that would be seen as a threat to the so-called “guns rights” shits who think that any number of innocents getting killed is an acceptable price in order to ensure that they can keep their precious penis replacements.

The man who killed his neighbor in this incident should never have been able to have that gun. He was a convicted felon, prohibited from owning a gun by state law. But we can’t do something sensible like, say, check whether someone can legally own a gun before letting them buy one. That would be an unacceptable infringement on their freedom.

Meanwhile, this shit is being charged with manslaughter. After all, it wasn’t murder. He was just playing with his precious, precious toy.

The beauty of math; the humor of stupidity.

%d bloggers like this: