## Types Gone Wild! SKI at Compile-Time

Over the weekend, a couple of my Foursquare coworkers and I were chatting on twitter, and one of my smartest coworkers, a great guy named Jorge Ortiz, pointed out that type inference in Scala (the language we use at Foursquare, and also pretty much my favorite language) is Turing complete.

Somehow, I hadn't seen this before, and it absolutely blew my mind. So I asked Jorge for a link to the proof. The link he sent me is a really beautiful blog post. It doesn't just prove that Scala type inference is Turing complete, but it does it in a remarkably beautiful way.

Before I get to the proof, what does this mean?

A system is Turing complete when it can perform any possible computation that could be performed on any other computing device. The Turing machine is, obviously, Turing complete. So is lambda calculus, the Minsky machine, the Brainfuck computing model, and the Scala programming language itself.

If type inference is Turing complete, then that means that you can write a Scala program where, in order to type-check the program, the compiler has to run an arbitrary program to completion. It means that there are, at least theoretically, Scala programs where the compiler will take forever - literally forever - to determine whether or not a given program contains a type error. Needless to say, I consider this to be a bad thing. Personally, I'd really prefer to see the type system be less flexible. In fact, I'd go so far as to say that this is a fundamental error in the design of Scala, and a big strike against it as a language. Having a type-checking system which isn't guaranteed to terminate is bad.

But let's put that aside: Scala is pretty entrenched in the community that uses it, and they've accepted this as a tradeoff. How did the blog author, Michael Dürig, prove that Scala type checking is Turing complete? By showing how to implement a variant of lambda calculus called SKI combinator calculus entirely with types.

SKI calculus is seriously cool. We know that lambda calculus is Turing complete. It turns out that for any lambda calculus expression, there's a way rewriting it without any variables, and without any lambdas at all, using three canonical master functions. If you've got those three, then you can write anything, anything at all. The three are called S, K, and I.

• The S combinator is: .
• The K combinator is: .
• The I combinator is: .

They come from intuitionistic logic, where they're fundamental axioms that describe how intuitionistic implication works. K is the rule ; S is the rule ; and I is .

Given any lambda calculus expression, you can rewrite it as a chain of SKIs. (If you're interested in seeing how, please just ask in the comments; if enough people are interested, I'll write it up.) What the author of the post id is show how to implement the S, K, and I combinators in Scala types.

trait Term {
type ap[x <: Term] <: Term
type eval <: Term
}


He's created a type Term, which is the supertype of any computable fragment written in this type-SKI. Since everything is a function, all terms have to have two methods: one of them is a one-parameter "function" which applies the term to a parameter, and the second is a "function" which simplifies the term into canonical form.

He implements the S, K, and I combinators as traits that extend Term. We'll start with the simplest one, the I combinator.

trait I extends Term {
type ap[x <: Term] = I1[x]
type eval = I
}

trait I1[x <: Term] extends Term {
type ap[y <: Term] = eval#ap[y]
type eval = x#eval
}


I needs to take a parameter, so its apply type-function takes a parameter x, and returns a new type I1[x] which has the parameter encoded into it. Evaluating I1[x] does exactly what you'd want from the I combinator with its parameter - it returns it.

The apply "method" of I1 looks strange. What you have to remember is that in lambda calculus (and in the SKI combinator calculus), everything is a function - so even after evaluating I.ap[x] to some other type, it's still a type function. So it still needs to be applicable. Applying it is exactly the same thing as applying its parameter.

So if have any type A, if you write something like var a : I.ap[A].eval, the type of a will evaluate to A. If you apply I.ap[A].ap[Z], it's equivalent to taking the result of evaluating I.ap[A], giving you A, and then applying that to Z.

The K combinator is much more interesting:

// The K combinator
trait K extends Term {
type ap[x <: Term] = K1[x]
type eval = K
}

trait K1[x <: Term] extends Term {
type ap[y <: Term] = K2[x, y]
type eval = K1[x]
}

trait K2[x <: Term, y <: Term] extends Term {
type ap[z <: Term] = eval#ap[z]
type eval = x#eval
}


It's written in curried form, so it's a type trait K, which returns a type trait K1, which takes a parameter and returns a type trait K2.

The implementation is a whole lot trickier, but it's the same basic mechanics. Applying K.ap[X] gives you K1[X]. Applying that to Y with K1[X].ap[Y] gives you K2[K, Y]. Evaluating that gives you X.

The S combinator is more of the same.

