Re: [Haskell-beginners] Further constraining types

On 08/03/2011 09:23 PM, Brandon Allbery wrote:

On Thu, Aug 4, 2011 at 01:03, Christopher Howard mailto:christopher.howard@frigidcode.com> wrote:

...to deal with the case where a negative parameter is passed in. But it seems like what I really want is something like this:

f :: Positive Int -> Int

I.e., the "positiveness" is hard-coded into the parameter type. But how do I do this? I was thinking it would involve some kind of "Positive Int" type, and some kind of "constructor" function like so:

positiveNum :: Int -> Positive Int

However, then this constructor function must deal with the problem of receiving a negative integer, and thus I have only shifted the problem. It is still an improvement, but yet it seems like I am missing some important concept here...

The concept is called "dependent types", where a type can depend on a value. Haskell doesn't support them natively, although there are some hacks for limited cases.

-- brandon s allbery allbery.b@gmail.com mailto:allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

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... -- frigidcode.com theologia.indicium.us