January 2009 - Haskell-Cafe

definition of data
by Max.cs 01 Jan '09

01 Jan '09

hi all, I want to define a data type Tree a that can either be a or Branch (Tree a) (Tree a)? I tried data Tree a = a | Branch (Tree a) (Tree a) deriving Show but it seems not accpetable in haskell ? any way I could achieve this ? Thanks max

6 6

ANN: gitit-0.4.1, recaptcha-0.1
by John MacFarlane 31 Dec '08

31 Dec '08

I'm pleased to announce the release of gitit-0.4.1, which I've just uploaded to HackageDB. Gitit is a wiki program that stores pages in a git repostory. Gitit now has support for (optional) captchas, using the reCAPTCHA service. I've packaged up the reCAPTCHA code as a separate library on HackageDB, recaptcha. Upgrading from older versions of gitit: The format of gitit's user database has changed. (gitit now generates a new random salt for each user, instead of using a single static salt for all users.) Unfortunately, this means that current users of gitit (yes, all seven of you) will have to delete your gitit-users file and have your users create new accounts. Sorry about the breaking change, but better now than later. When you upgrade, you'll also need to delete the _local directory, since changes have been made to the data structure that holds the application state. This shouldn't have any ill effects, since everything of lasting importance (users, pages) is stored elsewhere. If you use a configuration file, or if you want to start using reCAPTCHA (which requires a configuration file), you will also have to add fields for the captcha system. See data/SampleConfig.hs for the format. John

1 0

Re: [Haskell-cafe] bottom case in proof by induction
by raeck＠msn.com 31 Dec '08

31 Dec '08

I am afraid I am still confused. > foo [] = ... > foo (x:xs) = ... > There is an implied: > foo _|_ = _|_ > The right side cannot be anything but _|_. If it could, then that would imply we could solve the halting problem: in a proof, how I could say the right side must be _|_ without defining foo _|_ = _|_ ? and in the case of > bad () = _|_ > bad _|_ = () mean not every function with a _|_ input will issue a _|_ output, so we have to say what result will be issued by a _|_ input in the definitions of the functions if we want to prove the equvalence between them? However, in the case of map f _|_ , I do believe the result will be _|_ since it can not be anything else, but how I could prove this? any clue? ps, the definition of map does not mention anything about _|_ . Thanks Raeck From: Luke Palmer Sent: Wednesday, December 31, 2008 10:43 PM To: Max.cs ; raeck(a)msn.com Subject: Re: [Haskell-cafe] bottom case in proof by induction On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <max.cs.2009(a)googlemail.com> wrote: thanks Luke, so you mean the _|_ is necessary only when I have defined the pattern _|_ such as foo [] = [] foo _|_ = _|_ foo (x:xs) = x( foo xs ) -- consider non-termination case That is illegal Haskell. But another way of putting that is that whenever you do any pattern matching, eg.: foo [] = ... foo (x:xs) = ... There is an implied: foo _|_ = _|_ The right side cannot be anything but _|_. If it could, then that would imply we could solve the halting problem: halts () = True halts _|_ = False Because _|_ is the denotation of a program which never halts. To do it a bit more domain-theoretically, I'll first cite the result that every function has a fixed point. That is, for every f, there is a function fix f, where fix f = f (fix f). (The fix function is actually available in Haskell from the module Data.Function). Then let's consider this bad function: bad () = _|_ -- you can't write _|_ in Haskell, but "undefined" or "let x = x in x" mean the same thing bad _|_ = () Then what is fix f? Well, it either terminates or it doesn't, right? I.e. fix f = () or fix f = _|_. Taking into account that fix f = f (fix f): If it does: fix f = () = f () = _|_, a contradiction. If it doesn't: fix f = _|_ = f _|_ = (), another contradiction. >From a mathematical perspective, that's why you can't pattern match on _|_. >From an operational perspective, it's just that _|_ means "never terminates", and we can't determine that, because we would try to run it "until it doesn't terminate", which is meaningless... Luke

4 3

bottom case in proof by induction
by raeck＠msn.com 31 Dec '08

31 Dec '08

Dear all, Happy New Year! I am learning the Induction Proof over Haskell, I saw some proofs for the equivalence of two functions will have a case called 'bottom' but some of them do no have. What kind of situation we should also include the bottom case to the proof? How about the functions do not have the 'bottom' input such as: foo [] = [] foo (x:xs) = x : (foo xs) thank you, Raeck

4 3

ANN: monte-carlo-0.2, gsl-random-0.2.3
by Patrick Perry 31 Dec '08

31 Dec '08

I've released a new version of the monte-carlo packages for haskell. Here are the highlights for monte-carlo: Changes in 0.2: * More general type class, MonadMC, which allows all the functions to work in both MC and MCT monads. * Functions to sample from discrete distributions. * Functions to sample subsets For a quick tutorial, see my blog post at http://quantile95.com/2008/12/31/monte-carlo-poker-odds/ Happy New Year, everyone! Patrick

1 0