Typing differences for decimal and other literals is unintuitive

[bboston7]

Hey, this is my first bit of feedback on Cryptol and the Cryptol book as I've been working through it. Expect more tickets to stream in over the next week or two. I'm not necessarily suggesting these things should change, just pointing out little snags I came across.

It is unintuitive that decimal literals have type Integer while hex literals are of a fixed width numeric type based on the smallest number of bits they could fit into. This also applies to octal and binary literals.

This breaks an assumption I have that for all numerals n1, n2, and bases b1, b2, if n1 is a representation of a number x in base b1, and n2 is a representation of x in base b2, then n1 == n2.

This is not itself terribly strange, but it leads to some confusing situations. For example, 16 : [16] is legal, but 0x10 : [16] is not. In order to get a hexidecimal representation of 16 stored as a 16-bit number, I must instead write 0x0010. Most other languages would implicitly pad out 0x10 to 0x0010.

[weaversa]

There is a shortcut (not that it gets at your bigger issue).

Try `0x10 : [16]

[yav]

Yeah, literals are quite tricky. This might not be terribly well explained in the book, and we should probably correct it, but your statement about the types of the literals is not quite accurate. In particular, the rule is:

• Decimal lietrals are overloaded, which means they can be used at any type that supports literlas,
• Binary, octal, and hex literals are not: they have a fixed types.

So decimal literals are not restricted to Integer, you can write 10 : [8] for example.

Also the type of the other literals is determined by the number of digits in them, not the least number of bits you'd need to represent them. So 0x0001 is always a 16-bit value, even though one could represent it it just a single bit.

[brianhuffman]

People have been arguing about this design for a long time (see #30).

Another related awkwardness about our fixed-size typing rule for hex/octal/binary literals is that Cryptol's pretty printer doesn't respect it: For example, 21:[5] prints out as 0x15, but 0x15:[5] is a type error (see #179 (comment)).

On the other hand, sometimes you do want your literals to have a fixed size, and it's nice not to have to put type annotations on them. At one point I suggested that we could adopt verilog's syntax for literals, which include an optional explicit bit-width, but nobody else seemed to be enthusiastic about the idea.

[robdockins]

I wonder if we could thread this needle with a notion of "preferred defaulting" for literals. The idea is, all literals are polymorphic (like decimal literals are now); if the type is forced by context, we just unify and try to solve the corresponding Literal constraint. However, if the result type of the literal is unconstrained, we default (without warning!) to the preferred type. For decimal literals, this is Integer, for hex, decimal and binary literals, this is the explicit number of bits written.

[weaversa]

@Launchbury Would you be willing to share your thoughts on the history of this?

[yav]

The history of this is like this:

In the beginning, all literals were overloaded. As a result people would end up writing much more polymorphic programs than they intended, which would result in the various defaulting warnings and spurious type annotations. To solve this, we decided to make literals monomorphic, and for sizes that are powers of 2 there is a the natural literal width, which is pretty standard when you work with bits (e.g, 0x01 is a byte). This made things simpler, and didn't really loose any generality, as for the rare cases where you want to use binary or hex literals at non-standard types you can write a manual coercion, or use the type demotion trick that @weaversa mentioned above. This was considered to be a good thing, as it made it obvious that something unusual is happening in the code at this point.

Decimal literals, OTOH, remained overloaded because there was no natural type for them to use. This was in the pre Integer times, maybe it makes sense to make decimal literals always be Integer, although I am not sure that this would be convenient.