type-int- Type Level 2s- and 16s- Complement Integers

Portabilitynon-portable (MPTC, FD, TH, undecidable instances, and missing constructors)
MaintainerEdward Kmett <ekmett@gmail.com>



Simple type-level binary numbers, positive and negative with infinite precision. This forms a nice commutative ring with multiplicative identity like we would expect from a representation for Z.

The numbers are represented as a Boolean Ring over a countable set of variables, in which for every element in the set there exists an n in N and a b in {T,F} such that forall n' >= n in N, x_i = b.

For uniqueness we always choose the least such n when representing numbers this allows us to run most computations backwards. When we can't, and such a fundep would be implied, we obtain it by combining semi-operations that together yield the appropriate class fundep list.

The goal here was to pull together many of the good ideas I've seen from various sources, and sprinkle a two's complement negative number representation on top.

Reuses T and F from the Type.Boolean as the infinite tail of the 2s complement binary number. I'm particularly fond of the symmetry exhibited in the full adder.

TODO: TDivMod, TImplies, TGCD, TBit, TComplementBit, TSetBit