Bit operation typeclasses

Stream: Is there code for X?

[Wrenna Robson]

I am trying to describe in general the following behaviour for some type α:

• I have instances AndOp α and XorOp α.
• There exists some 0 such that x &&& 0 = 0 and x ^^^ 0 = x.
• There exists some 1 such that x &&& 1 = x.
• x ^^^ (x ^^^ y) = y and y ^^^ (x ^^^ y) = x.
• This means that given some b : Bool, and x y : α, I can map b to either 0 or 1 (in the obvious way), call that b' and then I have that x ^^^ ((x ^^^ y) &&& b)' = bif b then y else x and y ^^^ ((x ^^^ y) &&& b) = bif b then x else y`.

[Wrenna Robson]

The context for this is that we think of the map from b to b' as "bit extension`, and assuming we can do that in context time, this essentially describes a type on which we can do "branchless swaps".

[Wrenna Robson]

Possibly this bit extension map should also be part of the type!

[Aaron Liu]

Wrenna Robson said:

• This means that given some b : Bool, and x y : α, I can map b to either 0 or 1 (in the obvious way), call that b' and then I have that x ^^^ ((x ^^^ y) &&& b' = bif b then y else x and y ^^^ ((x ^^^ y) &&& b' = bif b then x else y.

you seem to have some mismatched parens

[Wrenna Robson]

Think that's fixed it