// The S combinator
trait S extends Term {
type ap[x <: Term] = S1[x]
type eval = S
}

trait S1[x <: Term] extends Term {
type ap[y <: Term] = S2[x, y]
type eval = S1[x]
}

trait S2[x <: Term, y <: Term] extends Term {
type ap[z <: Term] = S3[x, y, z]
type eval = S2[x, y]
}

trait S3[x <: Term, y <: Term, z <: Term] extends Term {
type ap[v <: Term] = eval#ap[v]
type eval = x#ap[z]#ap[y#ap[z]]#eval
}



Michid then goes on to show examples of how to use these beasts. He implements equality testing, and then shows how to test if different type-expressions evaluate to the same thing. And all of this happens at compile time. If the equality test fails, then it's a type error at compile time!

It's a brilliant little proof. Even if you can't read Scala syntax, and you don't really understand Scala type inference, as long as you know SKI, you can look at the equality comparisons, and see how it works in SKI. It's really beautiful.

## Static Typing: Give me a break!

I'm a software engineer. I write code for a living. I'm also a programming language junkie. I love programming languages. I'm obsessed with programming languages. I've taught myself more programming languages than any sane person has any reason to know.

Learning that many languages, I've developed some pretty strong opinions about what makes a good language, and what kind of things I really want to see in the languages that I use.

My number one preference: strong static typing. That's part of a more general preference, for preserving information. When I'm programming, I know what kind of thing I expect in a parameter, and I know what I expect to return. When I'm programming in a weakly typed language, I find that I'm constantly throwing information away, because I can't actually say what I know about the program. I can't put my knowledge about the expected behavior into the code. I don't think that that's a good thing.

