1 Jan 01:51 2009

### 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
```
1 Jan 02:16 2009

### 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.
```
1 Jan 02:39 2009

### 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.
```
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

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

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

1 Jan 04:50 2009

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

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

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

> 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
```
1 Jan 05:15 2009

### 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
>
```
1 Jan 05:16 2009

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

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

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

service. I've packaged up the reCAPTCHA code as a separate library on

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

### 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
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 #-}
>
>
> > 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.

```_______________________________________________