Re: [Haskell-beginners] Further constraining types

5 Aug 2011

      On 08/04/2011 12:03 AM, David Virebayre wrote:
...
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.
But users are not the only source of ints. For example, let's say I 
wanted to do my own square function, with a type like so:

square :: Int -> Positive Int

So, I use the special constructor function in the implementation:

square x = validatePositive $ x * x

Great! now I have a function that returns Positive Ints, which can be 
fed into any function that takes a Positive Int as its parameter.

Problem, though... how do I implement this special constructor in a way 
that meets the criteria for completeness that I outlined earlier? A 
validation function, by definition, allows for the possibility of 
invalidation. So the type would have to be:

validatePositive :: Int -> Maybe (Positive Int)

But this means the type of square would have to be changed to

square :: Int -> Maybe (Positive Int)

...which is unacceptable. (I /know/ square /will/ always return an 
positive integer, not that it /might/ do so!)

I could of course throw a "maybe"-style forced cast into the square 
function, but that would defeat one of the fundamental principles of 
what I'm trying to accomplish here.

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.

-- 
frigidcode.com
theologia.indicium.us