Patrick Perry | 1 Jan 01:51 2009
Picon

ANN: monte-carlo-0.2, gsl-random-0.2.3

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
Martijn van Steenbergen | 1 Jan 02:16 2009
Picon

Re: bottom case in proof by induction

Luke Palmer wrote:
> First, by simple definition, id _|_ = _|_.  Now let's consider foo _|_.  
> The Haskell semantics say that pattern matching on _|_ yields _|_, so 
> foo _|_ = _|_. So they are equivalent on _|_ also.  Thus foo and id are 
> exactly the same function.

Would it in general also be interesting to look at foo == id for input 
(_|_:xs) and all other possible positions and combinations of positions 
for bottom? I wonder how many cases you need to take into consideration 
to have covered every possible situation.

Martijn.
Derek Elkins | 1 Jan 02:39 2009
Picon

Re: bottom case in proof by induction

On Thu, 2009-01-01 at 02:16 +0100, Martijn van Steenbergen wrote:
> Luke Palmer wrote:
> > First, by simple definition, id _|_ = _|_.  Now let's consider foo _|_.  
> > The Haskell semantics say that pattern matching on _|_ yields _|_, so 
> > foo _|_ = _|_. So they are equivalent on _|_ also.  Thus foo and id are 
> > exactly the same function.
> 
> Would it in general also be interesting to look at foo == id for input 
> (_|_:xs) and all other possible positions and combinations of positions 
> for bottom? I wonder how many cases you need to take into consideration 
> to have covered every possible situation.

That case is already covered by the (x:xs) case.  The interesting,
potentially "extra", case is an infinite list.
S. Günther | 1 Jan 04:14 2009

Re: Updating doubly linked lists

Thanks for the answers to all.
Untying the knot was (and still is) exactly the problem I was facing.
I knew that the whole list had to be rebuild and wasn't concerned
with performance since at that point I just wanted to know how to
do it and if it is possible at all. After I realized that it maybe just to
hard in the circular case I tried my hand on a non circular version
coming up with the following.
data DList a =
  DLNode {left::(DList a), value::a, right::(DList a)} |
  Leaf

update :: DList a -> a -> DList a
update n newValue = n' where
  n' = DLNode (linkleft n n') newValue (linkright n n')

linkleft, linkright :: DList a -> DList a -> DList a
linkleft Leaf _ = Leaf
linkleft old new = l' where
  l  = left old
  l' = case l of {~Leaf -> l; _ -> l{left = linkleft l l', right = new}}

linkright Leaf _ = Leaf
linkright old new = r' where
  r  = right old
  r' = case r of {~Leaf -> r; _ -> r{right = linkright r r', left = new}}

Not the most elegant solution but relatively straightforward.
And it does what it should if the list is terminated with Leaves on
the left and
right. One can also run it on an circular list but then it just
(Continue reading)

raeck | 1 Jan 04:50 2009
Picon

Re: [Haskell-cafe] bottom case in proof by induction

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

Sent: Wednesday, December 31, 2008 10:43 PM
Subject: Re: [Haskell-cafe] bottom case in proof by induction

On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <max.cs.2009 <at> 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
_______________________________________________
Beginners mailing list
Beginners <at> haskell.org
http://www.haskell.org/mailman/listinfo/beginners
Jonathan Cast | 1 Jan 05:08 2009

Re: bottom case in proof by induction

On Thu, 2009-01-01 at 03:50 +0000, raeck <at> msn.com wrote:
> 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 _|_ = _|_ ?

This definition is taken care of for you by the definition of Haskell
pattern matching.  If the first equation for a function has a pattern
other than

  * a variable or
  * a lazy pattern (~p)

for a given argument, then supplying _|_ for that argument /must/ (if
the application is total) return _|_.  By rule.  (We say the pattern is
strict, in this case).

>  and in the case of
>  
> > bad () = _|_   
> > bad _|_ = ()

Note that these equations (which are not in the right form for the
Haskell equations that define Hasekll functions) aren't satisfied by any
Haskell function!

> mean not every function with a _|_ input will issue a _|_ output,

True --- but we can say a couple of things:

  * For all Haskell functions f, if f _|_ is an application of a
constructor C, then f x is an application of C (to some value), for all
x.  [1]
  * For all Haskell functions f, if f _|_ is a lambda expression, then f
x is a lambda expression, for all x.

The only other possibility for f _|_ is _|_.

(Do you see why bad above is impossible?)

