[Haskell-beginners] Further constraining types

[Christopher Howard]

On 08/03/2011 09:23 PM, Brandon Allbery wrote:
> On Thu, Aug 4, 2011 at 01:03, Christopher Howard
> <christopher.howard at frigidcode.com
> <mailto:christopher.howard at 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 at gmail.com <mailto:allbery.b at 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