fromInteger and arbitrarily shaped values

[weaversa]

Is this behavior of fromInteger intended?

Cryptol> fromInteger 3 : [3][3][10]
[[0x003, 0x003, 0x003], [0x003, 0x003, 0x003],
 [0x003, 0x003, 0x003]]

I can imagine one might accidentally do:

Cryptol> fromInteger 1234567890 : [4][8]         
[0xd2, 0xd2, 0xd2, 0xd2]

When they meant to do:

Cryptol> split (fromInteger 1234567890) : [4][8]
[0x49, 0x96, 0x02, 0xd2]

[yav]

I believe it is intentional, although perhaps questionable :) It happens because the type of fromInteger is:

fromInteger : Ring a => Integer -> a

so it works for any type that forms a Ring. As it happens, non-bit sequences form a Ring where they just lift the operations pointwise to their elements (e.g., to add to vectors, we add their elements pointwise), and we are just seeing the pointwise lifting of fromInteger to the sequence. So fromInteger 2 : [3][8] would be [fromInteger 2, fromInteger 2, fromInteger 2] which is [2,2,2]. When you keep doing this you get the result you observed above.

I agree that on occasion this could be confusing, however, the only solution I can think of do not see great:

• Change the type of fromInteger, but this would require us adding probably a whole new class, just for that
• Make sequences not be a ring---the pointwise lifting has been part of Cryptol for a long time though, so that might break existing code...

[weaversa]

Thanks for digging into this @yav! I agree that neither of your solutions are great. Perhaps another solution is to accept the behavior and document it -- Could the help text for :h Integer be updated to mention this behavior (similar to the help text for zero)?