> 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?

You have to deduce what the value at _|_ will be.

> 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?

Appeal to the semantics of Haskell pattern matching.  If you like, you
can de-sugar the definition of map a little, to get

  map = \ f xn -> case xn of
    [] -> []
    x:xn0 -> f x : map f xn0

And then you know that

    case _|_ of
      [] -> ...
      ...
  = _|_

whatever you fill in for the ellipses.  (Do you see why this *must* be
part of the language definition?)

> ps, the definition of map does not mention anything about _|_ .

The behavior of map f _|_ is fixed by the definition of Haskell pattern
matching.

jcc
Daniel Fischer | 1 Jan 05:15 2009
Picon

Re: bottom case in proof by induction

Am Donnerstag, 1. Januar 2009 04:50 schrieb raeck <at> msn.com:
> 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

Because _|_ is matched against a refutable pattern ([], in this case), so when 
foo is called with argument _|_, the runtime tries to match it against []. 
For that, it must reduce it far enough to know its top level constructor, 
which by definition of _|_ isn't possible, so the pattern match won't 
terminate, hence foo _|_ is a nonterminating computation, i.e. _|_.

>
> > bad () = _|_
> > bad _|_ = ()

You can't do that. You can only pattern-match against patterns, which _|_ 
isn't. 

>
> 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?

If you match against an irrefutable pattern (variable, wildcard or ~pattern), 
the matching succeeds without evaluating the argument, so then you can have 
functions which return a terminating value for nonterminating arguments:

lazyMap ~(x:xs) = [[],[x],xs]

*LazyTest> lazyMap undefined
[[],[*** Exception: Prelude.undefined
*LazyTest> lazyMap []
[[],[*** Exception: PrintPer.hs:28:0-28: Irrefutable pattern failed for 
pattern (x : xs)
*LazyTest> take 1 $ lazyMap undefined
[[]]

>
> 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 _|_ .

As above, evaluation of map f _|_ tries to match _|_ against [], which doesn't 
terminate.

>
> Thanks
> Raeck
>
Derek Elkins | 1 Jan 05:16 2009
Picon

Re: bottom case in proof by induction

On Wed, 2008-12-31 at 22:08 -0600, Jonathan Cast wrote:
> On Thu, 2009-01-01 at 03:50 +0000, raeck <at> msn.com wrote:
> > 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 _|_ = _|_ ?
> 
> This definition is taken care of for you by the definition of Haskell
> pattern matching.  If the first equation for a function has a pattern
> other than
> 
>   * a variable or
>   * a lazy pattern (~p)
> 
> for a given argument, then supplying _|_ for that argument /must/ (if
> the application is total) return _|_.  By rule.  (We say the pattern is
> strict, in this case).
> 
> >  and in the case of
> >  
> > > bad () = _|_   
> > > bad _|_ = ()
> 
> Note that these equations (which are not in the right form for the
> Haskell equations that define Hasekll functions) aren't satisfied by any
> Haskell function!

This isn't just a quirk of Haskell semantics.  bad is not computable.
Period.
John MacFarlane | 1 Jan 05:46 2009
Picon

ANN: gitit-0.4.1, recaptcha-0.1

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
Paolino | 1 Jan 08:01 2009
Picon

Re: WriterT [w] IO is not lazy in reading [w]

I must ask why runWriterT k :: State s (a,[Int]) is working.
Looks like I could runIO the same way I evalState there.
In that case I wouldn't wait for the State s action to finish.

Thanks


2008/12/31 Derek Elkins <derek.a.elkins <at> gmail.com>
On Wed, 2008-12-31 at 21:48 +0100, Paolino wrote:
> As someone suggested me, I can read the logs from Writer and WriterT as computation goes by,
> if the monoid for the Writer  is lazy readable.
> This has been true until I tried to put the IO inside WriterT
>
>
> > {-# LANGUAGE FlexibleContexts #-}
> > import Control.Monad.Writer
>
>
> > k :: (MonadWriter [Int] m) => m [Int]
>
> > k = let f x = tell [x] >> f (x + 1) in f 0
>
>
> > works :: [Int]
> > works = snd $ runWriter k
>
>
> > hangs :: IO [Int]
> > hangs = snd `liftM` runWriterT k

runWriterT :: MonadWriter w m a => WriterT w m a -> m (a, w)

which is to say runWriterT k :: IO (a, [Int])

It's not going to return anything until the IO action terminates, which is to say never.


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane