In terms of category theory, what we would need is subtraction and division types on top of product and sum types.

So a 32-bit integer is the product of 32 two-state bit types. Something akin to NonZero could be defined as that type minus one state, such that there are now 4294967296 - 1 representable values.

Similarly, pointer types on some machines always have some bits set to 0 due to hardware constraints. These can be represented in the type system as 2^64 / 2^n where 'n' is the number of bits that are not usable, resulting in something like 2^46 for typical CPUs. This would allow extra bits of state to be "packed in there".

This concept is more generally useful, not just for bit-packing.

For example, a database table row might be represented by a struct that contains a field for every column. But then, how to represent the result of a SELECT query!? Either you code-gen this into a new type, create that type manually, or use compiler-generated "unspeakable" type names. (Linq in C# does this.)

Or... the language could natively support type division, so you could use one struct type for "all columns" and then use division on the type to delete columns you don't need for a particular query or REST response.

There's a whole ecosystem of tools that work around the problem of not having this as a built-in feature in typical languages: AutoMapper, automap, Mapster, etc...

> So a 32-bit integer is the product of 32 two-state bit types. Something akin to NonZero could be defined as that type minus one state, such that there are now 4294967296 - 1 representable values.

I can see a couple of problem with this approach:

- you need to be able to talk about bit-level types, which contradicts the common assumption that all types are addressable, i.e. whose size and alignment is some positive integer (or zero) number of bytes;

- what if you want to substract more complex set of values? For example describing a 32 bit number without all multiples of 7? And how do you encode this in the compiler in such a way that type checking remains decidable?

- how do you safely and concisely express conversions and operations on these kind of types?

> Similarly, pointer types on some machines always have some bits set to 0 due to hardware constraints. These can be represented in the type system as 2^64 / 2^n where 'n' is the number of bits that are not usable, resulting in something like 2^46 for typical CPUs. This would allow extra bits of state to be "packed in there".

Note that this is not forward compatible, since newer CPUs can start using more bits. In fact recent CPUs started using 57 bits instead of 48 bits, so a program that packed more state in those top bits would now be broken. You should generally instead try to pack data in the least significant bits that will always be 0 due to alignment constraints.

Moreover the top bits are not always 0, they are equal to the most relevant bit of the used part of the address. On Linux this just happens to always be 0 for userspace addresses (and 1 for kernel addresses) but this won't be the case on all architectures and OSes.

I also wonder how you would define these types using subtraction/division types such that they are different?

- the address type being 64 bits but using only the least significant 48 bits and having the top 16 bits always 0 - the address type being 64 bits but using only the least significant 48 bits and having the top 16 bits always equal to the 48th bit - the address type being 48 bits

Clearly these types are all isomorphic, but they are definitionally different and in a way that really matters to the hardware.

My thinking was that this would be up to the compiler, where you’d have to specify the target CPU model for it to take advantage of the feature. Similarly, byte code VM could use this with runtime detection of the CPU properties.

This would work best in a high level language where the specific bit layout of struct types is not defined (by default). Rust is one such language, but this would also work with .NET and JVM languages.

One approach is that integers are represented as A < ( x < S + O ) < B. This would allow ranges, powers of two, “NonZero”, offsets, and the like the be represented in the lowest levels of the type system. Additionally, the high level type system could also keep an additional list of specific numbers that are excluded.

Pointer types could be internally represented as ordinary integers, or aligned non-null pointers on some architectures would be “0 < x << 3”.

This could have no effect on the emitted code, but the compiler would be free to utilise the spare low bits or the non-zero value if it chose to do so. Rust does this in a few hard-coded scenarios, but a more complete type model would allow more flexibility. I.e.: it could pack the enum discriminator and the value in there if the enum has only pointer types as values.

Conversely, the high level language can use this for type checks to give better error messages.

I'm not sure where subtraction and division types come into play then. If all of this is done internally in the compiler then this should part of the layout system/implementation, and not exposed to the user in the type system.

> where you’d have to specify the target CPU model

I would be wary of doing this unless you're sure your executable will only ever run on that CPU model.

> This would work best in a high level language where the specific bit layout of struct types is not defined (by default). Rust is one such language

Note that Rust does leak some implicit assumption about struct layouts. For example you can always get a pointer to a struct field, meaning a field can't be e.g. a single bit, it must be an non-negative amount of bytes (so for example the 32-bit number as product type of 32 1-bit numbers would not work if you use a struct as the product type).

> or aligned non-null pointers on some architectures would be “0 < x << 3”.

I wonder which architecture requires all pointers to have an alignment of 8.

> I wonder which architecture requires all pointers to have an alignment of 8.

Many bytecode VMs in 64-bit mode do this by default! They may not be forced to align pointers by the CPU hardware, but they do it anyway for various reasons. Many (non-x86) CPUs require aligned pointers to either 32- or 64-bit boundaries.

> so a program that packed more state in those top bits would now be broken

You can use pointer masking to avoid this issue - basically you tell the hardware to ignore the top N bits, even if they are part of the virtual address. RISC-V supports this for 7 and 16 top bits. I assume ARM has a similar feature.

Note that x86-64 has no such feature, and requires pointers to be in the canonical form I explained in my previous comment (sorry however for being overly x86-centric in that comment).

Moreover even on ARM/RISC-V the primary reason this feature was added was to use memory tagging to track allocations and detect out-of-bound-access/use-after-free bugs. Exposing those top bits for other usecases will make your language incompatible with that detection mechanism (possibly triggering false-positives in it)

> basically you tell the hardware to ignore the top N bits, even if they are part of the virtual address

You can ignore the top N bits even manually by masking the pointer. The issue arises if you ever get a pointer whose top N bits actually matter (i.e. if masking them off produces a pointer to a different address). If you don't have the guarantee that this will never happen then your pointer masking it wrong.

I think all your points are answered by the background section of the RISC-V pointer masking extension spec:

> Doing this without hardware support introduces significant overheads since the pointer tag needs to be manually removed for every conventional memory operation. Pointer masking support reduces these overheads.

> It is worth mentioning that while HWASAN is the primary use-case for the current pointer masking extension, a number of other hardware/software features may be implemented leveraging Pointer Masking. Some of these use cases include sandboxing, object type checks and garbage collection bits in runtime systems.

Ada has constrained range types. Idris has lots more fun stuff with types. But not very mainstream yet.

As far as I understand it there's no need for that. You don't need to say [0, 256) except 0; you can just say [1, 256).

With subtraction, you can say [0, 256) except [4, 9, 15, 26]. You can do that just by narrowing a single range.

But then, its kinda hard to optimise such a split range in the general case. The narrowing option gives you 80% (maybe more) of the performance at 20% (probably even less) of the cost.