But... (you knew there was a but coming, didn't you?)

This is my preference. I believe that it's right, but I also believe that reasonable people can disagree. Just because you don't think the same way that I do doesn't mean that you're an idiot. It's entirely possible for someone to know as much as I do about programming languages and have a different opinion. We're talking about preferences.

Sadly, that kind of attitude is something that is entirely too uncommon. I seriously wonder somethings if I'm crazy, because it seems like everywhere I look, on every topic, no matter how trivial, most people absolutely reject the idea that it's possible for an intelligent, knowledgeable person to disagree with them. It doesn't matter what the subject is: politics, religion, music, or programming languages.

What brought this little rant on is that someone sent me a link to a comic, called "Cartesian Closed Comic". It's a programming language geek comic. But what bugs me is this comic. Which seems to be utterly typical of the kind of attitude that I'm griping about.

See, this is a pseudo-humorous way of saying "Everyone who disagrees with me is an idiot". It's not that reasonable people can disagree. It's that people who disagree with me only disagree because they're ignorant. If you like static typing, you probably know type theory. If you don't like static typing, that there's almost no chance that you know anything about type theory. So the reason that those stupid dynamic typing people don't agree with people like me is because they just don't know as much as I do. And the reason that arguments with them don't go anywhere isn't because we have different subjective preferences: it's because they're just too ignorant to understand why I'm right and they're wrong.

Most programmers - whether they prefer static typing or not - don't know type theory. Most of the arguments about whether to use static or dynamic typing aren't based on type theory. It's just the same old snobbery, the "you can't disagree with me unless you're an idiot".

Among intelligent skilled engineers, the static versus dynamic typing thing really comes down to a simple, subjective argument:

Static typing proponents believe that expressing intentions in a static checkable form is worth the additional effort of making all of the code type-correct.

Dynamic typing proponents believe that it's not: that strong typing creates an additional hoop that the programmer needs to jump through in order to get a working system.

Who's right? In fact, I don't think that either side is universally right. Building a real working system is a complex thing. There's a complex interplay of design, implementation, and testing. What static typing really does is take some amount of stuff that could be checked with testing, and allows the compiler the check it in an abstract way, instead of with specific tests.

Is it easier to write code with type declarations, or with additional tests? Depends on the engineers and the system that they're building.

## Turing Crackpottery!

One of the long-time cranks who's commented on this blog is a bozo who goes by the name "Vorlath". Vorlath is a hard-core Cantor crank, and so he usually shows up to rant whenever the subject of Cantor comes up. But last week, while I was busy dealing with the Scientopia site hosting trouble, a reader sent me a link to a piece Vorlath wrote about the Halting problem. Apparently, he doesn't like that proof either.

Personally, the proof that the halting problem is unsolvable is one of my all-time favorite mathematical proofs. It's incredibly simple - just a couple of steps. It's very concrete - the key to the proof is a program that you can actually write, easily, in a couple of lines of code in a scripting language. And best of all, it's incredibly profound - it proves something very similar to Gödel's incompleteness theorem. It's wonderful.

To show you how simple it is, I'm going to walk you through it - in all of its technical details.

## Return of the Revenge of the Return of the Compression Schmuck

Well, folks, this one is going to be boring for most of you. But the
compression jackass, Jules "Julie-baby-dumbass" Gilbert has been repeatedly
bugging me. And today, he replied to my latest "fuck off and stop sending me
mail" with a long-winded proselytizing response in which he requested that I
be courteous and not publicize the discussion of his "work".

Fuck that

The entire correspondence is below.

Before I get to it: the short summary of what Jules is doing
is munging a file in a way that makes it amenable to recompression. In
the classic sense, this is removing a trivial bit of information from the
file, which thus allows is to be re-compressed just a tiny bit
more.

The catch is, of course, you can't un-compress it without re-introducing
the information that you removed. In his case, you need to repeatedly
un-compress, un-munge, un-compress, un-munge, and so on -
exactly the right number of times. From some of his emails, he
does this hundreds to thousands of times.

You can't un-compress his stuff without knowing how many times the compressor
ran. And how many times is that? Well, gosh, to know that, you need to know
some extra information. Anyone want to take a bet on what the
relationship is between the amount of additional compression he can get, and
the number of repetitions of his system? Anyone?

Ok. On to the transcript.

## Revenge of the Return of the Compression Idiot

Do I really need to go through this again? Argh!

As long-time readers will remember, a while back, I had an encounter with
a crackpot named Jules Gilbert who claimed to be able to cyclically compress
files. That is, he could take a particular input file, compress it, do
something to it, and then compress it again, making it smaller. He claimed to
be able to do this for any input.

And to make it more annoying, his claim to be able to do this brilliant
magical cyclical compression was attached to an obnoxious christian "I want to
save you soul" rant, where he effectively offered to share the profits from
this brilliant invention with me, if I'd only give him the chance to tell me

I tried to get rid of the schmuck. I asked him to leave me alone politely.
Then I asked him to leave me alone not-so politely. Then I asked him to
leave me alone very, very rudely. Then I publicly mocked him on this blog.
After the last, he finally seemed to take the hint and go away.

Unfortunately, good things often don't last. And yesterday, I received
another new message from him, bragging about the results of his uber-magical
compression system. He has now perfected it to the point where he can take
any input file, and compress it down to about 50K:

I am now compressing single bit as:

I use C code to pack up one bit to a byte and call bzip2's compress
buffer.

I print the result and compute the size.

(I did this for both gzip and bzip2.) Gzip didn't compress; it gave
me back about 6.25, but I needed at least 8.0.

And bzip2 gave it to me. About 8.2 and higher. (This is with no
actual I/O, just buffer to buffer.)

This was with random data. At least that's what people call it.
Bzip2 data. (It looks pretty random to me.)

I expect to show up at a friend's house and show him the system on
Monday. THIS IS NOT A COMPLETE SYSTEM, but it's not just research
either. The input was randomly chosen (not by me, by a C function,)
and the program has been arranged to simply open another file when a
current file is exhausted.

Every input file has been compressed once with bzip2. Each input file
is at least 5k bytes and was chosen with the intent to represent all
popular OS's somewhat equally.

This program is easily able to process MN's 415k file. And since it
uses 256 byte blocks, I can bring it down to about 50k (number
demonstrated in testing.) Another way to say this is that (with this
program,) all files greater than about 50k can be made that small.

This is the simplist system I have ever made that uses my "modern"

techniques (I mean, not my LSQ ideas of a decade ago.) i started
coding it this morning, to see if a certain idea worked...

I'm trying to drop bzip but it's pretty good! I'm also trying to
modulate my input to it, in order to obtain a gain from the pattern
recognition (the BWT may not be an actual FFT but it's a similar
idea.) If I can do this I will keep it.

If all this is greek to you, here's the thing: Just about every other
computer scientist in the whole wide world believes this is
impossible. Why is this valuable? Because it means that all files
and messages can be compressed in while in transit to, say, 50k --
probably much less. (Or while sitting on a CD-ROM or DVD.)

I love that line in there: "Just about every other computer scientist in
the whole wide world believes this is impossible".

Jules, baby, belief has nothing to do with it.

## Animal Experimentation and Simulation

In my post yesterday, I briefly mentioned the problem with simulations
as a replacement for animal testing. But I've gotten a couple of self-righteous
emails from people criticizing that: they've all argued that given the
quantity of computational resources available to us today, of course
we can do all of our research using simulations. I'll quote a typical example
from the one person who actually posted a comment along these lines:

This doesn't in any way reduce the importance of informing people about
the alternatives to animal testing. It strikes me as odd that the author of
the blogpost is a computer scientist, yet seems uninformed about the fact,
that the most interesting alternatives to animal testing are coming from that
field. Simulation of very complex systems is around the corner, especially
since computing power is becoming cheaper all the time.

That said, I also do think it's OK to voice opposition to animal testing,
because there *are* alternatives. People who ignore the alternatives seem to
have other issues going on, for example a sort of pleasure at the idea of
power over others - also nonhumans.

I'll briefly comment on the obnoxious self-righteousness of this idiot.
They started off their comment with the suggestion that the people who are
harassing Dr. Ringach's children aren't really animal rights
protestors; they're people paid by opponents of the AR movement in order to
discredit it. And then goes on to claim that anyone who doesn't see the
obvious alternatives to animal testing really do it because they
get their rocks off torturing poor defenseless animals.

Dumbass.

Anyway: my actual argument is below the fold.

## The Return of the Compression Idiot

Remember a while back, I wrote about a crackpot who pestered me both about
converting to Christianity, and his wonderful, miraculous compression system? He
claimed to be able to repeatedly compress any file, making it smaller each time.

Well, he's back pestering me again. Repeatedly asking him to leave me alone,
shouting at him, etc., hasn't worked. (His current claim is that he doesn't know how
to delete me from his gmail contacts list.) So I'm resorting to another round of
public humiliation, which I hope will be informative and entertaining as well.

