Lambda the Ultimate

It's a good point. Languages meant for general use should probably support rational bignums as the default; when you need the performance of hardware floating point, you should have to request it explicitly.

Come to think of it, even rational bignums might not be good enough for some cases; you might want symbolic arithmetic (2*sqrt(2)-sqrt(2)==sqrt(2), not 1.414...). Don't do any conversion until you have to display a result to the user.

What do you mean by "bounded natural numbers"? Do you mean twos-complement 32-bit ints, or the groups of 0..n-1 with arithmetic mod n? I have long wished for the latter.

Sid Meier's trick was to divide 2^32 by n and use that as ONE, and so on, letting the twos-complementedness mod everything for him. (Only works for powers of 2, though, and don't index your array with ONE!) A cute trick.

Do you mean twos-complement 32-bit ints, or the groups of 0..n-1 with arithmetic mod n?

I think the whole point of dependent types is being greedy about information, not letting it perish, or be diluted.

Could you elaborate about ONE? I am not sure I understood the idea.

"Could you elaborate about ONE? I am not sure I understood the idea."

Speaking of interpreting other people's posts... I'm assuming he means something like this:

Suppose you want to represent arithmetic modulo n. We would like to do this by mapping to two's complement 32-bit integers. So let's use the following mapping: the modulo-n integer k (0

It's probably easier to see why it works if we choose a smaller radix, e.g. 3. In this case we have



-4 100

-3 101

-2 110

-1 111

0 000

1 001

2 010

3 011




Consider the simplest case of modulo-2^3 arithmetic where we map 0 onto -4 = 100, 1 onto -3 = 101, and so on. To verify that the isomorphism works out in this case, we simply have to verify that two's complement arithmetic "wraps around" in the natural way. I think this is proved in pretty much all books that discuss two's complement arithmetic; this is essentially the property that makes "temporary overflow" not screw everything up in two's complement arithmetic.

Note that for addition and subtraction it is not a problem that our modulo-2^3 zero does not get mapped onto the two's complement zero. We can just account for this by offsetting appropriately when converting to and from the representation.

You can see that it works in the general case of modulo-n arithmetic by appealing to the simple case above.

I'd be interested if the original poster could elaborate on how this works out for multiplication!

"Note that for addition and subtraction it is not a problem that our modulo-2^3 zero does not get mapped onto the two's complement zero. We can just account for this by offsetting appropriately when converting to and from the representation."


This is wrong and in fact the mapping I describe does not work as advertised. Instead you want to associate a modulo-n integer k with k * (2^3 / n) calculated in UNSIGNED arithmetic, then treat the resulting bit pattern as a two's complement SIGNED integer and do all further calculations with two's complement arithmetic. Converting back is just a matter of inverting that formula.

Could you elaborate about ONE? I am not sure I understood the idea.

NORTH = 0x00000000
EAST  = 0x40000000
SOUTH = 0x80000000
WEST  = 0xC0000000
TURN_RIGHT = EAST   //  This is like  1.
TURN_LEFT  = WEST   //  This is like -1.
NO_TURN    = NORTH  //  This is like  0.

You could generalize this to any power-of-2-sized set of "numbers", and call them ONE, TWO, etc. And ZERO is always just regular integer 0.

I hope this also answers the question of how you multiply... one of the numbers needs to be a normal integer. Sounds a little messy, but works pretty well in practice, if you're stuck in C. But how nice if I had a language which would do this for me (or at least let me define such a thing nicely), and not just for powers of 2.

Incidentally, I do *not* see this as a subtype of the integers, because it's a different form of arithmetic: arithmetic mod some n. (But in the same light, I don't see how the naturals would be a subtype, since it's not closed under subtraction.)

The dependent type thing is interesting, though it seems less about "type" and more about "compiler optimization".

There's a paper by Oleg Kiselyov and Chung-chieh Shan about expressing configuration parameters via the type system. One of their examples is modular arithmetic. They use the type of a number to encode its modulus and then make every such type an instance of Num.