[Haskell-beginners] Further constraining types

[Christopher Howard]

On 08/04/2011 12:03 AM, David Virebayre wrote:
> 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.
>

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