[Haskell-beginners] Further constraining types

[David Virebayre]

2011/8/4 Christopher Howard <christopher.howard at frigidcode.com>:
> On 08/03/2011 09:23 PM, Brandon Allbery wrote:

> This seems like a really significant issue for a functional programming
> language. Am I eventually going to have to switch to Agda? My friends are
> trying to convert me...

I don't know Agda and what dependent type guarantee, but I don't see
how they would prevent a user typing '-123' where you expect a
positive number, so one way or another you will have to deal with
input at runtime.

Once you've validated your user input though, nothing prevents you to
have it return a Positive Int that you will guarantee can hold only
positive integers, for example by using a smart constructor, and
hiding the contructor in a separate module. You don't need dependant
types for this.

David.