## I Get Mail: Iterative Compression

Like a lot of other bloggers, I often get annoying email from people. This week, I've been dealing with a particularly annoying jerk, who's been bothering me for multiple reasons. First, he wants me to "lay off" the Christians (because if I don't, God's gonna get me). Second, he wants to convince me to become a Christian. And third, he wants to sell me on his brilliant new compression scheme.

See, aside from the religious stuff, he's a technical visionary. He's invented a method where he can take a source document, and repeatedly compress it, making it smaller each time.

This is a stupid idea that I've seen entirely too many times. But instead of just making fun of it, I thought it would be interesting to explain in detail why it doesn't work. It touches on a bunch of basic facts about how data compression works, and provides a nice excuse for me to write a bit about compression.

The basic idea of data compression is that you're eliminating redundancies in the original text. You can't discard information. Mathematically, a compression function is an invertible function C from an array of characters to an array of characters (or you could use bits if you prefer), such that if y=C(x), then on the average input, the length of y is smaller than the length of x.

An ideal compression system is one where for all possible values of x, C(x) is shorter than x. C is your compressor; and since C is reversible, it has a unique inverse function C-1 such that C-1(C(x)) = x. An illustration of this basic compression system is in the diagram to the side.

## The Z2K9 Problem

I've been getting a lot of emails asking about the so-called "Z2K9" problem.

For those who haven't heard, the software on a particular model of Microsoft's Zune music player froze up on New Year's eve, because of a bug. Apparently, they didn't
handle the fact that a leap year has 366 days - so on the 366th day of 2008, they froze up for the day, and couldn't even finish booting.

Lots of people want to know why on earth the player would freeze up over something like this. There was no problem with the date February 29th. There was nothing wrong with the date December 31st 2009. Why would they even be counting the days of the year, much less being so sensitive to them that they could crash the entire device for a full day?

The answer is: I don't have a damned clue. For the life of me, I can't figure out
why they would do that. It makes absolutely no sense.

## The Excel 65,535=100,000 Bug

I've been getting a lot of requests from people to talk about the recent Excel bug. For those of
a number very, very close to either 65,535 or 65,536 are displaying their result as 100,000.
It's only in the display though - the underlying number is actually represented correctly, so if you subtract 2 from 65,536, you'll get the correct answer of 65,534 - not 99,998.

I can't give you the specifics - because without seeing the Excel code, I can't tell exactly what they got wrong. But I've got some pretty good suspicions, so I'll do my best to explain the background that leads to the problem, and what I think is probably going on. (Another excellent explanation if this
is in the Wolfram blog post that I mentioned in my fast arithmetic fractals post this weekend.)

Older posts »

• Scientopia Blogs

• ## Tags

Bad Behavior has blocked 1068 access attempts in the last 7 days.