August 2010 - Beginners

Using the state monad.
by dan portin 08 Aug '10

08 Aug '10

I wrote a simple tableau theorem prover for propositional logic as my first Haskell program. My next goal is to write a theorem prover for modal logic. Fortunately, this is more complicated. In essence, I have a tableau data type, a rules function, and a rewrite function, which generate a tableau, surrounded by auxiliary functions to collapse the tableau into paths and extract interpretations. The tableau rewrite function is below. The "Status" and "check" functions are unnecessary, but I added them anyways, because some (other) tableau proof systems will require them. data Tableau = Node Status Expr [Tableau] deriving Eq data Status = C | I deriving (Show, Eq) -- Rules for propositional tableau. Rules are of the form (s, ex), where -- the value of s (Action) indicates the appropriate action (extend or branch) -- for the tableau rewritign function to take when injecting the formulas in -- the list ex. rule :: Expr -> (Action, [Expr]) rule (Var x) = (None, [Var x]) rule (Not (Var x)) = (None, [Not (Var x)]) rule (Not (Not e)) = (Extend, [e]) rule (Impl e1 e2) = (Branch, [Not e1, e2]) rule (Not (Impl e1 e2)) = (Extend, [e1, Not e2]) rule (Conj e1 e2) = (Extend, [e1, e2]) rule (Not (Conj e1 e2)) = (Branch, [Not e1, Not e2]) rule (Disj e1 e2) = (Branch, [e1, e2]) rule (Not (Disj e1 e2)) = (Extend, [Not e1, Not e2]) -- 'rewrite' constructs a complete tableau from a given tableau by applying the -- appropriate tableau rule at each incomplete node, then appropriately -- injecting the resultant expressions into the tableau. 'rewrite' recurses over -- the tableau until all nodes are complete. 'consTableau' constructs a -- complete tableau from an expression. consTableau :: Expr -> Tableau consTableau e = rewrite $ Node I e [] rewrite :: Tableau -> Tableau rewrite t = case (isComplete t) of True -> moveAnd rewrite t False -> case (rule $ getExpr t) of (None, _) -> check $ moveAnd rewrite t (Extend, ex) -> rewrite (check $ inject Extend ex t) (Branch, ex) -> rewrite (check $ inject Branch ex t) inject :: Action -> [Expr] -> Tableau -> Tableau inject a ex (Node s expr []) = case a of Extend -> Node s expr [foldr (\e y -> Node I e [y]) (Node I (last ex) []) (init ex)] Branch -> Node s expr $ map (\e -> Node I e []) ex inject a ex (Node s expr es) = Node s expr $ map (\b -> inject a ex b) es The most common rule for modal tableaux is: For a formula (◊P, *w*), increment *w* by some number *n *to yield the relation (*w*, *w* + *n*), then extending the tableau with a formula (P, *w + n*) for each formula (◻P, *w*) on the current path. In order to implement the rule, I would need to: (a) save the state of the tableau after each rewrite rule is applied; (b) if a rewrite rule for ◊ is applied, index the resultant relation and rewrite every formula ◻P on the current path; (3) check for infinite loops using a fairly simple algorithm. I see two ways this could be accomplished: (1) Implement the tableau rewriting using the state monad; (2) use a function like *rewrite* which saves the state of the tableau in an argument (so that after each rewrite, the state of the tableau is stored, and I can restart the recursion at that point). I'm trying to learn Haskell, however, so I'd like to learn more about monads. I understand the simple examples of monads generally given in tutorials (like Wadler's paper, which I'm working through), but I'm not sure what the *general structure* of what I'm looking for would look like (that is a problem). So my question, finally, is: *what would be the general structure of the implementation of the state monad for a tableau-style theorem prover* *look like, schematically*. I can't really square my goal with example implementations of the state monad, where the state is threaded through in a series of let expressions. Thanks, and sorry for the long post.

2 2

Integer performance of GHC
by Sebastián E. Peyrott 07 Aug '10

07 Aug '10

Hi, I'm looking for information on Haskell's viability for heavy integer math. My (very) naive tests show Haskell lagging behind C even when doing heavy (manual) inlining, compiling with special optimizations (funbox-strict-fields) and using continuation-passing-style when possible. Of course, being a beginner myself, I don't really know how good my code is. For reference, I wrote a simple MD5 implementation. It's as fast as the one in Happstack (Happstack.Crypto.MD5), which on my computer runs around 2.77 times slower then the base version from GNU coreutils (md5sum). GHC primitives appear as the next logical step in my tests, however I've been having problems using fixed sizes for integers (Word32# comes with no prim-ops defined?). Do you have any insights on this? Is it reasonable to expect Haskell integer performance to reach the levels of C with current implementations? Which are the limiting factors? Thanks!

3 5

Foreign function interface?
by Mathew de Detrich 07 Aug '10

07 Aug '10

---------- Forwarded message ---------- From: Mathew de Detrich <deteego(a)gmail.com> Date: Sat, Aug 7, 2010 at 7:19 PM Subject: Re: [Haskell-beginners] Foreign function interface? To: aditya siram <aditya.siram(a)gmail.com> Actually it is possible to use C++ with FFI without having to use a C Wrapper (albeit its quite complicated) http://www.haskell.org/haskellwiki/Cxx_foreign_function_interface <http://www.haskell.org/haskellwiki/GHC/Using_the_FFI>Also refer to http://qthaskell.berlios.de/ (thats a practical example of QtHaskell, which is a haskell binding to a C++ library, being Qt) <http://qthaskell.berlios.de/> On Sat, Jul 31, 2010 at 6:49 AM, aditya siram <aditya.siram(a)gmail.com>wrote: > > Can it interface with C++ as well as C? > No you have to wrap your C++ code in C. > -deech <Beginners(a)haskell.org> > > _______________________________________________ > Beginners mailing list > Beginners(a)haskell.org > http://www.haskell.org/mailman/listinfo/beginners > >

