On Thu, Aug 04, 2011 at 06:52:03PM -0800, Christopher Howard wrote:
Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far.
I recommend reading "The Power of Pi" by Oury and Swierstra (http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf). It's a very readable introduction to dependently-typed programming with several great examples. Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like. -Brent