Send Beginners mailing list submissions to beginners@haskell.org 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 beginners-requ...@haskell.org
You can reach the person managing the list at beginners-ow...@haskell.org 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 <allber...@gmail.com> Subject: Re: [Haskell-beginners] Further constraining types To: Christopher Howard <christopher.how...@frigidcode.com> Cc: Haskell Beginners <beginners@haskell.org> 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 < christopher.how...@frigidcode.com> 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 allber...@gmail.com 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 <dav.vire+hask...@gmail.com> Subject: Re: [Haskell-beginners] Further constraining types To: Christopher Howard <christopher.how...@frigidcode.com> Cc: Haskell Beginners <beginners@haskell.org> Message-ID: <cam_wfvvoxkk9d--bfxxhamq0ajx5fqn6fzls2m-js-40vcl...@mail.gmail.com> Content-Type: text/plain; charset=UTF-8 2011/8/5 Christopher Howard <christopher.how...@frigidcode.com>: > 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 <cel...@sairyx.org> Subject: Re: [Haskell-beginners] Further constraining types To: David Virebayre <dav.vire+hask...@gmail.com> Cc: Haskell Beginners <beginners@haskell.org> Message-ID: <4e3b9a21.3090...@sairyx.org> 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 <dav.vire+hask...@gmail.com> Subject: Re: [Haskell-beginners] Further constraining types To: Arlen Cuss <cel...@sairyx.org> Cc: Haskell Beginners <beginners@haskell.org> Message-ID: <CAM_wFVsjk+KRvSvEwXahgmyEtqWORWzgWaubfmPM7eZMVWyf=a...@mail.gmail.com> Content-Type: text/plain; charset=UTF-8 2011/8/5 Arlen Cuss <cel...@sairyx.org>: >> 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 Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners End of Beginners Digest, Vol 38, Issue 9 ****************************************