1 1

Re: [Haskell-beginners] Parsec
by C Gosch 06 Aug '10

06 Aug '10

2010/8/6 Dean Herington <heringtonlacey(a)mindspring.com> > At 11:42 PM +0200 8/5/10, C Gosch wrote: > >> Hi, >> does anyone here know their way around in Parsec? >> I'm trying to parse a file which contains some binary parts too. >> I have been using Parsec 3.0.1 to parse the first ASCII part, but all the >> parsers are >> returning Char type tokens, so it would not work with the binary parts .. >> is there any way to do this? >> I am using Text.Parsec.ByteString.Lazy. >> >> Note that I'm new to Haskell and Parsec, and doing this within a small >> project that >> I basically do to get a grip on Haskell (and Parsec, because it appears to >> be really nifty and I want to learn more about it). >> >> Thanks for any hints, >> Christian >> > > Parsing binary parts of a file is not inherently a problem. A parser can > return any type; different parsers in your application will likely return > different types. > > If you include some code we'll be able to help you more specifically. > > Dean > You're right, I probably used the wrong words .. I meant that apparently the tokens Parsec uses are of type Char, and I would actually at some point like to continue parsing, but using different tokens. Sorry if I still got it wrong, I'm new :) I can post some code later, as I don't have it here right now. Cheers, Christian

4 5

Parsec
by C Gosch 06 Aug '10

06 Aug '10

Hi, does anyone here know their way around in Parsec? I'm trying to parse a file which contains some binary parts too. I have been using Parsec 3.0.1 to parse the first ASCII part, but all the parsers are returning Char type tokens, so it would not work with the binary parts .. is there any way to do this? I am using Text.Parsec.ByteString.Lazy. Note that I'm new to Haskell and Parsec, and doing this within a small project that I basically do to get a grip on Haskell (and Parsec, because it appears to be really nifty and I want to learn more about it). Thanks for any hints, Christian

2 1

Re: [Haskell-beginners] Boilerplate Code
by Matt Andrew 05 Aug '10

05 Aug '10

I had a play today and managed to figure out how to write the code I needed. If anyone is curious the resulting code is: {-# LANGUAGE TemplateHaskell #-} module Template where import Language.Haskell.TH typeChecker :: String -> Q Exp typeChecker schemeType = do x <- newName "x" return $ LamE [VarP x] (CaseE (VarE x) [Match (ConP ty [WildP]) (NormalB (AppE (ConE bool) (ConE true))) [],Match WildP (NormalB (AppE (ConE bool) (ConE false))) []]) where ty = mkName schemeType bool = mkName "Bool" true = mkName "True" false = mkName "False" I then import this module into where I am defining the predicates (templates have to be defined in a seperate module), where the code becomes: numberP :: SchemeVal -> SchemeVal numberP = $(typeChecker "Number") boolP :: SchemeVal -> SchemeVal boolP = $(typeChecker "Bool") symbolP :: SchemeVal -> SchemeVal symbolP = $(typeChecker "Symbol") So, as I always knew, not really worth the effort as I've written a 13 line module to save 3 lines of code, but a good learning experience =) Thanks again for the point in the right direction. Cheers, Matt

2 2

getopt
by Gaius Hammond 05 Aug '10

05 Aug '10

Hi all, I have used GetOpt in Python and Ocaml so I am reasonably familiar with it, and I have been studying the technique here: http://www.haskell.org/haskellwiki/High-level_option_handling_with_GetOpt Can anyone explain to me what is actually happening here: opts <- foldl (>>=) (return startOptions) actions let Options { optVerbose = verbose , optInput = input , optOutput = output } = opts input >>= output I understand the fold is evaluating everything in the actions list overlaying them onto the startOptions record, then getting these out of IO and into the opts record - but where are "verbose", "input" and "output" coming from? Are they just aliases? Any insight gratefully received :-) Thanks, G

3 2

package random requires two versions of time
by Ashish Agarwal 05 Aug '10

05 Aug '10

Running 'cabal configure' on one of our code bases gives: package random-1.0.0.2 requires time-1.1.4 package random-1.0.0.2 requires time 1.2.03 in addition to several other such warnings. This one is the oddest however since it is the same version of random that presumably requires two different versions of time. How can that be? Output of 'cabal info random' gives: Dependencies: base >= 3 && <5, time -any This happens only on a Debian system, in which I installed the Haskell Platform using apt-get.

2 2

How to avoid Gmail attachments? ("An HTML attachment was scrubbed")
by Peter Schmitz 04 Aug '10

04 Aug '10

I see that when I post to the Haskell lists ( http://www.haskell.org/mailman/listinfo) from gmail, the end of my post has: "

3 3

Question regarding the ListT Monad Transformer
by Tim Cowlishaw 04 Aug '10

04 Aug '10

Hey all, I'm trying to get my head around the ListT Monad Transformer, and am having trouble working out how to use it. Essentially, I am trying to transform a type of [IO a] to IO [a] I'd assumed that this might work something like this Transform [IO a] to ListT IO a call runListT to transform ListT IO a to IO [a] ..having I'd assumed that this was the correct situation to use a Monad Transformer, as I'm layering monads around each other. However, while the second half of the transformation above is catered for via runListT - I can't seem to work out how to do the first - namely, to write a function of type [IO a] -> ListT IO a . To be honest, I'm not entirely sure I've entirely got my head around Monad Transformers yet - does what I'm describing make any sense at all, and if so, is there any chance you could point me in the right direction towards implementing (and hopefully understanding) this? Cheers, Tim

2 2