3 ms·

You mention integer ranges as a specific type you hope gets handled. But how does something like that work? It feels somewhere between the general type and the

You mention integer ranges as a specific type you hope gets handled. But how does something like that work? It feels somewhere between the general type and the specialization type? Would this just be a higher level in the integer section of the specialization lattice? Or would you want it out of the lattice structure completely? Because it would kinda conflict with integer unions, when thinking about it lattice-y (Admittedly I'm in the same boat, I don't know the math but stumbled upon implementing my own type system recently)

sparkie 2y ago
Every _BitInt(N) is a subtype of _BitInt(N+1). For practical purposes though, you'd usually make each intN a subtype of intN*2, up to some top integer type which supports arbitrary precision. int8 <= int16 <= int32 <= int64 <= bigint For this mini subtype hierarchy, you can literally just number the types in increasing order, and use `<=`, rather than bitmasks. For inclusion of unsigned integers, the same rule applies, but each `unsigned _BitInt(N)` is also a subtype of `signed _BitInt(N+1)`. It might make sense to number the unsigned integers one higher than their signed variants of the same width to simplify testing for compatibility. A specific bit, such as 1000b could indicate a signed integer. UNSIGNED = 0000b; SIGNED = 1000b; enum IntType { UINT8 = UNSIGNED | 1, UINT16 = UNSIGNED | 2, UINT32 = UNSIGNED | 3, UINT64 = UNSIGNED | 4, UBIGINT = UNSIGNED | 7, INT8 = SIGNED | 0, INT16 = SIGNED | 1, INT32 = SIGNED | 2, INT64 = SIGNED | 3, BIGINT = SIGNED | 7, }; is_uint8_subtype(ty) = (ty | UNSIGNED) <= UINT8 is_uint16_subtype(ty) = (ty | UNSIGNED) <= UINT16 is_uint32_subtype(ty) = (ty | UNSIGNED) <= UINT32 is_uint64_subtype(ty) = (ty | UNSIGNED) <= UINT64 is_natural(ty) = (ty | UNSIGNED) <= UBIGINT is_int8_subtype(ty) = (ty | SIGNED) <= INT8 is_int16_subtype(ty) = (ty | SIGNED) <= INT16 is_int32_subtype(ty) = (ty | SIGNED) <= INT32 is_int64_subtype(ty) = (ty | SIGNED) <= INT64 is_integer(ty) = (ty | SIGNED) <= BIGINT This is approximately how I handle it the numerical tower in my interpreter (extended with some ad-hoc rules to also support rationals, real, complex and quaternions).
- cobertos 2y ago
  Interesting, I wasn't thinking of sized integers when thinking of int ranges (moreso of Python ranges like `3..7` for integers `3 | 4 | 5 | 6 | 7`) but this is fascinating as well. The interplay between different types of ranges feels like it might be complex to model. I wonder if a type system exists that can modify the type lattice at run-time or just before run-time, so user-defined types can be added to a system even if the program is already built. As the types usually require explicit language support but I can always foresee more explicit un-typable things that might be useful just not useful enough to put in a general type system
tekknolagi 2y ago
Probably a different thing entirely than the specialization. A new lattice. A pair of uint64 for int ranges that has its own join function, maybe. CF Bolz-Tereick has a good blog post about this for pypy and it also talks about known bits
- cobertos 2y ago
  Ah! So like lower and upper bound that join separately to include the total min and total max between the two ranges types. I see

sparkie 2y ago

Every _BitInt(N) is a subtype of _BitInt(N+1). For practical purposes though, you'd usually make each intN a subtype of intN*2, up to some top integer type which supports arbitrary precision. int8 <= int16 <= int32 <= int64 <= bigint For this mini subtype hierarchy, you can literally just number the types in increasing order, and use `<=`, rather than bitmasks. For inclusion of unsigned integers, the same rule applies, but each `unsigned _BitInt(N)` is also a subtype of `signed _BitInt(N+1)`. It might make sense to number the unsigned integers one higher than their signed variants of the same width to simplify testing for compatibility. A specific bit, such as 1000b could indicate a signed integer. UNSIGNED = 0000b; SIGNED = 1000b; enum IntType { UINT8 = UNSIGNED | 1, UINT16 = UNSIGNED | 2, UINT32 = UNSIGNED | 3, UINT64 = UNSIGNED | 4, UBIGINT = UNSIGNED | 7, INT8 = SIGNED | 0, INT16 = SIGNED | 1, INT32 = SIGNED | 2, INT64 = SIGNED | 3, BIGINT = SIGNED | 7, }; is_uint8_subtype(ty) = (ty | UNSIGNED) <= UINT8 is_uint16_subtype(ty) = (ty | UNSIGNED) <= UINT16 is_uint32_subtype(ty) = (ty | UNSIGNED) <= UINT32 is_uint64_subtype(ty) = (ty | UNSIGNED) <= UINT64 is_natural(ty) = (ty | UNSIGNED) <= UBIGINT is_int8_subtype(ty) = (ty | SIGNED) <= INT8 is_int16_subtype(ty) = (ty | SIGNED) <= INT16 is_int32_subtype(ty) = (ty | SIGNED) <= INT32 is_int64_subtype(ty) = (ty | SIGNED) <= INT64 is_integer(ty) = (ty | SIGNED) <= BIGINT This is approximately how I handle it the numerical tower in my interpreter (extended with some ad-hoc rules to also support rationals, real, complex and quaternions).

cobertos 2y ago
Interesting, I wasn't thinking of sized integers when thinking of int ranges (moreso of Python ranges like `3..7` for integers `3 | 4 | 5 | 6 | 7`) but this is fascinating as well. The interplay between different types of ranges feels like it might be complex to model. I wonder if a type system exists that can modify the type lattice at run-time or just before run-time, so user-defined types can be added to a system even if the program is already built. As the types usually require explicit language support but I can always foresee more explicit un-typable things that might be useful just not useful enough to put in a general type system

tekknolagi 2y ago

Probably a different thing entirely than the specialization. A new lattice. A pair of uint64 for int ranges that has its own join function, maybe. CF Bolz-Tereick has a good blog post about this for pypy and it also talks about known bits

cobertos 2y ago
Ah! So like lower and upper bound that join separately to include the total min and total max between the two ranges types. I see