[Haskell-cafe] who maintains the POSIX/Unix Unistd.hs?
Hello, I am trying to find the definition for the data type TimeSpec/CTimeSpec. thanks, Vasili ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
Luke Palmer wrote: It seems that there is a culture developing where people intentionally ignore the existence of seq when reasoning about Haskell. Indeed I've heard many people argue that it shouldn't be in the language as it is now, that instead it should be a typeclass. I wonder if it's possible for the compiler to do more aggressive optimizations if it, too, ignored the existence of seq. Would it make it easier to do various sorts of lambda lifting, and would it make strictness analysis easier? The introduction of seq has several implications. The first problem is that parametricity would dictate that the only functions of type forall a,b. a - b - b are const id const _|_ _|_ Since seq is different from these, giving it this polymorphic type weakens parametricity. This does have implications for optimizations, in particular for fusion, see also http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion Parametricity can be restored with a class constraint seq :: Eval a = a - b - b In fact, that's how Haskell 1.3 and 1.4 did it. The second problem are function types. With seq on functions, eta-expansion is broken, i.e. we no longer have f = \x.f x because seq can be used to distinguish _|_ and \x. _|_ One of the many consequences of this is that simple laws like f = f . id no longer hold, which is a pity. But then again, _|_ complicates reasoning anyway and we most often pretend that we are only dealing with total functions. Unsurprisingly, this usually works. This can even be justified formally to some extend, see also N.A.Danielsson, J.Hughes, P.Jansson, J.Gibbons. Fast and Loose Reasoning is Morally Correct. http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] help in tree folding
Daniel Fischer ha scritto: Am Dienstag, 6. Mai 2008 22:40 schrieb patrik osgnach: Brent Yorgey ha scritto: On Tue, May 6, 2008 at 8:20 AM, patrik osgnach [EMAIL PROTECTED] wrote: Hi. I'm learning haskell but i'm stuck on a generic tree folding exercise. i must write a function of this type treefoldr::(Eq a,Show a)=(a-b-c)-c-(c-b-b)-b-Tree a-c Tree has type data (Eq a,Show a)=Tree a=Void | Node a [Tree a] deriving (Eq,Show) as an example treefoldr (:) [] (++) [] (Node '+' [Node '*' [Node 'x' [], Node 'y' []], Node 'z' []]) must return +∗xyz any help? (sorry for my bad english) Having a (Tree a) parameter, where Tree is defined as an algebraic data type, also immediately suggests that you should do some pattern-matching to break treefoldr down into cases: treefoldr f y g z Void = ? treefoldr f y g z (Node x t) = ? -Brent so far i have tried treefoldr f x g y Void = x Yes, nothing else could be done. treefoldr f x g y (Node a []) = f a y Not bad. But actually there's no need to treat nodes with and without children differently. Let's see: treefoldr f x g y (Node v ts) should have type c, and it should use v. We have f :: a - b - c x :: c g :: c - b - b y :: b v :: a. The only thing which produces a value of type c using a value of type a is f, so we must have treefoldr f x g y (Node v ts) = f v someExpressionUsing'ts' where someExpressionUsing'ts' :: b. The only thing we have which produces a value of type b is g, so someExpressionUsing'ts' must ultimately be g something somethingElse. Now take a look at the code and type of foldr, that might give you the idea. Cheers, Daniel treefoldr f x g y (Node a (t:ts)) = treefoldr f x g (g (treefoldr f x g y t) y) (Node a ts) but it is incorrect. i can't figure out how to build the recursive call thanks for the answer Patrik thanks for the tip. so, if i have understood correctly i have to wirite something like: treefoldr f x g y (Node a ts) = f a (g (treefoldr f x g y (head ts)) (g (treefoldr f x g y (head (tail ts)) (g ... it looks like a list foldr so... treefoldr f x g y Void = x treefoldr f x g y (Node a ts) = f a (foldr (g) y (map (treefoldr f x g y) ts)) it seems to work. i'm not yet sure it is correct but is better than nothing thanks to you all. now i will try to write a treefoldl ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] The Monad.Reader (11) - Call for Copy
Call for Copy The Monad.Reader - Issue 11 Please consider writing something for the next issue of The Monad.Reader. The deadline for Issue 11 is ** August 1, 2008 ** It doesn't matter if you're a respected researcher or if you have only just started learning Haskell, get your thoughts together and write an article for The Monad.Reader! The Monad.Reader is a electronic magazine about all things Haskell. It is less formal than journal, but more enduring than a wiki-page or blog. There have been a wide variety of articles, including: exciting code fragments, intriguing puzzles, book reviews, tutorials, and even half-baked research ideas. * Submission Details * Get in touch with me if you intend to submit something -- the sooner you let me know what you're up to, the better. Please submit articles for the next issue to me by e-mail (wss at cs.nott.ac.uk). Articles should be written according to the guidelines available from http://www.haskell.org/haskellwiki/The_Monad.Reader Please submit your article in PDF, together with any source files you used. The sources will be released together with the magazine under a BSD license. If you would like to submit an article, but have trouble with LaTeX please let me know and we'll sort something out. All the best, Wouter This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
Just for curiocity, is there a practically useful computation that uses 'seq' in an essential manner, i.e. apart from the efficiency reasons? Abhay On Wed, May 7, 2008 at 2:48 PM, apfelmus [EMAIL PROTECTED] wrote: Luke Palmer wrote: It seems that there is a culture developing where people intentionally ignore the existence of seq when reasoning about Haskell. Indeed I've heard many people argue that it shouldn't be in the language as it is now, that instead it should be a typeclass. I wonder if it's possible for the compiler to do more aggressive optimizations if it, too, ignored the existence of seq. Would it make it easier to do various sorts of lambda lifting, and would it make strictness analysis easier? The introduction of seq has several implications. The first problem is that parametricity would dictate that the only functions of type forall a,b. a - b - b are const id const _|_ _|_ Since seq is different from these, giving it this polymorphic type weakens parametricity. This does have implications for optimizations, in particular for fusion, see also http://www.haskell.org/haskellwiki/Correctness_of_short_cut_fusion Parametricity can be restored with a class constraint seq :: Eval a = a - b - b In fact, that's how Haskell 1.3 and 1.4 did it. The second problem are function types. With seq on functions, eta-expansion is broken, i.e. we no longer have f = \x.f x because seq can be used to distinguish _|_ and \x. _|_ One of the many consequences of this is that simple laws like f = f . id no longer hold, which is a pity. But then again, _|_ complicates reasoning anyway and we most often pretend that we are only dealing with total functions. Unsurprisingly, this usually works. This can even be justified formally to some extend, see also N.A.Danielsson, J.Hughes, P.Jansson, J.Gibbons. Fast and Loose Reasoning is Morally Correct. http://www.comlab.ox.ac.uk/people/jeremy.gibbons/publications/fast+loose.pdf Regards, apfelmus ___ 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
[Haskell-cafe] Re: Control.Exception.evaluate - 'correct definition' not so correct
Abhay Parvate wrote: Just for curiocity, is there a practically useful computation that uses 'seq' in an essential manner, i.e. apart from the efficiency reasons? I don't think so because you can always replace seq with const id . In fact, doing so will get you more results, i.e. a computation that did not terminate may do so now. In other words, we have seq _|_ = _|_ seq x = idfor x _|_ but (const id) _|_ = id (const id) x = id for x _|_ So, (const id) is always more defined () than seq . For more about _|_ and the semantic approximation order, see http://en.wikibooks.org/wiki/Haskell/Denotational_semantics Regards, apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] runInteractiveProcess and hGetLine on Windows
Hello all,
I bumped into a feature which might be a bug, but to be certain, I'd
like to hear your opinion. I'm running ghc 6.8.2 on Windows XP, and with
ghci I do the following:
Prelude System.Process System.IO (inp,outp,err,ph) -
runInteractiveProcess kpsewhich [testfile.txt] Nothing
Nothing
('kpsewhich' is a simple path searching utility used by web2c TeX
system, returns the full path to the file if found in the system defined
search path, but you all probably know that.)
and then:
Prelude System.Process System.IO hGetLine outp
which gives me:
./testfile.txt\r
as opposed to ./testfile.txt which I get on my Linux box.
Is the \r supposed to be at the end? I thought it is part of the line
separator in Windows, and as such, should not be part of the line
retrieved? Same thing happens when compiled with ghc.
Best Wishes,
Harri K.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Haddock and upload questions?
2008/5/6 Galchin, Vasili [EMAIL PROTECTED]: 2) http://hackage.haskell.org/packages/upload.html - do I have to set up my .cabal in a special way to run dist? I believe it works automatically, using the values of the fields you set, e.g. Exposed-modules and Other-modules. - once I checked that my Cabal package is compliant on this page, how do I get a username and password? http://hackage.haskell.org/packages/accounts.html Linked from the front page of hackage: http://hackage.haskell.org/packages/hackage.html -- Denis ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, May 07, 2008 at 04:42:45PM +0200, Harri Kiiskinen wrote: Prelude System.Process System.IO (inp,outp,err,ph) - runInteractiveProcess kpsewhich [testfile.txt] Nothing Nothing ... Prelude System.Process System.IO hGetLine outp which gives me: ./testfile.txt\r as opposed to ./testfile.txt which I get on my Linux box. Is the \r supposed to be at the end? I thought it is part of the line separator in Windows, and as such, should not be part of the line retrieved? Same thing happens when compiled with ghc. This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). In order to get windows-style line handling, a file handle needs to be opened in text mode, which is certainly not the correct behavior for runInteractiveProcess, which has no knowledge about the particular behavior of the program it's running. \r\n as newline should die a rapid death... windows is hard enough without maintaining this sort of stupidity. -- David Roundy Department of Physics Oregon State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, May 07, 2008 at 08:33:23AM -0700, Bryan O'Sullivan wrote: David Roundy wrote: This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). I think it would be more accurate to say that runInteractiveProcess has an inadequate API, since you can't indicate whether the interaction with the other process should happen in text or binary mode. I don't see any reason to support text mode. It's easy to filter by hand if you absolutely have to deal with ugly applications on ugly platforms. -- David Roundy Department of Physics Oregon State University ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
Hello David, Wednesday, May 7, 2008, 7:46:11 PM, you wrote: I don't see any reason to support text mode. It's easy to filter by hand if you absolutely have to deal with ugly applications on ugly platforms. you mean unix, of course? ;) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, May 07, 2008 at 07:48:45PM +0400, Bulat Ziganshin wrote: Hello David, Hi Bulat! Wednesday, May 7, 2008, 7:46:11 PM, you wrote: I don't see any reason to support text mode. It's easy to filter by hand if you absolutely have to deal with ugly applications on ugly platforms. you mean unix, of course? ;) Maybe I should have said if you don't care what the actual output of the programs you run is? Then it would have been clear that I was talking about Windows... David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On May 7, 2008, at 8:46 AM, David Roundy wrote: On Wed, May 07, 2008 at 08:33:23AM -0700, Bryan O'Sullivan wrote: David Roundy wrote: This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). I think it would be more accurate to say that runInteractiveProcess has an inadequate API, since you can't indicate whether the interaction with the other process should happen in text or binary mode. I don't see any reason to support text mode. Doesn't hGetLine imply text mode? What does Line mean, otherwise? Donn Cave, [EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, May 7, 2008 at 9:12 AM, Donn Cave [EMAIL PROTECTED] wrote: Doesn't hGetLine imply text mode? What does Line mean, otherwise? On normal operating systems, line means until you reach a '\n' character. In fact, that's also what it means when reading in text mode, it's just that when in text mode on DOS-descended systems, the character sequence \r\n is converted to \n by the operating system. David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Figuring out if an algebraic type is enumerated through Data.Generics?
On Wed, May 7, 2008 at 7:47 AM, Jules Bean [EMAIL PROTECTED] wrote: Alfonso Acosta wrote: It would certainly be difficult map any Haskell type to VHDL, so, by now we would be content to map enumerate algebraic types (i.e. algebraic types whose all data constructors have arity zero, e.g. data Colors = Green | Blue | Red) Wouldn't it be much simpler to use the standard deriveable classes Bounded and Enum, instead of an admittedly very clever trick using Data? No, for the reasons explained in the probably_unnnecesary_background I don't see how those instantiations would help. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
David Roundy [EMAIL PROTECTED] wrote: ...when in text mode on DOS-descended systems, the character sequence \r\n is converted to \n by the operating system. So basically, Windows supports both the \n convention and the \r\n convention by making a distinction between text and binary read modes. No other major operating system requires this distinction -- they are all *nixen -- so it seems reasonable to just punt on it. It would be too bad, though, if this resulted in a lot of Windows specific code getting written -- there are a lot of Windows users and eventually they'll unionize or something. People will throw together System.Win32.TextMode or something like that and then projects will be littered with platform specific code, though they needn't be. If we just put up a `textMode` filter, then everyone will have to throw that in front of their reads/writes to guard against corruption on Windows. We'll have verbose, silly looking code. If, on the other hand, we just give in to Windows, then some things are good and some are bad. First of all, if hGetLine has Windows behaviour on Windows and Unix behaviour on Unix, then any data files shipped with Cabal packages will likely need to be newline transformed. That is annoying. On the other hand, the semantics of 'getting a line' will be maintained across platforms, and the Windows users will be pacified (for a time). We all know what appeasement got the British... -- _jsn ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
David Roundy wrote: \r\n as newline should die a rapid death... windows is hard enough without maintaining this sort of stupidity. Windows *does* do a number of very silly things. However, Windows isn't going away any time soon. And personally, I'd prefer it if we could make it easier to support it in Haskell. I think a pure function that takes text formatted in any way and transforms it into some kind of canonical form would be a useful starting point. You'd probably want a platform-specific inverse function too. (I notice that FilePath manages to work differently on different platforms, so it's possible.) Currently the only way to do these transformations is to set the right channel mode at the instant you read the text. If we had a set of pure functions, you could transform the text after it's read - even if it's read in the wrong file mode, or you don't know whether it's text or binary until later. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] The Monad.Reader (11) - Call for Copy
Wouter Swierstra wrote: Please consider writing something for the next issue of The Monad.Reader. You know, I'm actually tempted to do just that... It doesn't matter if you're a respected researcher or if you have only just started learning Haskell, get your thoughts together and write an article for The Monad.Reader! It probably *does* matter, however, that I don't have anything interesting to say. :-( Ah well. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, 2008-05-07 at 08:33 -0700, Bryan O'Sullivan wrote: David Roundy wrote: This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). I think it would be more accurate to say that runInteractiveProcess has an inadequate API, since you can't indicate whether the interaction with the other process should happen in text or binary mode. Simon: do the new entry points in System.Process take line ending conventions into account? It doesn't require any new api: (inh,outh,errh,pid) - runInteractiveProcess path args Nothing Nothing -- We want to process the output as text. hSetBinaryMode outh False As of a couple weeks ago the docs for runInteractiveProcess even say: -- The 'Handle's are initially in binary mode; if you need them to be -- in text mode then use 'hSetBinaryMode'. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, 2008-05-07 at 08:46 -0700, David Roundy wrote: On Wed, May 07, 2008 at 08:33:23AM -0700, Bryan O'Sullivan wrote: David Roundy wrote: This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). I think it would be more accurate to say that runInteractiveProcess has an inadequate API, since you can't indicate whether the interaction with the other process should happen in text or binary mode. I don't see any reason to support text mode. It's easy to filter by hand if you absolutely have to deal with ugly applications on ugly platforms. If it was only Windows' silly line ending convention I'd be tempted to agree but we probably want to distinguish text and binary handles anyway. You get Chars out of a text handle (with some string ed/decoding) and bytes out of a binary handle. In that case, default line ending convention is just another thing to throw in with the text encoding conversion. Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Wed, May 07, 2008 at 09:24:46PM +0100, Duncan Coutts wrote: On Wed, 2008-05-07 at 08:46 -0700, David Roundy wrote: On Wed, May 07, 2008 at 08:33:23AM -0700, Bryan O'Sullivan wrote: David Roundy wrote: This is the correct behavior (although it's debatable whether kpsewhich should be outputting in text mode). I think it would be more accurate to say that runInteractiveProcess has an inadequate API, since you can't indicate whether the interaction with the other process should happen in text or binary mode. I don't see any reason to support text mode. It's easy to filter by hand if you absolutely have to deal with ugly applications on ugly platforms. If it was only Windows' silly line ending convention I'd be tempted to agree but we probably want to distinguish text and binary handles anyway. You get Chars out of a text handle (with some string ed/decoding) and bytes out of a binary handle. In that case, default line ending convention is just another thing to throw in with the text encoding conversion. But that's a feature that was only added in a very recent ghc, right? I consider it an ugly hack to work around the fact that we have no system for dealing with file encodings. I'd rather consider text mode handles to be an ugly workaround for an ugly system, and have a clean solution for unicode (e.g. one that allows for the reading of files that are not in the locale encoding). I certainly wouldn't want to be forced to live with DOS line endings just to generate unicode output. Fortunately, darcs doesn't do unicode (or need to) or text mode, so I personally am pretty safe from this feature. David ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Using Template Haskell to make type-safe database access
Hi Wouter Wouter Swierstra wrote: Here's a concrete example. Suppose you have a query q that, when performed, will return a table storing integers. I can see how you can ask the SQL server for the type of the query, parse the response, and compute the Haskell type [Int]. I'm not sure how to sum the integers returned by the query *in Haskell* (I know SQL can sum numbers too, but this is a simple example). What would happen when you apply Haskell's sum function to the result of the query? Does TH do enough compile time execution to see that the result is well-typed? Not only pictures, but also code can say more than a thousands words. Therefore, I have been implementing a proof of concept. The code is attached in two files - SqlExpr.hs and UseSqlExpr.hs. The former contains two SQL expressions + Haskell code. The latter is the Template Haskell (TH) code that makes it possible to type-safely access the database. UseSqlExpr.hs is a lot easier to understand than SqlExpr.hs. So if you only have time to look at one of them, look at UseSqlExpr.hs. The reason SqlExpr.hs is harder to understand is not just because it is longer, but also because TH is difficult. At least TH was difficult for me. It might just be because I have never worked with anything like TH before (have not learned Lisp yet :( ). It remained me of going from OO to FP. You have to change how you think. Your example of fetching a [Int] and take there sum is shown in UseSqlExpr.hs. The output from running UseSqlExpr.hs (on my computer) is: [1,2,3,4] [(1,WikiSysop,),(2,Mads,Mads Lindstr\195\184m),(3,Madstest,Bob),(4,Test2,Test 2)] Sum is: 10 Having the SQL server compute types for you does have other drawbacks, I think. For example, suppose your query projects out a field that does not exist. An error like that will only get caught once you ask the server for the type of your SQL expression. If you keep track of the types in Haskell, you can catch these errors earlier; Haskell's type system can pinpoint which part of the query is accessing the wrong field. I feel that if you really care about the type of your queries, you should guarantee type correctness by construction, rather than check it as an afterthought. But the SQL database will output a meaningful error message. And TH is asking the server at compile time. Thus, the user can also get the error message at compile time. TH is used as part of the compilation process. I _think_ it would be fair to say it occurs concurrently with type checking (or maybe intermittently). Thus the user do not get the error message later than with a type based approach. If you, with the currently implemented proof of concept, name a non-existing field in your SQL you get: compile time output UseSqlExpr.hs:22:6: Exception when trying to run compile-time code: Exception when trying executing prepared statement : execute execute: [1054: [MySQL][ODBC 3.51 Driver][mysqld-5.0.32-Debian_7etch5-log]Unknown column 'duser_id' in 'field list'] Code: compileSql DSN=MySQL_DSN;USER=StocksDaemon; SELECT duser_id FROM user; In the expression: $[splice](compileSql DSN=MySQL_DSN;USER=StocksDaemon; SELECT duser_id FROM user;) c In the definition of `selectIntegerList': selectIntegerList c = $[splice](compileSql DSN=MySQL_DSN;USER=StocksDaemon; SELECT duser_id FROM user;) c make: *** [all] Fejl 1 /compile time output ok, there is some noise. But at the end of line three it says Unknown column 'duser_id'. Also with a little more work I could properly improve the output. Perhaps I should explain my own thoughts on the subject a bit better. I got interested in this problem because I think it makes a nice example of dependent types in the real world - you really want to But won't you end up implementing all the functionality of an SQL parser? While possible, it does seem like a huge job. With a TH solution you will safe a lot of work. Also, almost every software developer already knows SQL. And the few that do not, will likely have to learn SQL if they are to do substantial work with databases. Whereas if you implement a type based solution a developer will have to learn how to use your library. A library that will be a lot more complex to learn than what I am proposing (assuming the developer already knows SQL). compute the *type* of a table based on the *value* of an SQL DESCRIBE. Nicolas Oury and I have written a draft paper describing some of our ideas: http://www.cs.nott.ac.uk/~wss/Publications/ThePowerOfPi.pdf I have not read the paper yet, as I have been busy coding. Plus I have a day job. But I did read the first couple of pages and so far the paper seems very interesting. When time permits I will read the rest. Hopefully this weekend. Any
Re: [Haskell-cafe] Induction (help!)
Hi One of you chaps mentioned the Nat data type data Nat = Zero | Succ Nat Let's have add :: Nat - Nat - Nat add Zero n = n add (Succ m)n = Succ (add m n) Prove add m Zero = m I'm on the verge of giving up on this. :-( Cheers Paul ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re[2]: [Haskell-cafe] Using Template Haskell to make type-safe database access
Hello Mads, Thursday, May 8, 2008, 1:24:05 AM, you wrote: also because TH is difficult. At least TH was difficult for me. It might just be because I have never worked with anything like TH before (have no, TH is dificult by itself. if you have spare time - read about metalua, which implements the same idea in Lua environment. it's simple and straightforward, and even allows to easily change syntax. one possible reason of TH difficulty may be that Haskell is strict-typed language -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Induction (help!)
PR Stanley wrote: add Zero n = n So this function takes the left argument, and replaces Zero with n. Well if n = Zero, this clearly leaves the left argument unchanged... ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Induction (help!)
On Wed, May 7, 2008 at 9:27 PM, PR Stanley [EMAIL PROTECTED] wrote: Hi One of you chaps mentioned the Nat data type data Nat = Zero | Succ Nat Let's have add :: Nat - Nat - Nat add Zero n = n add (Succ m)n = Succ (add m n) Prove add m Zero = m To prove this by induction on m, you would need to show: 1) add Zero Zero = Zero 2) If add m Zero = m, then add (Succ m) Zero = Succ m Number (1) is completely trivial, nothing more needs to be said. (2) is easy, after expanding the definition. Here the P I used was P(x) := add m Zero = m, the thing we were trying to prove. (1) is a base case, P(Zero). (2) is the inductive step, If P(m) then P(Succ m). Hoping I don't sound patronizing: if you're still having trouble, then I suspect you haven't heard what it means to prove an if-then statement. Here's a silly example. We want to prove: If y = 10, then y - 10 = 0. First we *assume* the condition of the if. We can consider it true. Assume y = 10. Show y - 10 = 0. Well, y = 10, so that's equivalent to 10 - 10 = 0, which is true. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
Thank You all for the lively discussion, and of course, a nice and simple answer to my problem: On Wed, 2008-05-07 at 21:17 +0100, Duncan Coutts wrote: (inh,outh,errh,pid) - runInteractiveProcess path args Nothing Nothing -- We want to process the output as text. hSetBinaryMode outh False As to the following claim: As of a couple weeks ago the docs for runInteractiveProcess even say: -- The 'Handle's are initially in binary mode; if you need them to be -- in text mode then use 'hSetBinaryMode'. At least the haskell.org standard library reference does not say this (http://haskell.org/ghc/docs/latest/html/libraries/process/System-Process.html), but the information can be found on the System.IO reference page. As a general comment to this feature, I find it quite acceptable, as on non-Windows systems it does no harm, and on Windows, you get the desired behaviour. Seems to reflect closely the practice and distinction in C (http://en.wikipedia.org/wiki/Newline), too. Harri K. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] who maintains the POSIX/Unix Unistd.hs?
2008/5/7 Galchin, Vasili [EMAIL PROTECTED]: Hello, I am trying to find the definition for the data type TimeSpec/CTimeSpec. http://www.haskell.org/ghc/docs/latest/html/libraries/unix/src/System-Posix-Unistd.html Doesn't look like it's exported from anywhere, just used internally for c_nanosleep AGL -- Adam Langley [EMAIL PROTECTED] http://www.imperialviolet.org ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
On Thu, 2008-05-08 at 00:12 +0200, Harri Kiiskinen wrote: Thank You all for the lively discussion, and of course, a nice and simple answer to my problem: On Wed, 2008-05-07 at 21:17 +0100, Duncan Coutts wrote: (inh,outh,errh,pid) - runInteractiveProcess path args Nothing Nothing -- We want to process the output as text. hSetBinaryMode outh False As to the following claim: As of a couple weeks ago the docs for runInteractiveProcess even say: -- The 'Handle's are initially in binary mode; if you need them to be -- in text mode then use 'hSetBinaryMode'. At least the haskell.org standard library reference does not say this (http://haskell.org/ghc/docs/latest/html/libraries/process/System-Process.html) Sorry, I wasn't clear. I meant that it was added in the development branch a couple weeks ago. http://darcs.haskell.org/libraries/process/System/Process.hs Duncan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Induction (help!)
Paul,
Sometimes it helps to go exhaustively through every detail to be sure
there is no magic going on. Proceed only if you want exhaustive detail...
If it seems that people are skipping some steps in their argument, it is
because they are! They already understand it so well that they forgot to
add them. Here is what I believe is an excruciatingly complete proof, to
assure you that no handwaving is going on.
The values of Nat are defined inductively on their structure, using its
initial algebra. Take the data type definition
data Nat = Zero | Succ Nat
There is actually an implied undefined as well, so this is really
Nat = undefined | Zero | Succ Nat
Just as 3 = const 3 x for any x, we can convert from pointed to
pointfree notation (i.e. go from a recursive definition to a
least-defined fixed point definition):
f = const undefined | const Zero | Succ
Nat = LFP (m - infinity) ( f^m undefined )
[ For the notationally picky, I am using | instead of + in the functor
for clarity, which causes no ambiguity.]
Because we are overachievers, we will prove our theorem not just for the
least-defined fixed point of f, but change the limit to a union and
prove it for (f^m undefined) for every m, which includes the fixed point.
Why the extra work? Because now we have an inductive argument. The base
case is undefined, and each step is another application of f.
DEFINITION:
add Zero n = n -- Line 1
add (Succ m) n = Succ (add m n)-- Line 2
THEOREM:
forall x :: Nat, add x Zero = x
PROOF: By induction
BASE CASE: x = f^0 undefined = undefined
add undefined Zero = undefined
{ Line 1, strict pattern match failure in first arg }
STEP CASE: Assume add x Zero = x, Prove add y Zero = y where y in f x
What y are in f x?
f x = (const undefined | const Zero | Succ) x
= const undefined x | const Zero x | Succ x
= undefined | Zero | Succ x
We have to consider each of these possibilities for y.
1) add undefined Zero = undefined { Base case }
2) add Zero Zero = Zero{ Def. line 1 }
3) add (Succ x) Zero
= Succ (add x Zero){ Def. line 2 }
= Succ x { Step case assumption }
This exhausts the three cases for y.
Therefore, by induction add x Zero = x for all x :: Nat
Note how structural induction maps to induction over integers. You do
not have to enumerate some flattened form of the domain and do induction
over their enumerated order. Indeed, some domains (like binary trees)
are not even countably infinite, so the induction hypothesis would not
be valid when used in this way.
Instead you rely on the fact that all algebraic data types already have
an (at most countably infinite) complete partial order based on
constructor application (or eqivalently, initial algebra composition)
[and always remembering that there is an implied union in | with
undefined], grounded at undefined, and that consequently you can do
induction over constructor application.
I hope that there are no errors in the above and that I have not left
out even the smallest detail. You should be able to see from the above
that structural induction works on any algebraic data type.
Obviously, after the first time only a masochist would be so verbose.
But the induction hypothesis does after all require a first time! :)
Dan Weston
PR Stanley wrote:
Hi
One of you chaps mentioned the Nat data type
data Nat = Zero | Succ Nat
Let's have
add :: Nat - Nat - Nat
add Zero n = n
add (Succ m)n = Succ (add m n)
Prove
add m Zero = m
I'm on the verge of giving up on this. :-(
Cheers
Paul
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Induction (help!)
So, when you apply the function to the first element in the set - e.g. Zero or Nil in the case of lists - you're actually testing to see the function works. Then in the inductive step you base everything on the assumption that p holds for some n and of course if that's true then p must hold for Succ n but you have to prove this by taking Succ from n and thus going bakc to its predecessor which is also the hypothesis p(n). So, to reiterate assumption: if hypothesis then conclusion if p(n) then p(Succ n) proof of assumption if p(Succ n) = Succ(p(n)) then we've won. If pn+1) = p(n) + p(1) then we have liftoff! I'm not going to go any further in case I'm once again on the wrong track. Cheers Paul At 22:43 07/05/2008, you wrote: On Wed, May 7, 2008 at 9:27 PM, PR Stanley [EMAIL PROTECTED] wrote: Hi One of you chaps mentioned the Nat data type data Nat = Zero | Succ Nat Let's have add :: Nat - Nat - Nat add Zero n = n add (Succ m)n = Succ (add m n) Prove add m Zero = m To prove this by induction on m, you would need to show: 1) add Zero Zero = Zero 2) If add m Zero = m, then add (Succ m) Zero = Succ m Number (1) is completely trivial, nothing more needs to be said. (2) is easy, after expanding the definition. Here the P I used was P(x) := add m Zero = m, the thing we were trying to prove. (1) is a base case, P(Zero). (2) is the inductive step, If P(m) then P(Succ m). Hoping I don't sound patronizing: if you're still having trouble, then I suspect you haven't heard what it means to prove an if-then statement. Here's a silly example. We want to prove: If y = 10, then y - 10 = 0. First we *assume* the condition of the if. We can consider it true. Assume y = 10. Show y - 10 = 0. Well, y = 10, so that's equivalent to 10 - 10 = 0, which is true. Luke ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Induction (help!)
PR Stanley [EMAIL PROTECTED] wrote: Hi One of you chaps mentioned the Nat data type data Nat = Zero | Succ Nat Let's have add :: Nat - Nat - Nat add Zero n = n add (Succ m)n = Succ (add m n) Prove add m Zero = m I'm on the verge of giving up on this. :-( The important point is to learn to regard an infinite number of terms as one term, and how to mess with it without allowing individual terms to escape or dangle around. -- (c) this sig last receiving data processing entity. Inspect headers for past copyright information. All rights reserved. Unauthorised copying, hiring, renting, public performance and/or broadcasting of this signature prohibited. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
Windows:end of line is \r\n Unix: end of line is \n BUT, these days Windows programs have to deal with text files written on Unix, and Unix programs have to deal with text files written on Windows, especially when mounting networked file systems using things like NFS and Samba. Even when working with local files, there isn't any way for a program on either system to tell where a text file originally came from. So programs on BOTH systems really need to deal with BOTH conventions. We can go further: the Internet convention for end of line is, sadly, and somewhat accidentally, the same as the Windows convention. It's a right pain sometimes having to remember to stuff \r into things on UNIX so that it will go the right way down the wire (according to the strict protocol) to a program on the other end whose designer really wished the \r weren't there, but that's the world we live in. According to the ASCII standard, it was fully legitimate to use backspace and carriage return to get over-striking (which is why ASCII includes oddities such as ^ and ` : they really are for accents, and , did double duty as cedilla, ' as acute accent, =\b/ really was not-equals (as was /\b=), c). According the the ISO 8859 standard, that's not kosher any more. So there are (on Windows and Unix) no known uses for isolated \r characters. Accordingly, a text mode that simply throws away every \r it comes across will not just be useful on Windows, it will be useful on Unix as well. The old DOS Ctrl-Z convention hasn't been recommended practice on Windows for years, so there's not much point bothering with that. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Interesting critique of OCaml
An interesting critique of OCaml. http://enfranchisedmind.com/blog/2008/05/07/why-ocaml-sucks/ One phrase that stood out, regarding GHC's support for deforestation transformations like build/foldr and stream fusion: Haskell is doing data structure level optimizations with the ease that most other compiler do peephole instruction optimization. This is a non-trivial result. Which I think really captures the joy of being able to write algebraic and data structure transformations, via rewrite rules, without having to extend the compiler -- all thanks to purity, laziness, and static typing. -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] I am new to haskell
Hi All, I am new to Haskell. Can anyone guide me how can I start on it (Like getting binaries, some tutorials)? Thanks in advance. -- Regards, Ambrish Bhargava ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] How can see old threads.
Hi, I want to know, how can see old threads (may be I can get my answers from there itself)? -- Regards, Ambrish Bhargava ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] I am new to haskell
On Thu, 2008-05-08 at 10:07 +0530, Ambrish Bhargava wrote: Hi All, I am new to Haskell. Can anyone guide me how can I start on it (Like getting binaries, some tutorials)? All of this is on haskell.org. I'm kind of curious how you know about this mailing list without going to haskell.org or seeing all the resources on it. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How can see old threads.
bhargava.ambrish: Hi, I want to know, how can see old threads (may be I can get my answers from there itself)? You can search the list here: http://dir.gmane.org/gmane.comp.lang.haskell.cafe And find more information about all the lists and other resources at: http://haskell.org -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How can see old threads.
Thanks.. On Thu, May 8, 2008 at 10:26 AM, Don Stewart [EMAIL PROTECTED] wrote: bhargava.ambrish: Hi, I want to know, how can see old threads (may be I can get my answers from there itself)? You can search the list here: http://dir.gmane.org/gmane.comp.lang.haskell.cafe And find more information about all the lists and other resources at: http://haskell.org -- Don -- Regards, Ambrish Bhargava ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] runInteractiveProcess and hGetLine on Windows
Richard A. O'Keefe [EMAIL PROTECTED] writes: According to the ASCII standard, it was fully legitimate to use backspace and carriage return to get over-striking (which is why ASCII includes oddities such as ^ and ` : they really are for accents, and , did double duty as cedilla, ' as acute accent, =\b/ really was not-equals (as was /\b=), c). According the the ISO 8859 standard, that's not kosher any more. So there are (on Windows and Unix) no known uses for isolated \r characters. Say what? I use \r when generating output to a terminal when I want to update the current line of output instead of writing a new line. E.g. for tracking progress in my programs. (As a line terminator followed by \n, it would have no effect though.) -k -- If I haven't seen further, it is by standing in the footprints of giants ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
