2011/8/4 Christopher Howard
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.