[Haskell-beginners] Further constraining types

[Brent Yorgey]

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