Unlawful Num instance

[Bodigrim]

README.md says that

There exist many Haskell libraries to handle bit-vectors, but to the best of my knowledge bv is the only one that adequately supports bit-vector arithmetic.

but I struggle to grasp what kind of arithmetic it is. It seems that neither (+) nor (*) are associative:

> -1 + (1 + (-2)) :: BV
[3]2
> (-1 + 1) + (-2) :: BV
[3]6

> 21 * (4 * 14) :: BV
[6]56
> (21 * 4) * 14 :: BV
[6]24

[IagoAbal]

Hi,

If this doesn't work as expected let me know...
bitVec 3 (-1) + (bitVec 3 1 + bitVec 3 (-2))

The docs say that bit-vectors are in most cases interpreted as unsigned integers, and that's why I simply zero-extended. If you want to perform signed arithmetic, then you need to make sure that you operate bit-vectors of the same size. Size "polymorphism" assumes unsigned arithmetic.

At the time I implemented Num and other classes merely for syntactic convenience. But I agree that it's a pity that Num BV doesn't satisfy the laws it's supposed to. As I noticed when discussing #4, I'm starting to think that the library should perform sign-extension rather than zero-extension in several places...

I want to revisit this decision but it will be a "major" change in the library and it will break backwards compatibility, so I want to think how much this would affect existing users. I'm not even sure whether that would be enough or whether there will still be some unsatisfied laws. Ultimately one could use sized-types... but then I guess that part of the design space is already covered by bv-sized.

If this is a big issue for you and you are willing to help that would be very appreciated. I have little spare time nowadays.

[IagoAbal]

Hi again,

Sorry I didn't reply to the associativity of multiplication example, although the justification is kind of the same.

I assume you know that your examples behave like that because fromInteger doesn't know what size of bit-vectors do you need, so it takes the minimum required. Then, when + or * find that their operands have different sizes, they just zero-extend the smaller one and perform the operation. This of course isn't associative.

So, more generally, if you want arithmetic laws to apply then the library requires you to be explicit about the sizes of bit-vectors in most cases. The automatic zero-extension feaure is there for convenience (at least I thought it was convenient like for bit-masks...). At the time I thought it was a better idea than making virtually all the functions partial and raise run-time errors.

Unfortunately I cannot fix associativity of multiplication. Perhaps I should consider deprecating the Num instance. Or make some operations raise errors rather than zero-extend. In any case I should clarify the docs.

Let me know if you have suggestions to improve the library (that can be implemented without sized-types).

[Bodigrim]

I am not an active user of bv, just a passer-by; my interest is purely theoretical.

IMHO the best solution is to check that both arguments of (+) and (*) have the same size and throw an error otherwise, and clarify claims in README.md. Current implementation does not really make much sense when sizes mismatch.

I can possibly prepare a PR, if you'd have time to review and merge it.

[IagoAbal]

OK, I will just think on this. Allowing operations between bit-vectors of different sizes is convenient. I am aware that this breaks arithmetic laws, although I'm not sure whether I should sacrifice that convenience for the sake of theoretical correctness.

I would even argue that in 21 * (4 * 14) :: BV the first * is not the same as the second *, so associativity does not even apply.

Sign-extending would fix some of these cases (but not all). Perhaps I could just offer a flag to turn this off the same way that you can turn off bounds checks. In any case I should probably clarify the docs.

Thanks for the feedback!

[Bodigrim]

I cannot really agree that non-associativity is just a question of theoretical correctness. It means that users have to keep it in mind all the time, when using sum, product, foldMap and other members of Foldable.

Back to my original question, it would be still nice to clarify in README what kind of "bit-vector arithmetic" this is. There are, obviously, infinite possibilities and the implemented arithmetic was neither of my initial guesses (for instance, I expected some sort of polynomials modulo 2 - this is what I use in bitvec library).

[IagoAbal]

If you look at the QuickCheck properties it should be clear that the intended arithmetic is that of bit-vectors of size n. If you sum, product, etc bit-vectors of the same size n then you can be sure arithmetic laws hold. Not everything can be made type-safe (or is practical to do type-safe).

"Automagic" zero-extension to resolve size mismatching was supposed to be a mere convenience that, back in 2012-ish, I judged better than just making everything a partial function. If I remember correctly, at the time there were no sized types in Haskell.

Not sure whether to change the code or how exactly but, sure, I should definitely clarify it in the README.