[Haskell-beginners] Further constraining types

[Christopher Howard]

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