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: [Haskell-cafe] bottom case in proof by induction
([email protected])
2. Re: until and Time (Daniel Fischer)
3. Re: [Haskell-cafe] bottom case in proof by induction
(Daniel Fischer)
4. definition of data (Max.cs)
5. Re: [Haskell-cafe] definition of data (Brandon S. Allbery KF8NH)
----------------------------------------------------------------------
Message: 1
Date: Thu, 1 Jan 2009 03:50:28 -0000
From: <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] bottom case in proof
by induction
To: "Luke Palmer" <[email protected]>, <[email protected]>,
<[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
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 ; [email protected]
Subject: Re: [Haskell-cafe] bottom case in proof by induction
On Wed, Dec 31, 2008 at 3:28 PM, Max.cs <[email protected]> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20090101/51738186/attachment-0001.htm
------------------------------
Message: 2
Date: Thu, 1 Jan 2009 04:54:44 +0100
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] until and Time
To: "Steve Klabnik" <[email protected]>, [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
Am Donnerstag, 1. Januar 2009 04:18 schrieb Steve Klabnik:
> Hello everyone. I have a quick question about Time.
>
> I was talking about Haskell on the Arch Linux forums today, and someone was
> trying to put together code that would print a series of periods for, say,
> 5 minutes. I felt like using 'until' would be the most correct way of going
> about it, but when I tried to do it...
>
>
> import Time
>
> makeLater :: ClockTime -> ClockTime
> makeLater t = addToClockTime (TimeDiff 0 0 0 0 0 5 0) t
>
> updateTime :: ClockTime -> ClockTime
> updateTime t = t
>
> main = do
> start <- getClockTime
> until ((==) $ makeLater start) (updateTime) start
> putStrLn "done"
>
> Now, updateTime isn't correct. And this wouldn't print any periods. But GHC
> is giving me errors:
>
> $ runhaskell temp.hs
>
> temp.hs:11:2:
> Couldn't match expected type `IO t'
> against inferred type `ClockTime'
> In the expression:
> until ((==) $ makeLater start) (updateTime) start
> In a 'do' expression:
> until ((==) $ makeLater start) (updateTime) start
> In the expression:
> do start <- getClockTime
> until ((==) $ makeLater start) (updateTime) start
> putStrLn "done"
>
> I'm not sure where IO t is coming from at all. Am I even on the right
> track? How would you write this code?
Since it appears as a statement in the main do-block, ghc expects "until ..."
to have type IO t. But as
Prelude> :t until
until :: (a -> Bool) -> (a -> a) -> a -> a
until ((==) $ makeLater start) (updateTime) start
actually has type ClockTime, so can't appear as a statement in a do-block,
that's what ghc tells you.
Since you want a timeout, which involves IO, you must do something in IO.
You can define a general control structure (I'm sure that is already defined
somewhere, but I can't be bothered to hoogle it now)
untilM :: (Monad m) => (a -> m Bool) -> (a -> m a) -> a -> m a
untilM test action value = do
stop <- test value
if stop then return value
else do
newval <- action value
untilM test action newval
and then
isLaterThan :: ClockTime -> IO Bool
isLaterThan end = do
now <- getClockTime
return (end < now)
main = do
start <- getClockTime
let end = addToClockTime (TimeDiff 0 0 0 0 0 5 0) start
untilM (\_ -> isLaterThan end) (\_ -> putChar '.') ()
putStr "\n"
------------------------------
Message: 3
Date: Thu, 1 Jan 2009 05:15:01 +0100
From: Daniel Fischer <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] bottom case in proof
by induction
To: <[email protected]>, "Luke Palmer" <[email protected]>,
<[email protected]>, <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset="iso-8859-1"
Am Donnerstag, 1. Januar 2009 04:50 schrieb [email protected]:
> 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
>
------------------------------
Message: 4
Date: Thu, 1 Jan 2009 07:32:13 -0000
From: "Max.cs" <[email protected]>
Subject: [Haskell-beginners] definition of data
To: <[email protected]>, <[email protected]>
Message-ID: <72bd3446ddca468bb5237c62ea7b7...@hxzhao>
Content-Type: text/plain; charset="gb2312"
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
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20090101/11fad6a9/attachment-0001.htm
------------------------------
Message: 5
Date: Thu, 1 Jan 2009 02:35:55 -0500
From: "Brandon S. Allbery KF8NH" <[email protected]>
Subject: [Haskell-beginners] Re: [Haskell-cafe] definition of data
To: "Max.cs" <[email protected]>
Cc: [email protected], [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset="us-ascii"
On 2009 Jan 1, at 2:32, Max.cs wrote:
> data Tree a = a | Branch (Tree a) (Tree a) deriving Show
>
> but it seems not accpetable in haskell ?
You need a constructor in both legs of the type:
> data Tree a = Leaf a | Branch (Tree a) (Tree a) deriving Show
--
brandon s. allbery [solaris,freebsd,perl,pugs,haskell] [email protected]
system administrator [openafs,heimdal,too many hats] [email protected]
electrical and computer engineering, carnegie mellon university KF8NH
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://www.haskell.org/pipermail/beginners/attachments/20090101/8ddd680d/attachment.htm
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 7, Issue 1
***************************************
