An Integer That Only Decreases?
by Maxwell Joslyn. .
Is it correct to say that a type system needs to implement dependent types if it is to allow the expression of an integer that can only decrease? The goal would be to define a type R Integer
such that a function R Integer -> R Integer
would only compile if the Integer
inside the output value was equal or less to the one inside the input.