Dependent types and plus
Tuesday, January 4th, 2011My story starts with a simple function: +
Starting with Java… tell me what’s wrong with this picture?
public void blah() {
int x = 3;
int y = 5;
int z = x + y;
System.out.println("z = " + z);
}
z evaluates fine… but what about this?
public void blah() {
int x = Integer.MAX_VALUE;
int y = Integer.MAX_VALUE;
int z = x + y;
System.out.println("z = " + z);
}
Apparently z = -2. AAAAAAAAAAAAAARGH! That’s nonsensical! Surely an exception would be better than an incorrect value. Yes, incorrect. No, I don’t care about the semantics of overflows in 32-bit calculations in CPUs. It’s just plain wrong. For the purposes of discussion, let’s just pretend + doesn’t terminate when it overflows.
Ok, so why does the compiler allow this? What’s going on?
In maths, integers are closed under addition – i.e. int + int = int. This relies on the integers being unbounded. In (most? all?) programming languges, we only have bounded integers. Bounded integers are not closed under addition.
So, + is int -> int -> int… but this is only correct for unbounded integers. For bounded integers, + is really int -> int -> long
Why long? Simply that Integer.MAX_VALUE + Integer.MAX_VALUE <= Long.MAX_VALUE.
So, in java, an int is an integral type with bounds -2,147,483,648 … 2,147,483,647 (Integer.MIN_VALUE and MAX_VALUE). Let’s denote this as int[-2,147,483,648, 2,147,483,647]. Similarly, long would be int[-9,223,372,036,854,775,808, 9,223,372,036,854,775,807]. Then, + would be:
int[-2,147,483,648, 2,147,483,647] -> int[-2,147,483,648, 2,147,483,647] -> int[-9,223,372,036,854,775,808, 9,223,372,036,854,775,807]
But, 2,147,483,647 + 2,147,483,647 = 4294967294, which is far less than the long bound. So, we could say + is:
int[-2,147,483,648, 2,147,483,647] -> int[-2147483648, 2147483647] -> int[−4,294,967,296, 4,294,967,294]
My head is spinning from big numbers. Sorry. Anyway, this pattern generalises to:
+ :: int[a1, b1] + int[a2, b2] -> int[a1 + a2, a2 + b2]
Note, above, the result of the addition could fit into either a int[-9,223,372,036,854,775,808, 9,223,372,036,854,775,807] or an int[−4294967296, 4294967294] – i.e. a value of the narrower type could fit into the larger type. So we could say that:
int[a1, b1] is a subtype of int[a2, b2] for all a1 <= a2 and b1 >= b2
Back to +, notice that the return type is actually defined in terms of +! How can that be? Well, there’s something missing from the definition of +.
+ :: int[a1, b1] + int[a2, b2] -> int[a1 + a2, a2 + b2] for all a1, a2, b1, b2 :: int[-∞, ∞]
As such, + for bounded integers is defined in terms of + for unbounded integers. We just need an unbounded integer type. I haven’t seen one in practise yet – we seem to be stuck with bounded integers as they easily map to the underlying hardware. We need to break free of this – we need the unbounded integers we take for granted in pure maths, and then, if we need bounded integers, implement them in terms of unbounded integers. Then, we can optimise for hardware capabilities in the compiler and runtime.
A similar recursive definition happens with values. Take the value 3. What type is it? Well, a 3 can’t be more than 3 or less than 3, so it’s bounds are 3 and 3. i.e. int[3, 3]. More generally, x :: int[x, x] for all x :: int[-∞, ∞]. This gives us one type for each value – as such, what is the difference between the value 3 and the once-inhabited type int[3, 3]? What really is the difference between a type and a value? I can imagine a type system whereby types and values are completely unified, rather than distinct concepts.
Anyway, let’s look at a practical example. Take the expression 3 + 4. Adding type annotations:
3 :: int[3, 3] + 4 :: int[4, 4]
and it would evaluate to 7 :: int[7, 7]
but, I could also say: z :: int[0, 256] = 3 + 4, because int[0, 256] is a supertype of int[7, 7]
So, if we type-alias, say, smallint = int[0, 256], I can say: z :: smallint = 3 + 4. This is looking more like normal code. Now, if java did this, then int x = Integer.MAX_VALUE + Integer.MAX_VALUE wouldn’t type-check, but long x = Integer.MAX_VALUE + Integer.MAX_VALUE would.
Ahhhhhhhhhhhhhhhhhhh. Sigh of relief. That’s so much better!
But, what happens if I need to narrow a type? Say, I have an integer from user input, which could be anything, but I need to store it in, say, an int[0, 256]? Yawn. It’s just validation, and we just need a function like this:
narrow :: int[a1, b1] -> Maybe int[a2, b2]
This all seems a lot for just avoiding integer overflows, but it has potential to prevent bugs, and this is just the tip of the iceberg for dependent types.
