Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Further constraining types (Brandon Allbery)
2. Re: Further constraining types (David Virebayre)
3. Re: Further constraining types (Arlen Cuss)
4. Re: Further constraining types (David Virebayre)
----------------------------------------------------------------------
Message: 1
Date: Fri, 5 Aug 2011 00:29:15 -0400
From: Brandon Allbery <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Christopher Howard <[email protected]>
Cc: Haskell Beginners <[email protected]>
Message-ID:
<cakfcl4w94fojn1vm-t_hjcuq-qikvnbzfyxu2y0mwys_+ez...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
On Thu, Aug 4, 2011 at 02:51, Christopher Howard <
[email protected]> wrote:
> On 08/03/2011 09:23 PM, Brandon Allbery wrote:
>
>> 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.
>>
> 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...
Agda is a wonderful FP platform, but I'm not convinced Agda is at all ready
to be an *applications* platform. So if theory is your thing, go straight
to Agda; if you want to use FP for real world problems, Haskell is (at least
for now) a better choice. (Or OCaml, but you then lose the advantages of
purity on top of not having dependent types.)
--
brandon s allbery [email protected]
wandering unix systems administrator (available) (412) 475-9364 vm/sms
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://www.haskell.org/pipermail/beginners/attachments/20110805/f87c5bbb/attachment-0001.htm>
------------------------------
Message: 2
Date: Fri, 5 Aug 2011 09:17:22 +0200
From: David Virebayre <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Christopher Howard <[email protected]>
Cc: Haskell Beginners <[email protected]>
Message-ID:
<cam_wfvvoxkk9d--bfxxhamq0ajx5fqn6fzls2m-js-40vcl...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
2011/8/5 Christopher Howard <[email protected]>:
> 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
> validatePositive :: Int -> Maybe (Positive Int)
> But this means the type of square would have to be changed to
> square :: Int -> Maybe (Positive Int)
I would go with :
validatePositive :: Int -> Maybe (Positive Int)
square :: Positive Int -> Positive Int
For the subtraction problem as shown by Thomas, you can
subtract :: Positive Int -> Positive Int -> Maybe (Positive Int)
subtract (Positive a) (Positive b)
| a >= b = Just $ Positive (a-b)
| otherwise = Nothing
But that's what you want to avoid, so maybe it's acceptable, depending
on your problem, to do:
subtract :: Positive Int -> Positive Int -> Positive Int
subtract (Positive a) (Positive b)
| a >= b = Positive (a-b)
| otherwise = Positive 0
The only other solution would be to statically guarantee that a>b,
with dependent types you could probably; but since I know next to
nothing about that, I have trouble seeing how could work with a simple
example like that: (and I would love to learn !)
1 - read two lines from stdin
2 - convert each lines to natural numbers a and b
3 - subtract b from a , a>b should be statically guaranteed
4 - print the result
David.
------------------------------
Message: 3
Date: Fri, 05 Aug 2011 17:22:09 +1000
From: Arlen Cuss <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: David Virebayre <[email protected]>
Cc: Haskell Beginners <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1
> I would go with :
> validatePositive :: Int -> Maybe (Positive Int)
> square :: Positive Int -> Positive Int
But squaring a negative Int is still guaranteed to be positive!
------------------------------
Message: 4
Date: Fri, 5 Aug 2011 09:44:48 +0200
From: David Virebayre <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Arlen Cuss <[email protected]>
Cc: Haskell Beginners <[email protected]>
Message-ID:
<CAM_wFVsjk+KRvSvEwXahgmyEtqWORWzgWaubfmPM7eZMVWyf=a...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
2011/8/5 Arlen Cuss <[email protected]>:
>> I would go with :
>> ?validatePositive :: Int -> Maybe (Positive Int)
>> ?square :: Positive Int -> Positive Int
>
> But squaring a negative Int is still guaranteed to be positive!
I thought he said he wanted to work with natural numbers.
David.
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 38, Issue 9
****************************************
