Your example is perfectly possible to implement in most languages; you just can't expect to give a function an arbitrary run-time integer value and have its validity checked at compile time :) So, the type would have to look something like this:
class IntegerPowerOfTwo {
private int exponent;
public IntegerPowerOfTwo(int exponent) {
this.exponent = exponent;
}
public int toInt() {
return 1 << exponent;
}
}
If you want a compile-time conversion from a constant integer to an IntegerPowerOfTwo, it is possible with C++, for instance, although you need a bit of template metaprogramming.
I'd like to know why this was downvoted. (Edit: other than the fact that the exponent should be unsigned int :/)
The whole point of encapsulation is to be able to write data types that have invariants other than those offered by the machine-level types. If you want a type T that satisfies the predicate
∀n∈T: ∃k∈N: n = 2^k
then you write a type that only provides operations that maintain the constraint. In this case, for instance, construction from k and multiplication by another T. As I said, some languages like C++ do also allow things such as compile-time conversion of an unconstrained constant integer into a power-of-two integer, with a compile error if the constraint isn't satisfied, but in my opinion that's mostly syntactic sugar. Would be nice if you could simply write, say,
type intPowerOfTwo = unsigned int where ∀intPowerOfTwo n: ∃unsigned int k: n = 2^k
but what about the unsigned int operations, such as addition, that do not maintain the invariant? Should the type system include a general theorem prover that can deduce which operations are allowed?
However, I understand this was simply an example and do agree that expressive and powerful type systems are certainly a very useful tool. C++ template metaprogramming (pretty much computing with types as values) is very impressive even if horribly ad hoc and the concepts feature (constrained templates), if ever actually implemented, will make all kinds of things easier.
I'm not sure why you're being downvoted. This technique is not entirely unlike using a phantom type, which is a common way of encoding such constraints into the type system.
I'll admit it's not ideal; in fact, it's often downright cumbersome. In some cases, it's not possible to encode desired information into a particular type system.
But in this case, it seems valid to me. There is no way to construct a value of IntegerPowerOfTwo that does not represent a power of two, and therefore it fulfills GP's example requirement.
