An Integer That Only Decreases?
Published on November 8, 2020
Debuggery
Some fields hidden!
- visibility: ['public']
- author: {'uid': ['/'], 'name': ['Maxwell Joslyn'], 'note': ['I am a human bean']}
- url: ['/2020/11/08/vi', '/ideas/an-integer-that-only-decreases']
- type: ['entry']
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.