Negative numeric types?

[robdockins]

While working on support for enumerations with explicit strides, it occurred to me that we can't write the following:

[ -10 .. 10 ]: [_]Integer

Cryptol complains that -10 is not a numeric type. Obviously, there are other ways to achieve the intended effect, but I don't think any are as clear. It also turns out to be pretty tricky to find a way to express something like:

[-10 .. 10 by 3 ]

especially if one wants to be parametric in the stride.

One way to handle this would be to simply allow numeric types to be some version of the integers (extended with either one or two infinities depending on the properties we want) instead of the extended naturals. I don't know exactly what effects this would have, but probably it would mostly mean that the [n]a type constructor would gain a n >= 0 well-formededness condition. It would also have some impact on the questions regarding the Literal class and its downward closure.

I don't really know if this is worth doing, but I thought I'd write down my thoughts.

[yav]

I think we probably have quite a lot of places where we are assuming that the sizes are naturals, so it'd be pretty tricky to do that, I think.

I wonder, though, if we may want to rethink the part where enumerations are types. Perhaps we can revert them back to being normal values, with some rules that we should be able to determine statically the length of the sequence... It might be a bit ad-hoc, but I wonder if it would end up being more intuitive. That's kind of how it used to be on Cryptol 1, so there is a precedent...

[robdockins]

This would be a pretty big change, and this is a relatively weak motivation for it, so I think we probably won't do this.