Polymorphic Recursion / Rank-2 Confusion

[oleg at pobox.com]

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.