3 ms·

> because a is only big when b is small or some property like that Exactly, the expressiveness of the type system then (typically) becomes the obstacle: How do

> because a is only big when b is small or some property like that Exactly, the expressiveness of the type system then (typically) becomes the obstacle: How do you express that a and b could each reach INT_MAX but their sum never exceeds INT_MAX?

Arch-TK 4y ago
Those kinds of assumptions are where you explicitly cast to a smaller ranged type with the option of an error if the sum does exceed a limit. The point of this type system is not to be able to fully encode every possible interaction between numbers in a system, but rather to remove unnecessary bounds checking in a bunch of cases and make it explicit in the few cases where you ARE actually making an assumption.
- codethief 4y ago
  > Those kinds of assumptions are where you explicitly cast to a smaller ranged type But how exactly do you do that? As mentioned, a and b individually can still reach INT_MAX. I agree with your overall assessment, though. If a type system could represent (and recognize, and evaluate / automatically draw conclusions from) any possible restriction on the values of variables this would probably amount to the type system being able to carry out arbitrary mathematical proofs. The existence of such a type system seems rather unlikely.
  - Arch-TK 4y ago
    In some pretend rust. Pretend Integer exists and has the properties I described: fn special_sum(a: Integer<0..(1<<32)>, b: Integer<0..(1<<32)>) -> Option<Integer<0..(1<<32)>> { Integer<0..(1<<32)>::try_from(a + b) } The type of the expression a+b would be Integer<0..(1<<33)-1>. Obviously you can design a language which makes this much more ergonomic. That language can also avoid needing to use a type larger than a 32 bit wide unsigned integer to perform the operation through a special optimisation. Moreover, there's nothing stopping the type system from being able to maintain more sophisticated rules, for example there's nothing stopping a product type of two Integer<0..(1<<32)> having a rule applied which ensures that the sum of the two values cannot exceed 2*32-1.

Arch-TK 4y ago

Those kinds of assumptions are where you explicitly cast to a smaller ranged type with the option of an error if the sum does exceed a limit. The point of this type system is not to be able to fully encode every possible interaction between numbers in a system, but rather to remove unnecessary bounds checking in a bunch of cases and make it explicit in the few cases where you ARE actually making an assumption.

codethief 4y ago
> Those kinds of assumptions are where you explicitly cast to a smaller ranged type But how exactly do you do that? As mentioned, a and b individually can still reach INT_MAX. I agree with your overall assessment, though. If a type system could represent (and recognize, and evaluate / automatically draw conclusions from) any possible restriction on the values of variables this would probably amount to the type system being able to carry out arbitrary mathematical proofs. The existence of such a type system seems rather unlikely.
- Arch-TK 4y ago
  In some pretend rust. Pretend Integer exists and has the properties I described: fn special_sum(a: Integer<0..(1<<32)>, b: Integer<0..(1<<32)>) -> Option<Integer<0..(1<<32)>> { Integer<0..(1<<32)>::try_from(a + b) } The type of the expression a+b would be Integer<0..(1<<33)-1>. Obviously you can design a language which makes this much more ergonomic. That language can also avoid needing to use a type larger than a 32 bit wide unsigned integer to perform the operation through a special optimisation. Moreover, there's nothing stopping the type system from being able to maintain more sophisticated rules, for example there's nothing stopping a product type of two Integer<0..(1<<32)> having a rule applied which ensures that the sum of the two values cannot exceed 2*32-1.