Obj-C’s type system is too strong

That’s rather a surprising title, isn’t it! Objective-C has one of the weakest type systems of any language. What I’m going to demonstrate though, is that with the addition of Objective-C’s “block” construct (really closures with a special name), Objective-C’s type system is now not only too weak for my tastes, but too strong to do useful things!

In short, Objective-C’s type system is broken, not only does it allow lots of incorrect programs that many type systems disallow, but it also disallows a fair number of correct programs that it shouldn’t.

Blocks

Objective-C gained a really useful feature lately – the closure. We can define a closure like so:

// Define a closure that multiplies it's argument by a variable 'a'.
- (void)myClosureDefiningMethod
{
    int a = 5;
    int (^timesA)(int x) = ^(int x) { return x * a; };
}

The syntax isn’t the prettiest in the world, but it mirrors C function pointer syntax, so it’s not all bad.

Higher Order Programming

The ability to create functions on the fly like this is really powerful, so much so, that whole languages (like Haskell) base their programming style on doing this kind of thing lots. Let’s then, turn to Haskell for inspiration about what kinds of things we might want to do with this.

The standard Haskell library (the Prelude) defines some really stunningly simple things using this technique, and the lovely thing is that they turn out to be quite useful. Lets look at const for example:

const :: a -> b -> a
const x y = x

So, we pass const an argument, and what we get back is a new function that ignores it’s argument, and returns our original one. It’s dead simple, but mega useful.

Lets try to define the same function with Obj-C closures then:

(a (^)(b ignore))constantly(a ret)
{
    return ^(b ignore){ return ret; };
}

This looks great! We have our const function, but wait, I’ve cheated. I’ve not defined the return type of the closure, or the type of constantly’s argument properly. What I want to be able to say is, in typical C weak typing fashion, “any type at all”. This, although it wouldn’t specify the type very strongly, would at least allow me to use the function. Unfortunately, neither C, nor Obj-C has such a type. The closest you can reasonably get is void *, and that won’t admit a whole swathe of useful types like BOOL, int, float etc.

Exponentiation Types

A pair colleagues of mine and I have been staring at an interesting riddle, which I’m guessing exists in the literature somewhere. He pointed out that we have sum types where a+b is the type containing all the values in a, and all the values in b, we have product types where a*b is the type containing all the values which contain an a, and a b. What we don’t have though is exponentiation types. The riddle then – what is the type ab?

Bart realised that this type is b -> a. The type contains all functions that map bs onto as. This has some rather nice mathematical properties. We know from our early maths a couple of rules about exponents:

ab * ac = ab+c

This gives us a rather nice isomorphism: (b -> a, c -> a) is equivalent to (b + c) -> a. That is, if we have one function that produces an a from bs, another that gives us an a from cs, we can write a function that gives us as, given either a b or a c, and vice versa.

Secondly, and perhaps even nicer
(ab)c = ab*c

This gives us a different isomorphism: c -> b -> a is equivalent to (b,c) -> a. Woohoo, we have currying!

This seems very close to the curry-howard isomorphism, but not quite there. Does anyone know who’s discovered this already?