Dominic Steinitz wrote:
My motivation in using this type was to see if, for example, I could restrict addition of a vector to another vector to vectors of the same length. This would be helpful in the crypto library where I end up having to either define new length Words all the time or using lists and losing the capability of ensuring I am manipulating lists of the same length.
Perhaps you might find the following http://pobox.com/~oleg/ftp/Haskell/number-parameterized-types.html relevant to your task. The page demonstrates bitvectors of a statically-checked width. An attempt to AND or OR two bitvectors of different widths results in a type error. The width can be specified in _decimal_ rather than in binary, which makes types smaller and far easier to read. Type error messages also become more comprehensible. To implement just the width-checking, we need only Haskell 98. Incidentally, the approach can be easily extended to arbitrary bases, e.g., base64. Therefore, we can define numerals over a field Z^{*}_p whose modulus p is statically known and statically checked. It would be a type error to add or multiply two numerals with different moduli. With base64-bigits, we need only 86 bigits for a 512-bit modulus. Eighty-six terms make a type expression a bit long, but still manageable; whereas binary types such as Zero and One would make the approach unfeasible.