[Haskell-cafe] readFile problem
Hi I am writing a network server in haskell. Lately I seem to have introduced a new bug. On Linux, when a client closes the connection to the server, the server dumps core. On Windows, the error message there is way different from the core dump on Linux. It says: application.exe: config.xml: openFile: does not exist (No such file or directory) I use readFile to read the config file. I tried to print out the config file after it is read to make sure that it is completely read. I only load this config file exactly once during program initialization. The config is used long before the crash. I printed the current working dir in the exception handler and there is something interesting. Instead of the path to the application, it is \C:\\WINDOWS\\system32. There are many things i do not understand. Why the different behaviour on Linux and Windows? Shouldn't an exception be thrown on Linux instead of a core dump? I don't use any unsafePerformIO or foreign calls. Why the changed path? I never change working directory in my code. Why is a function (- reading the config file) re-evaluated at a later point in time? How can I debug such a problem? My environement is ghc 6.6 on Ubuntu or Windows XP. thanks for any ideas Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] readFile problem
On 1/8/07, Stefan Aeschbacher [EMAIL PROTECTED] wrote: There are many things i do not understand. Why the different behaviour on Linux and Windows? Shouldn't an exception be thrown on Linux instead of a core dump? I don't use any unsafePerformIO or foreign calls. Why the changed path? I never change working directory in my code. Why is a function (- reading the config file) re-evaluated at a later point in time? How can I debug such a problem? My environement is ghc 6.6 on Ubuntu or Windows XP. It may be difficult to say without seeing your code. Is it possible for you to post it, or at least a minimal test case that would illustrate the different errors on the different OSes? What Unix toolkit are you using when running ghc on Windows, if any (cygwin, mingw, both, neither?) Cheers, Kirsten -- Kirsten Chevalier* [EMAIL PROTECTED] *Often in error, never in doubt What is research but a blind date with knowledge? -- Will Henry ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] readFile problem
2007/1/8, Kirsten Chevalier [EMAIL PROTECTED]: On 1/8/07, Stefan Aeschbacher [EMAIL PROTECTED] wrote: There are many things i do not understand. Why the different behaviour on Linux and Windows? Shouldn't an exception be thrown on Linux instead of a core dump? I don't use any unsafePerformIO or foreign calls. Why the changed path? I never change working directory in my code. Why is a function (- reading the config file) re-evaluated at a later point in time? How can I debug such a problem? My environement is ghc 6.6 on Ubuntu or Windows XP. It may be difficult to say without seeing your code. Is it possible for you to post it, or at least a minimal test case that would illustrate the different errors on the different OSes? What Unix toolkit are you using when running ghc on Windows, if any (cygwin, mingw, both, neither?) I know that it's difficult without code but unfortunately the whole program is already quite large (several thousand lines) and I wouldn't see how to extract a relevant test case at the moment as i have no real clue where to search for the problem. I use cygwin on Windows. I just compiled the application from a cmd.exe and the result is the same (even though cmd.exe (and the normal cygwin terminal) swallows the error message, but the error is shown when run in rxvt). regards Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] HaskellForge?
Hi I.e. cabal + hackage + planet.haskell + weekly news ;) Does hackage actually allow a user to setup a new darcs repo on a remote server? That's about the only thing lacking - for everything else people can just use code.google.com, which is way better than anything any Haskell hacker would ever have time to come up with. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] readFile problem
Hi Stefan, I am writing a network server in haskell. Lately I seem to have introduced a new bug. On Linux, when a client closes the connection to the server, the server dumps core. Are you using any calls to system? Any libraries which may do funky stuff? application.exe: config.xml: openFile: does not exist (No such file or directory) I use readFile to read the config file. I tried to print out the config file after it is read to make sure that it is completely read. I only load this config file exactly once during program initialization. The config is used long before the crash. I printed the current working dir in the exception handler and there is something interesting. Instead of the path to the application, it is \C:\\WINDOWS\\system32. What is the working directory at the begining? Is that really the working directory? The \C at the start isn't the C drive, but some bizare escape code, I think. Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
RE: [Haskell-cafe] trouble installing ghc 6.6: xargs: /usr/bin/ar: terminated by signal 11
I've added this useful response to the GHC Building FAQ, here http://hackage.haskell.org/trac/ghc/wiki/Building/FAQ Please continue to add material to this page. Simon | -Original Message- | From: [EMAIL PROTECTED] [mailto:[EMAIL PROTECTED] On Behalf Of Duncan | Coutts | Sent: 07 January 2007 13:38 | To: tphyahoo | Cc: haskell-cafe@haskell.org | Subject: Re: [Haskell-cafe] trouble installing ghc 6.6: xargs: /usr/bin/ar: terminated by signal 11 | | On Sat, 2007-01-06 at 15:30 -0800, tphyahoo wrote: | I'm having trouble installing ghc 6.6. On ubuntu, virtual server (user mode | linux). | | Something seems to be killing the process, no idea why. | | Anyone seen this? | | Yes. | | /usr/bin/ar: creating libHSbase.a | xargs: /usr/bin/ar: terminated by signal 11 | | | What is happening is that the ghc build system is linking thousands and | thousands of tiny .o files into libHSbase.a. GNU ar isn't optimised for | this use-case and it takes far more memory than it really needs to. So | what happens is that ar takes 500Mb of memory and your virtual | machine / virtual server probably isn't configured with that much memory | and so the linux kernel OOM killer terminates the ar process. | | To make this worse, since there are so many .o files, it takes several | invocations of ar to link them all. On each invocation ar is building | the symbol index (-q is ignored) and this is what takes the most time | and memory. It's a good deal quicker to use a custom program (100 lines | of Haskell) to build libHSbase.a and then use ranlib just once to build | the symbol index. | | I submitted a patch to gnu binutils to make ar take less memory when | linking 1000's of files so it now only takes around 100Mb rather than | 500Mb when linking libHSbase.a. That patch is included in version 2.17 I | think (in other words most systems don't have it yet). | | What you can do in the mean time is either configure your virtual | machine with more memory or turn off the split-objs feature when you | configure ghc. Just add SplitObjs=NO to your mk/build.mk file (which | may not exist to start with). (The Gentoo ebuild does this | automatically) | | Duncan | | ___ | Haskell-Cafe mailing list | Haskell-Cafe@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] readFile problem
Hi 2007/1/8, Neil Mitchell [EMAIL PROTECTED]: Hi Stefan, I am writing a network server in haskell. Lately I seem to have introduced a new bug. On Linux, when a client closes the connection to the server, the server dumps core. Are you using any calls to system? Any libraries which may do funky stuff? No calls to system. Libraries I use: MissingH (only some time function) and HaXML. application.exe: config.xml: openFile: does not exist (No such file or directory) I use readFile to read the config file. I tried to print out the config file after it is read to make sure that it is completely read. I only load this config file exactly once during program initialization. The config is used long before the crash. I printed the current working dir in the exception handler and there is something interesting. Instead of the path to the application, it is \C:\\WINDOWS\\system32. What is the working directory at the begining? Is that really the working directory? The \C at the start isn't the C drive, but some bizare escape code, I think. Oups, I think i must have slipped that first \ in by mistake during the composition of the mail. The path at the start of the application is d:\development\simulator_v2 and when the error occurs it is C:\WINDOWS\system32 (without the show i used before). In the last hours I found out the following: the program looks something like this: main = do withSocketsDo $ runSimulator runSimulator = do dir - getCurrentDirectory putStrLn (Dir is: ++ dir) config - readConfig fork many threads It seems as if runSimulator is executed twice when the error happens. The first time dir is printed correctly (d:...). Then the application starts, all threads are created and it runs normally. When the client closes the socket the error: socket: 1832: hGetChar: failed (Unknown error) happens (which in my eyes should rather be isEOFError?). Then the withSocketsDo seems to execute runSimulator again (dir then is C:...). thanks Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
So Terminating contains all the terminating terms in the untyped lambda
calculus and none of the non-terminating ones. And the type checker
checks
this. So it sounds to me like the (terminating) type checker solves the
halting problem. Can you please explain which part of this I have
misunderstood?
-- Lennart
On Jan 7, 2007, at 17:31 , Jim Apple wrote:
To show how expressive GADTs are, the datatype Terminating can hold
any term in the untyped lambda calculus that terminates, and none that
don't. I don't think that an encoding of this is too surprising, but I
thought it might be a good demonstration of the power that GADTs
bring.
{-# OPTIONS -fglasgow-exts #-}
{- Using GADTs to encode normalizable and non-normalizable terms in
the lambda calculus. For definitions of normalizable and de Bruin
indices, I used:
Christian Urban and Stefan Berghofer - A Head-to-Head Comparison of
de Bruijn Indices and Names. In Proceedings of the International
Workshop on Logical Frameworks and Meta-Languages: Theory and
Practice (LFMTP 2006). Seattle, USA. ENTCS. Pages 46-59
http://www4.in.tum.de/~urbanc/Publications/lfmtp-06.ps
@incollection{ pierce97foundational,
author = Benjamin Pierce,
title = Foundational Calculi for Programming Languages,
booktitle = The Computer Science and Engineering Handbook,
publisher = CRC Press,
address = Boca Raton, FL,
editor = Allen B. Tucker,
year = 1997,
url = citeseer.ist.psu.edu/pierce95foundational.html
}
-}
module Terminating where
-- Terms in the untyped lambda-calculus with the de Bruijn
representation
data Term t where
Var :: Nat n - Term (Var n)
Lambda :: Term t - Term (Lambda t)
Apply :: Term t1 - Term t2 - Term (Apply t1 t2)
-- Natural numbers
data Nat n where
Zero :: Nat Z
Succ :: Nat n - Nat (S n)
data Z
data S n
data Var t
data Lambda t
data Apply t1 t2
data Less n m where
LessZero :: Less Z (S n)
LessSucc :: Less n m - Less (S n) (S m)
data Equal a b where
Equal :: Equal a a
data Plus a b c where
PlusZero :: Plus Z b b
PlusSucc :: Plus a b c - Plus (S a) b (S c)
{- We can reduce a term by function application, reduction under
the lambda,
or reduction of either side of an application. We don't need this
full
power, since we could get by with normal-order evaluation, but that
required a more complicated datatype for Reduce.
-}
data Reduce t1 t2 where
ReduceSimple :: Replace Z t1 t2 t3 - Reduce (Apply (Lambda t1)
t2) t3
ReduceLambda :: Reduce t1 t2 - Reduce (Lambda t1) (Lambda t2)
ReduceApplyLeft :: Reduce t1 t2 - Reduce (Apply t1 t3) (Apply
t2 t3)
ReduceApplyRight :: Reduce t1 t2 - Reduce (Apply t3 t1) (Apply
t3 t2)
{- Lift and Replace use the de Bruijn operations as expressed in
the Urban
and Berghofer paper. -}
data Lift n k t1 t2 where
LiftVarLess :: Less i k - Lift n k (Var i) (Var i)
LiftVarGTE :: Either (Equal i k) (Less k i) - Plus i n r - Lift
n k (Var i) (Var r)
LiftApply :: Lift n k t1 t1' - Lift n k t2 t2' - Lift n k (Apply
t1 t2) (Apply t1' t2')
LiftLambda :: Lift n (S k) t1 t2 - Lift n k (Lambda t1) (Lambda
t2)
data Replace k t n r where
ReplaceVarLess :: Less i k - Replace k (Var i) n (Var i)
ReplaceVarEq :: Equal i k - Lift k Z n r - Replace k (Var i) n r
ReplaceVarMore :: Less k (S i) - Replace k (Var (S i)) n (Var i)
ReplaceApply :: Replace k t1 n r1 - Replace k t2 n r2 - Replace
k (Apply t1 t2) n (Apply r1 r2)
ReplaceLambda :: Replace (S k) t n r - Replace k (Lambda t) n
(Lambda r)
{- Reflexive transitive closure of the reduction relation. -}
data ReduceEventually t1 t2 where
ReduceZero :: ReduceEventually t1 t1
ReduceSucc :: Reduce t1 t2 - ReduceEventually t2 t3 -
ReduceEventually t1 t3
-- Definition of normal form: nothing with a lambda term applied to
anything.
data Normal t where
NormalVar :: Normal (Var n)
NormalLambda :: Normal t - Normal (Lambda t)
NormalApplyVar :: Normal t - Normal (Apply (Var i) t)
NormalApplyApply :: Normal (Apply t1 t2) - Normal t3 - Normal
(Apply (Apply t1 t2) t3)
-- Something is terminating when it reduces to something normal
data Terminating where
Terminating :: Term t - ReduceEventually t t' - Normal t' -
Terminating
{- We can encode terms that are non-terminating, even though this
set is
only co-recursively enumerable, so we can't actually prove all of
the
non-normalizable terms of the lambda calculus are non-normalizable.
-}
data Reducible t1 where
Reducible :: Reduce t1 t2 - Reducible t1
-- A term is non-normalizable if, no matter how many reductions you
have applied,
-- you can still apply one more.
type Infinite t1 = forall t2 . ReduceEventually t1 t2 - Reducible t2
data NonTerminating where
NonTerminating :: Term t - Infinite t - NonTerminating
-- x
test1 :: Terminating
test1 = Terminating (Var Zero) ReduceZero NormalVar
-- (\x . x)@y
test2 :: Terminating
test2 = Terminating (Apply (Lambda
Re: [Haskell-cafe] GADTs are expressive
On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote: So Terminating contains all the terminating terms in the untyped lambda calculus and none of the non-terminating ones. And the type checker checks this. So it sounds to me like the (terminating) type checker solves the halting problem. Can you please explain which part of this I have misunderstood? Perhaps you, the user, have to encode the proof of halting in the way you construct the term? Just guessing. Best regards Tomasz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Tomasz Zielonka [EMAIL PROTECTED] wrote: On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote: So it sounds to me like the (terminating) type checker solves the halting problem. Can you please explain which part of this I have misunderstood? Perhaps you, the user, have to encode the proof of halting in the way you construct the term? The Terminating datatype takes three parameters: 1. A term in the untyped lambda calculus 2. A sequence of beta reductions 3. A proof that the result of the beta reductions is normalized. Number 2 is the hard part. For a term that calculated the factorial of 5, the list in part 2 would be at least 120 items long, and each one is kind of a pain. GHC's type checker ends up doing exactly what it was doing before: checking proofs. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] why can't you surround (+) in backticks and have it be infix?
Issues: In Haskell, any function or constructor can be enclosed in backticks and then used as an infix operator. from http://www-users.cs.york.ac.uk/~mfn/hacle/issues/node2.html But this seems to be contradicted by... from #haskell -- 09:19 tphyahoo let func = (+) in 1 `func` 2 -- 09:19 lambdabot 3 -- 09:20 tphyahoo but .. -- 09:20 tphyahoo 1 `(+)` 2 -- 09:20 tphyahoo 1 `(+)` 2 -- 09:20 lambdabot Parse error (+) is a function, is it not? Where's the rub? thomas. -- View this message in context: http://www.nabble.com/why-can%27t-you-surround-%28%2B%29-in-backticks-and-have-it-be-infix--tf2939834.html#a8219424 Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] hsffig build problem
Hello, I am trying to install hsffig and I get the following error: bash$ make : : Linking cabal-setup.exe ... Distribution/Simple/Configure.o:fake:(.text+0x74fd): undefined reference to [EMAIL PROTECTED]' collect2: ld returned 1 exit status make: *** [cabal-setup] Error 1 I am using ghc6.6 in cygwin on windows XP. Has anyone else encountered and/or overcome this? thanks, Jeff --- This e-mail may contain confidential and/or privileged information. If you are not the intended recipient (or have received this e-mail in error) please notify the sender immediately and destroy this e-mail. Any unauthorized copying, disclosure or distribution of the material in this e-mail is strictly forbidden.___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: GHC performance of 64-bit
I noticed that GHC generates slower code on an Linux amd64 bit platform than the 32-bit version on a cheaper 32-bit machine. CPUTime for running sieve of Erathostenes to generate 10,000 primes: Athlon XP 2800 (32-bit): 7.98 secs Athlon 64 3800 (64-bit): 10.29 secs This is using GHC 6.6 on the 64-bit machine and 6.4.1 on the 32-bit one. I googled around and could not find any information regarding degraded performance of ghc/haskell on 64-bit machines. Any ideas? Could it be the effect of doubling the size of pretty much everything, leading to poorer memory-hierarchy performance? Stefan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why can't you surround (+) in backticks and have it be infix?
tphyahoo wrote:
Issues: In Haskell, any function or constructor can be enclosed in backticks
and then used as an infix operator.
from http://www-users.cs.york.ac.uk/~mfn/hacle/issues/node2.html
But this seems to be contradicted by...
from #haskell
-- 09:19 tphyahoo let func = (+) in 1 `func` 2
-- 09:19 lambdabot 3
-- 09:20 tphyahoo but ..
-- 09:20 tphyahoo 1 `(+)` 2
-- 09:20 tphyahoo 1 `(+)` 2
-- 09:20 lambdabot Parse error
(+) is a function, is it not?
Where's the rub?
The thing inside the backticks has to be a syntatic name, not an
expression. The grammar from the Haskell Report
( http://www.haskell.org/onlinereport/syntax-iso.html )...
varid -(small {small | large | digit | ' })reservedid
conid -large {small | large | digit | ' }
varop -varsym | `varid ` (variable operator)
qvarop -qvarsym | `qvarid ` (qualified variable operator)
conop -consym | `conid ` (constructor operator)
qconop -gconsym | `qconid ` (qualified constructor operator)
...I've also thought it would be nice to be able to say things like...
(foo `liftM2 (,)` bar)
Greg Buchholz
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: HaskellForge?
On 2007-01-07, Imam Tashdid ul Alam [EMAIL PROTECTED] wrote: is it a good idea to have HaskellForge? Ruby, Lua and some other languages have already adopted GForge, and I must say, those sites look *impressive*!!! Have you looked at trac? I'm using it for about a dozen projects over on http://software.complete.org/. For instance, http://software.complete.org/missingh I looked at Savane and GForge, and both looks like they were overkill for what I wanted. They are both very invasive on the host system, requiring user accounts to be setup, hosts entries added, DNS control, all sorts of Apache tweaks, etc. You really need a dedicated OS install for them. And neither really seemed to be all that featureful, either. Wikis weren't a standard part of either, and forums were a deprecated part of one. The one thing they have over GForge is mailing list integration, but I just point people to haskell-cafe anyway. Plus: only trac has integration with darcs. It took some time to get trac setup and working the way I want to, with the right plugins, but once done, it's been happy. -- John ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] HaskellForge?
On 1/7/07, Brandon S. Allbery KF8NH [EMAIL PROTECTED] wrote: http://rubyforge.org/ , for one. But I'd argue it's not really Hackage, so much as a pretty wrapper for darcs.haskell.org. (Gems is the Ruby equivalent of Cabal and Hackage.) I've been programming in Ruby for about 1.5 years, and rubyforge is one of the strong features of the community. It's a central place where libraries can be distributed easily to other ruby hackers. From my limited experience with Haskell (about 5 months), finding, installing, and using libraries is one of the bigger pains. For example, if I want to install Rails (ruby web-app framework), I just type: gem install rails It's pretty slick. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why can't you surround (+) in backticks and have it be infix?
On 08/01/07, Greg Buchholz [EMAIL PROTECTED] wrote: ...I've also thought it would be nice to be able to say things like... (foo `liftM2 (,)` bar) You can fake this: (-!) = ($) (!-) = flip ($) foo -! liftM2 (,) !- bar Not perfect, but it's interesting nonetheless. And yes, this was a product of some #haskell brainstorming and algorithm tennis. :) -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On Mon, 8 Jan 2007 08:51:40 -0500 Jim Apple [EMAIL PROTECTED] wrote: The Terminating datatype takes three parameters: 1. A term in the untyped lambda calculus 2. A sequence of beta reductions 3. A proof that the result of the beta reductions is normalized. Number 2 is the hard part. For a term that calculated the factorial of 5, the list in part 2 would be at least 120 items long, and each one is kind of a pain. GHC's type checker ends up doing exactly what it was doing before: checking proofs. Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a partial proof - that *if* the expression you are demanding terminates, you will get a value of the correct type. If it doesn't, you won't get what you wanted. (Unlike in say Coq, where all functions must be proved to terminate - modulo a recently-discovered bug.) What this means is that you can supply e.g. undefined in place of (2) or (3) and fool the typechecker into thinking that (1) terminates, when it doesn't. -- Robin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] HaskellForge?
Am Montag, 8. Januar 2007 17:15 schrieb Justin Bailey: [...] For example, if I want to install Rails (ruby web-app framework), I just type: gem install rails It's pretty slick. How does this work with the native packaging mechanism on your platform (RPM, ...)? Does it work behind it's back (which would be bad)? Let's assume that rails needs foo and bar as well, which are not yet on your box. Does gem install transitively get/update all dependecies of rails? Cheers, S. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
On 1/8/07, Robin Green [EMAIL PROTECTED] wrote: On Mon, 8 Jan 2007 08:51:40 -0500 Jim Apple [EMAIL PROTECTED] wrote: GHC's type checker ends up doing exactly what it was doing before: checking proofs. Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a partial proof - that *if* the expression you are demanding terminates, you will get a value of the correct type. Of course. Were there a recursion-free dialect of Haskell, it could be typecheck/proofcheck the Terminating datatype, though it would be useless for doing any actual work. Proof assistants like Coq can solve this dilemma, and so can languages in the Dependent ML family, by allowing non-terminating programs but only terminating proofs, and by proving termination by well-founded induction. Nobody should think Haskell+GADTs provides the sort of assurances that these can. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] HaskellForge?
On 1/8/07, Sven Panne [EMAIL PROTECTED] wrote: Am Montag, 8. Januar 2007 17:15 schrieb Justin Bailey: [...] For example, if I want to install Rails (ruby web-app framework), I just type: gem install rails It's pretty slick. How does this work with the native packaging mechanism on your platform (RPM, ...)? Does it work behind it's back (which would be bad)? Let's assume that rails needs foo and bar as well, which are not yet on your box. Does gem install transitively get/update all dependecies of rails? Gems is pretty self-contained - gems can depend on other gems, with a variety of versioning options. If you try to install a gem that depends on others, you will be asked if you wish to install those first (unless the correct versions are already present on your machine). I use Windows so there isn't any other packaging system for it to interact with. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Beta Gtk2Hs Getting Started
Hello All, The beta of the 'Gtk2Hs:Getting Started' short tutorial for beginners, Haskell GUI for Dummies, if you like :-) can be viewed at http://j-van-thiel.speedlinq.nl/gtk2hs/gtk2hsGetStart.html It tells what Gtk2Hs is, shows how to write and run 'Hello World', introduces the api and explains how to use it, refers to the Glade tutorials, gives an example of widget layout, and ends with some general pointers. It should take no more than 2,3 hours of the user's time. All feedback very welcome. Regards, Hans van Thiel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Beta Gtk2Hs Getting Started
Hallo, On 1/8/07, Hans van Thiel [EMAIL PROTECTED] wrote: Hello All, The beta of the 'Gtk2Hs:Getting Started' short tutorial for beginners, Haskell GUI for Dummies, if you like :-) can be viewed at http://j-van-thiel.speedlinq.nl/gtk2hs/gtk2hsGetStart.html Nitpicking: Glade does not belong to GTK+, neither does libglade, which are independent projects. -- -alex http://www.ventonegro.org/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] trouble installing greencard -- -fno-prune-tydecls flag ( was Re: trivial function application question )
I wrote: In the meantime, how about the following: In default non-verbose mode, silently memoize the list of packages that were not found. Then, only if something goes wrong, say something like: The package failed to build. Perhaps the reason is that one of the following packages was not found: Neil Mitchell wrote: That doesn't seem that helpful. On error, give a list of maybe 25 things that are missing, only to find out that you're running GHC 6.4.1 on Windows which no one ever tried before. It's not really narrowing the cause of the error too much anyway. Oh, I agree completely. Clearly it would be great if Cabal could process and report dependencies in a more meaningful way. However, if that will take more time before it can happen, I am just supporting what a few other people have already suggested in this thread as an easy first step. These do not require any change in the way Cabal processes things - just the way messages are printed. I am just combining a few things already said : o Verbose and non-verbose options. o Always show information if something really went wrong. o Include a message that may help people not to panic as much. -Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] why can't you surround (+) in backticks and have it be infix?
David House wrote: : | You can fake this: | | (-!) = ($) | (!-) = flip ($) | | foo -! liftM2 (,) !- bar | | Not perfect, but it's interesting nonetheless. | | And yes, this was a product of some #haskell | brainstorming and algorithm tennis. :) :-) Was anyone in that brainstorm thinking of Chung-chieh Shan's -: and :- (http://www.haskell.org/pipermail/haskell-cafe/2002-July/003215.html) or was the similarity just a really cool coincidence? Regards, Tom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why can't you surround (+) in backticks and have it be infix?
On 08/01/07, [EMAIL PROTECTED] [EMAIL PROTECTED] wrote: Was anyone in that brainstorm thinking of Chung-chieh Shan's -: and :- (http://www.haskell.org/pipermail/haskell-cafe/2002-July/003215.html) It's likely. I don't remember exactly where it came from. -- -David House, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
Robin Green wrote: Well, not really - or not the proof you thought you were getting. As I am constantly at pains to point out, in a language with the possibility of well-typed, non-terminating terms, like Haskell, what you actually get is a partial proof - that *if* the expression you are demanding terminates, you will get a value of the correct type. I only want to point out that the above terminates actually is can be put in NF, since putting the expression in WHNF is not enough. In other words, you need deepSeq, not seq when forcing/checking proofs. To partially mitigate this problem, I believe strictness annotations can be used, as in data Nat t where Z :: Nat Zero S :: ! Nat t - Nat (Succ t) Now one could safely write foo :: Nat t - A t - B foo proof value = proof `seq` -- here you can assume t to be a finite type-level natural If proof is invalid, foo will return _|_. Using no strictess annotation, but still using seq instead of deepSeq, the code above would be unsafe, since one can always pass (S undefined) as proof. Using seq also allows to check the proof in constant time (neglecting the proof generation time, of course). deepSeq instead would require traversing the proof each time one wants to check it, e.g. in different functions. Does anyone else believe that using strictess annotations in GADT proof terms would be good style? Zun. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] why can't you surround (+) in backticks and have it beinfix?
[EMAIL PROTECTED] wrote: David House wrote: You can fake this: (-!) = ($) (!-) = flip ($) foo -! liftM2 (,) !- bar Was anyone in that brainstorm thinking of Chung-chieh Shan's -: and :- (http://www.haskell.org/pipermail/haskell-cafe/2002-July/003215.html) or was the similarity just a really cool coincidence? I hope no-one seriously thinks the above syntax is clearer than: liftM2 (,) foo bar Brian. -- Operators: one small step for compilers, one giant leap for obfuscation. http://www.metamilk.com ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] MissingH: profiler support?
Hey all, I'm trying to profile my application, which makes use of MissingH. But when compiling with -prof -auto-all, I get the following error: Language.hs:8:7: Could not find module `Data.String': Perhaps you haven't installed the profiling libraries for package MissingH-0.18.0? Use -v to see a list of the files searched for. When compiling without those options, everything works just fine. I built missingh from source, and added -prof -auto-all to GHCPARMS, and did a ./setup configure,make,install and still no result. Does anyone know what could be wrong? I'd really like to keep using MissingH and having profiling support at the same time. Thanks, -chris ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: [Gtk2hs-users] Beta Gtk2Hs Getting Started
On Mon, 2007-01-08 at 18:20 +0100, Hans van Thiel wrote: Hello All, The beta of the 'Gtk2Hs:Getting Started' short tutorial for beginners, Haskell GUI for Dummies, if you like :-) can be viewed at http://j-van-thiel.speedlinq.nl/gtk2hs/gtk2hsGetStart.html It tells what Gtk2Hs is, shows how to write and run 'Hello World', introduces the api and explains how to use it, refers to the Glade tutorials, gives an example of widget layout, and ends with some general pointers. It should take no more than 2,3 hours of the user's time. All feedback very welcome. Hooray! Thanks Hans. I should also note that a new release of Gtk2Hs is imminent. You can grab the latest pre-release and report any issues: http://haskell.org/gtk2hs/gtk2hs-0.9.10.4.tar.gz Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Beta Gtk2Hs Getting Started
On Mon, 2007-01-08 at 16:11 -0200, Alex Queiroz wrote: Hallo, On 1/8/07, Hans van Thiel [EMAIL PROTECTED] wrote: Hello All, The beta of the 'Gtk2Hs:Getting Started' short tutorial for beginners, Haskell GUI for Dummies, if you like :-) can be viewed at http://j-van-thiel.speedlinq.nl/gtk2hs/gtk2hsGetStart.html Nitpicking: Glade does not belong to GTK+, neither does libglade, which are independent projects. Though they're pretty tightly integrated. Glade is the recommended way to build Gtk+ UIs. Indeed the libglade functionality is going to be included in Gtk+ itself in the next major release. So yes, technically they're currently independent components but for the purposes of an intro tutorial I think it's fine to introduce them all as one programmer's toolkit. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] GADTs are expressive
Thanks! I'm sure I could have figured this out by looking at the code, but it was easier to ask. It's very cool example, even if it doesn't practical. :) -- Lennart On Jan 8, 2007, at 08:51 , Jim Apple wrote: On 1/8/07, Tomasz Zielonka [EMAIL PROTECTED] wrote: On Mon, Jan 08, 2007 at 08:02:36AM -0500, Lennart Augustsson wrote: So it sounds to me like the (terminating) type checker solves the halting problem. Can you please explain which part of this I have misunderstood? Perhaps you, the user, have to encode the proof of halting in the way you construct the term? The Terminating datatype takes three parameters: 1. A term in the untyped lambda calculus 2. A sequence of beta reductions 3. A proof that the result of the beta reductions is normalized. Number 2 is the hard part. For a term that calculated the factorial of 5, the list in part 2 would be at least 120 items long, and each one is kind of a pain. GHC's type checker ends up doing exactly what it was doing before: checking proofs. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Monad Set via GADT
On 1/3/07, Roberto Zunino [EMAIL PROTECTED] wrote: 1) Why the first version did not typececk? 2) Why the second one does? 3) If I replace (Teq a w) with (Teq w a), as in SM :: Ord w = Teq w a - Set.Set w - SetM a then union above does not typecheck! Why? I guess the type variable unification deriving from matching Teq is not symmetric as I expect it to be... These are very interesting questions that I forgot about until reminded by Haskell Weekly News. Thanks, HWN! 1) Class constraints can't be used on pattern matching. They ARE restrictive on construction, however. This is arguably bug in the Haskell standard. It is fixed in GHC HEAD for datatypes declared in the GADT way, so as not to break H98 code: http://article.gmane.org/gmane.comp.lang.haskell.cvs.all/29458/match=gadt+class+context 2) The second one works because Class constraints can be used when pattern matching existentials. 3) I imagine this might have something to do with the coercions that System FC uses. With one ordering, a coercion might occur that in another one is unnecessary. This coercion might allow the use of Ord w by using it before the coercion from S.Set a to S.Set w. #3 is just a guess. Jim ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] HaskellForge?
On Mon, 2007-08-01 at 18:19 +0100, Sven Panne wrote: For example, if I want to install Rails (ruby web-app framework), I just type: gem install rails It's pretty slick. How does this work with the native packaging mechanism on your platform (RPM, ...)? Does it work behind it's back (which would be bad)? It doesn't. It is its own Ruby-specific packaging mechanism. Let's assume that rails needs foo and bar as well, which are not yet on your box. Does gem install transitively get/update all dependecies of rails? Well rails needs dozens of libraries, seemingly, and it can be told to collect all dependencies. (If it isn't told one way or another, it asks.) This is true, however, iff the dependencies are all gems themselves. If you need a third-party library installed that's not wrapped in a gem, you have to use your usual packaging system to get it. (Being an Ubuntu user, I use aptitude.) Overall, I like the gems approach. The Ruby packages for debian-alikes are almost invariably out of date and building a lot of these Ruby enhancements is a pain in the posterior. If I want a stable version of a given component, I'll use aptitude (or RPM or whatever) and live with it being out of date. If I want the latest and greatest, however, I'll stick to the gems. Since gems can be installed and deleted just like aptitude's packages can be (and just as cleanly) it really isn't that hard an approach. -- Michael T. Richter Email: [EMAIL PROTECTED], [EMAIL PROTECTED] MSN: [EMAIL PROTECTED], [EMAIL PROTECTED]; YIM: michael_richter_1966; AIM: YanJiahua1966; ICQ: 241960658; Jabber: [EMAIL PROTECTED] [Blacks] ... are inferior to the whites in the endowments both of body and mind. --Thomas Jefferson signature.asc Description: This is a digitally signed message part ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
