On 08/05/2011 06:00 AM, Brent Yorgey wrote:
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.
I'll read through the link this weekend.
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
Are you saying that is how I would do it Agda, or is there a way to do that in Haskell? More detail would be great. -- frigidcode.com theologia.indicium.us