Discussion

Coq and The Monad Laws: Introduction

Submitted by mrd on Wed, 08/15/2007 - 2:26pm.

Over the past few months I've been spending some time with Coq, the proof assistant. I am still very much a beginner, so as an exercise I decided to try and prove the three Monad laws for the implementation of the List Monad.

In Haskell, the List Monad looks like this:

instance Monad [] where return x = [x] m >>= f = concatMap f m

Coq is a proof-assistant for a constructive logic, so it can also be used as a (dependently-typed) functional programming language. You can open an interactive session and type the lines in using coqtop. However, I use the ProofGeneral Emacs-based interface and save my code in a file like "listmonad.v". You can then step through the lines using C-c C-n. There also exists a custom GUI called CoqIDE.

In Coq, I defined the Monad methods like so:

Section ListMonad. Require Import List. Definition ret (A : Set) (a : A) := a :: nil. Definition bind (A B : Set) (m : list A) (f : A -> list B) := flat_map f m.

I opened up a new section (but did not close it yet). The definitions are fairly unremarkable, except that now the types A and B are explicit parameters. In Coq, a single colon is used for type annotations, and a double colon is used for list consing. flat_map is Coq's version of concatMap. I did not know that before, but found it by using SearchAbout list. at the interactive Coq prompt.

I can see what Coq thinks of my definitions:

Coq < Check ret. ret : forall A : Set, A -> list A Coq < Check bind. bind : forall A B : Set, list A -> (A -> list B) -> list B

Now we are ready to state the three Monad Laws. First, in Haskell notation:

1. return a >>= f = f a 2. m >>= return = m 3. (m >>= f) >>= g = m >>= (\x -> f x >>= g)

The first two Monad laws, in essence, assert that return is an identity operation on the left and right sides of bind. The third says that bind is associative.

In Coq:

Theorem first_law : forall (A B : Set) (a : A) (f : A -> list B), bind A B (ret A a) f = f a. Theorem second_law : forall (A : Set) (m : list A), bind A A m (ret A) = m. Theorem third_law : forall (A B C : Set) (m : list A) (f : A -> list B) (g : B -> list C), bind B C (bind A B m f) g = bind A C m (fun x => bind B C (f x) g).

Entering any of these Theorems into Coq will engage the interactive proof mode. In the next article, I will examine the proofs of the first two laws.

Haskell and XML

Submitted by mrd on Sun, 08/05/2007 - 8:59am.

I installed HXT this week to use in a small project which dealt with some XML data. It is a slick library, and it has introduced me to the joy of Arrows. I scavenged for tutorial information, and there are some useful pages out there -- The Haskellwiki page on HXT, and Neil Bartlett's recent blog entry.

However, when it came down to getting some practical work done, I found myself scouring the HXT Arrow API documentation. While it is pretty neat to figure out which combinator to use solely based on the examination of types, I would have preferred a selection of code examples.

That is what Practical Examples of HXT in Action is attempting to be. I've concocted 3 articles so far, and I'm hoping to add more. The current examples demonstrate: arrow syntax, basic useful combinators, a little development methodology, optional and list data, and simple integration with Network.HTTP.

Chess in Haskell

Submitted by chessguy on Thu, 06/28/2007 - 9:30pm.

I thought that since chess AI is (or, at least, has been) a hobby of mine, it would be fun and educational to write one in Haskell. And if I'm going to do that, I figure I may as well blog about it!

A few preliminary matters before I dive into the code. First, I make no promises as to how often I will add to this blog. A chess AI is a long project, and I don't currently have a ton of time to devote to it. Second, I intend to start very simply, and inefficiently, with data structures that I know can be improved on. Part of the fun will be refactoring it later. Finally, I fully admit to being a novice Haskeller. I've been studying it for a year or so now, but still struggle with things I should have mastered long ago. Suggestions are highly desirable.

Ok, let's do this! First, a few definitions:

type Board = Array Int Piece

data Piece = Piece Color PieceType
data Color = White | Black
data PieceType = Pawn | Knight | Bishop | Rook | Queen | King

We represent a board as a simple array, indexed by Ints. This gives us O(1) access to any square. This is one area that I guarantee I will come back to, but it's simple enough to start with. Board representation is a HUGE issue with chess AI, and there are many, many things we can try with it. Anyway, we'll use a standard convention, which is to number square A1 (the square closest to white, on his left) as square 0, and H8 (on black's left) as 63. That is, the board will look like this (leading 0's added for spacing only):
BLACK
56 57 58 59 60 61 62 63
48 49 50 51 52 53 54 55
40 41 42 43 44 45 46 47
32 33 34 35 36 37 38 39
24 25 26 27 28 29 30 31
16 17 18 19 20 21 22 23
08 09 10 11 12 13 14 15
00 01 02 03 04 05 06 07
WHITE

Now a few useful little things:

emptyBoard :: Board
emptyBoard = array (0,63) []

piece :: Char -> Piece
piece c = Piece color pType
where color = if (isUpper c) then White else Black
pType = case (toUpper c) of
'P' -> Pawn
'N' -> Knight
'B' -> Bishop
'R' -> Rook
'Q' -> Queen
'K' -> King

addToBoard :: Piece -> Int -> Board -> Board
addToBoard piece loc board = board // [(loc, piece)]

An empty board is trivially defined as an integer within the proper range, and with no associations. I'll note here that I've never really dealt with arrays in haskell, so this will be a learning process. I already like the fact that creating an empty array is so intuitive. The piece function is a simple constructor for Piece. It follows a typical chess convention for denoting pieces: uppercase means white, lowercase means black. More on chess notation in a moment. addToBoard adds a piece to the board. Again, it's very simple and elegant-feeling.

Now comes the fun part for this entry:

loadFEN :: String -> Board
loadFEN = loadFEN' 56 emptyBoard

loadFEN' :: Int -> Board -> String -> Board
loadFEN' _ b (' ':xs) = b
loadFEN' _ b "" = b
loadFEN' n b ('/':xs) = loadFEN' (n-16) b xs
loadFEN' n b (x:xs) | x `elem` ['1'..'9'] = loadFEN' (n + (digitToInt x)) b xs
loadFEN' n b (x:xs) = loadFEN' (n+1) b' xs
where b' = addBoard (piece x) n b

Chess has this awful thing about notation. There are a few different ones (particularly for move representation), and they tend to be pretty awful. This function is to convert a string, in a notation called FEN, to an instance of our board data structure. a description of FEN can be found here . Suffice it to say, this is a tedious process to do in any language. In fact, the above function is very elegant compared to many languages. Essentially, we're simply looping through the string, while keeping a reference to the next square on the board that we're going to put a piece on. Since FEN starts with the square on black's right, we start on square 56 (see above diagram). We'll assume for now that the FEN is well-formed.

If you notice from the Wikipedia article, there are several fields to FEN notation. For now, we'll just deal with the first, and longest field, which tells where the pieces are. We'll come back to the other fields later. Thus, if the first character of the string is a space, or if the string is empty, then we're done, and we can simply return the board. If it's a slash, we've reached the end of a row, and we need to move the board reference to the beginning of the next row, then process the rest of the string. If the first character is a digit, it indicates some empty squares, so we'll simply adjust the board reference again. Finally, the only option left, is that we're looking at an actual piece, in which case we need to construct the piece, add it to the board, and process the rest of the string.

I think that's enough for this entry. Next time: move generation!

Dynamic Programming in Haskell

Submitted by mrd on Thu, 02/22/2007 - 8:57pm.

Dynamic Programming is an algorithm design strategy which can be essentially described as breaking a problem down into subproblems and re-using previously computed results. Sometimes, a problem which appears to take exponential time to solve can be reformulated using a Dynamic Programming approach in which it becomes tractable. The benefit is especially clear when the subproblem solutions overlap considerably. The technique of memoization is a major time-saver in those cases.

A common Haskell newbie question is: how do I memoize? At first, it appears to be a very difficult problem, because access to mutable arrays and hashtables is restricted. It is important to realize that lazy evaluation is actually memoization itself and can be leveraged in that way for the purposes of Dynamic Programming. In fact, as a result, the expression of these algorithms can be more natural and lucid in Haskell than in a strict language.

Here, I am going to examine the classic ``knapsack problem.'' Given a number of items, their values, and their sizes -- what is the best combination of items that you can fit in a limited-size knapsack?

> module Knapsack where > import Control.Monad > import Data.Array > import Data.List > import Test.QuickCheck
I am going to represent items with this data type. Essentially, it is just a tuple of the item itself, its value, and its size. > data Item a = Item { item :: a, > itemValue :: Int, > itemSize :: Int } > deriving (Eq, Show, Ord)
Cells will be used both to represent the solution to the knapsack problem, and as individual cells in the matrix for the Dynamic Programming algorithm. It is a pair consisting of: summed values, and the items in the sack. > data Cell a = Cell (Int, [Item a]) > deriving (Eq, Show, Ord)
This powerset definition is a very neat use of the List monad (which I pulled from the Haskell wiki). You can think of it as saying: for each element in the list, half the possible subsets will include it, and half will not. > powerset :: [a] -> [[a]] > powerset = filterM (const [True, False])
brutepack considers the powerset of the items, cutting out those subsets which are too large in size, and picking the most valuable subset left. As you might figure, this is going to run in O(2^n) thanks to the use of powerset. The definition should be simple to understand and will provide a sound basis for testing the Dynamic Programming alternative. > brutepack :: (Ord a) => Int -> [Item a] -> Cell a > brutepack size items = maximum [ > cellOf subset | > subset <- powerset items, itemsFit subset > ] > where > itemsFit items = sum (map itemSize items) <= size > cellOf items = Cell (sum (map itemValue items), items)

The Dynamic Programming algorithm is as follows:

Consider a matrix where the rows are indexed by size and the columns by items. The rows range from 1 to the size of the knapsack, and the columns are one-to-one with the items in the list.


value = $30     $20    $40
 size =  4       3      5
_item_|_lion___tiger___bear_
      |
     1|
      |
     2|
      |
     3|
      |
     4|        v(2,4)<--.
      |                 |
     5|                 |
      |                 |
     6|                 |
      |                 |
     7|                 |
      |              <--|    
     8|        v(2,8) v(3,8)
      |

This is a diagram where the knapsack has a maximum size allowance of 8, and we want to stuff some animals in it. Each element in the matrix is going to tell us the best value of items by size. That means the answer to the whole problem is going to be found in v(3,8) which is the bottom-rightmost corner.

The value of any one cell in the matrix will be decided by whether it is worthwhile to add that item to the sack or not. In the v(3,8) cell it compares the v(2,8) cell to the left to the v(2,4) cell up above. The v(2,8) cell has no room for the bear, and the v(2,4) cell represents the situation where the bear will fit. So the question, after determining if the bear will fit in the bag at all, is: is value of bear + v(2,4) better than v(2,8)?

This definition of v lends itself to a very nice recursive formulation.

             
              / v(m-1,n)                    if (s_n) > n
              \ 
    v(m,n) = -|      / v(m-1,n)
              /      \
              \ max -|                      otherwise
                     /
                     \ v(m-1,n-(s_n)) + v_n
where s_n is the size of item n and v_n is its value.

A typical implementation of this algorithm might initialize a 2D array to some value representing ``undefined.'' In Haskell, we can initialize the entire array to the correct value directly and recursively because it will not be computed until needed. All that is necessary is to express the data-dependencies, and the order of evaluation will take care of itself.

This code takes the algorithm a little further by tracking a field in each cell that contains a list of the items in the sack at that point.

> dynapack :: Int -> [Item a] -> Cell a > dynapack size items = valOf noItems size > where > noItems = length items > itemsArr = listArray (1,noItems) items > itemNo n = itemsArr ! n > > table = array ((1,1),(noItems,size)) $ > [ > ((m, n), cell m n) | > m <- [1..noItems], > n <- [1..size] > ] > > valOf m n > | m < 1 || n < 1 = Cell (0, []) > | otherwise = table ! (m,n) > > cell m n = > case itemNo m of > i@(Item _ v s) > | s > n || > vL >= vU + v -> Cell (vL , isL) > | otherwise -> Cell (vU + v, i:isU) > where > Cell (vL, isL) = valOf (m - 1) n > Cell (vU, isU) = valOf (m - 1) (n - s)

The matrix is defined in the variable table and valOf is our function v here. This definition very naturally follows from the algorithmic description because there is no problem with self-reference when defining cells in the array. In a strict language, the programmer would have to manually check for the presence of values and fill in the table.

Testing

It's important to be confident that the algorithm is coded correctly. Let's see if brutepack and dynapack agree on test inputs. I will define my own simple data type to customize the randomly generated test data.

> newtype TestItems = TestItems [(Int, Int, Int)] > deriving (Eq, Show, Ord)
> nubWithKey k = nubBy (\a b -> k a == k b) > fst3 (a,b,c) = a > tripleToItem (i,v,s) = Item i v s

The Arbitrary class expects you to define your customly generated test data in the Gen monad. QuickCheck provides a number of handy combinators, and of course you can use normal monadic functions.

sized is a QuickCheck combinator which binds the generator's notion of "size" to a parameter of the supplied function. This notion of "size" is a hint to test-data creators that QuickCheck wants data on the "order of" that size. Of course, what "size" means can be freely interpreted by the author of the function, in this case I am using it for a couple purposes.

The basic idea is simply: create a list of randomly generated tuples of length "size", and choose values and item-sizes randomly from (1, "size"). Notice how the randomly generated tuple is replicated with the monadic combinator replicateM. Then, before returning, just make sure that there are no "repeated items" by running nubWithKey fst3 over the generated list. That will cut out any items with the same name as previous items.

> instance Arbitrary TestItems where > arbitrary = sized $ \n -> do > items <- replicateM n > $ do > i <- arbitrary > v <- choose (1, n) > s <- choose (1, n) > return $ (i, v, s) > return . TestItems . nubWithKey fst3 $ items

With an Arbitrary instance, we can now define a property: it extracts the tuples and creates Items out of them, then tries out both algorithms for equivalence. Note that I am only checking the final values, not the actual items, because there may be more than one solution of the same value.

> prop_effectivePacking (TestItems items) = v1 == v2 > where items' = map tripleToItem items > Cell (v1,_) = brutepack 16 items' > Cell (v2,_) = dynapack 16 items'
Knapsack> verboseCheck prop_effectivePacking 0: TestItems [(1,2,3),(3,2,2)] 1: TestItems [] 2: TestItems [(1,1,1)] 3: TestItems [(2,1,2),(-1,2,3),(0,2,3)] 4: TestItems [(-2,2,2),(-1,1,1),(3,2,3),(4,2,2)] ...

It will progressively check larger "size" samples and you will notice that the brute force algorithm is going to start dragging down performance mightily. On my computer, in the ghci interpreter, brutepack on even just 20 items takes 10 seconds; while dynapack takes almost no time at all.

Conclusion

Algorithms making use of Dynamic Programming techniques are often expressed in the literature in an imperative style. I have demonstrated an example of one such algorithm in a functional language without resorting to any imperative features. The result is a natural recursive expression of the algorithm, that has its advantage from the use of lazy evaluation.

Synchronized threads, part II

Submitted by mrd on Fri, 01/05/2007 - 6:34pm.

For comparison, here is an implementation of multiple threads of which each attempt to perform as many steps as possible in 1 second.


> import Control.Monad > import Control.Concurrent > import Control.Concurrent.STM > import Data.List > import Data.IORef > import System.Time > import System.Environment > import System.IO > import System.Random > import Text.Printf > import Ratio

oneThread greedily attempts to loop through as many steps as possible until one second has elapsed. Then it blocks while it waits for the main thread to collect the previous result, so it can put the new result in the TMVar. Every step it takes, it executes the supplied function parameter f.

> oneThread :: TMVar Int -> Int -> a -> (a -> a) -> IO () > oneThread mvar n v f = do > TOD s ps <- getClockTime > loop (fromIntegral s + ps%(10^12)) n n v > where > loop prevTime prevN n v = do > TOD s ps <- getClockTime > let now = fromIntegral s + ps%(10^12) > tdiff = now - prevTime > ndiff = fromIntegral $ n - prevN > sps = floor (ndiff / tdiff) > v' = f v > if tdiff >= 1 then > do atomically $ putTMVar mvar sps > loop now n n v > else v' `seq` loop prevTime prevN (n + 1) v'

nosync is akin to sync in that it is an STM action which collects results from all the threads via the TMVars. Again, the key portion is easy: mapM takeTMVar mvars.

> nosync :: (Num a, Ord a) => [TMVar a] -> STM (a, a) > nosync mvars = do > vals <- mapM takeTMVar mvars > return $ (maximum vals, sum vals)
> initialize :: Int -> a -> (a -> a) -> IO ([ThreadId], [TMVar Int]) > initialize k v f = do > mvars <- atomically (forM [1..k] > (\_ -> newEmptyTMVar)) > thds <- forM (zip mvars [1..k]) > (\(ch, n) -> forkIO (oneThread ch 0 v f)) > return (thds, mvars)

nosyncLoop waits for all the threads to place a value into their TMVar, which will happen after one second.

> nosyncLoop :: [TMVar Int] -> IO () > nosyncLoop mvars = do > (best, sum) <- atomically $ nosync mvars > printf "Best steps / second = %d; Sum steps / second = %d\n" best sum > hFlush stdout > nosyncLoop mvars

A computational time-waster to simulate "real work".

> computation l = let (v:l') = l > in fact v `seq` l' > > fact n = product [1..n]
> main :: IO () > main = do > args <- getArgs > let n = case args of > [] -> 10 > a:_ -> read a > g <- newStdGen > (_,mvars) <- initialize n (randomRs (500,600) g) computation > nosyncLoop mvars

System is a 4-way Xeon 3.6GHz.


[mrd@system ~]$ ghc --make -O2 -threaded Unsync.lhs

[mrd@system ~]$ ./Unsync 1 +RTS -N1 Best steps / second = 3179; Sum steps / second = 3179 Best steps / second = 3181; Sum steps / second = 3181 Best steps / second = 3178; Sum steps / second = 3178 Best steps / second = 3175; Sum steps / second = 3175 Best steps / second = 3174; Sum steps / second = 3174 [mrd@system ~]$ ./Unsync 1 +RTS -N2 Best steps / second = 3142; Sum steps / second = 3142 Best steps / second = 3168; Sum steps / second = 3168 Best steps / second = 3174; Sum steps / second = 3174 Best steps / second = 3177; Sum steps / second = 3177 Best steps / second = 3172; Sum steps / second = 3172

[mrd@system ~]$ ./Unsync 5 +RTS -N1 Best steps / second = 635; Sum steps / second = 3071 Best steps / second = 638; Sum steps / second = 3094 Best steps / second = 668; Sum steps / second = 3080 Best steps / second = 669; Sum steps / second = 3184 Best steps / second = 751; Sum steps / second = 3181 [mrd@system ~]$ ./Unsync 5 +RTS -N2 Best steps / second = 1429; Sum steps / second = 5601 Best steps / second = 1434; Sum steps / second = 5647 Best steps / second = 1446; Sum steps / second = 5647 Best steps / second = 1413; Sum steps / second = 5647 Best steps / second = 1502; Sum steps / second = 5639 [mrd@system ~]$ ./Unsync 5 +RTS -N3 Best steps / second = 1912; Sum steps / second = 5792 Best steps / second = 2092; Sum steps / second = 5934 Best steps / second = 2107; Sum steps / second = 5938 Best steps / second = 1959; Sum steps / second = 5922 Best steps / second = 2068; Sum steps / second = 5960 [mrd@system ~]$ ./Unsync 5 +RTS -N4 Best steps / second = 1876; Sum steps / second = 7428 Best steps / second = 1865; Sum steps / second = 7402 Best steps / second = 1891; Sum steps / second = 7420 Best steps / second = 1895; Sum steps / second = 7581 Best steps / second = 1899; Sum steps / second = 7602

[mrd@system ~]$ ./Unsync 10 +RTS -N1 Best steps / second = 334; Sum steps / second = 2852 Best steps / second = 332; Sum steps / second = 3100 Best steps / second = 334; Sum steps / second = 3082 Best steps / second = 335; Sum steps / second = 3176 Best steps / second = 335; Sum steps / second = 3186 [mrd@system ~]$ ./Unsync 10 +RTS -N2 Best steps / second = 594; Sum steps / second = 5577 Best steps / second = 669; Sum steps / second = 5631 Best steps / second = 588; Sum steps / second = 5641 Best steps / second = 622; Sum steps / second = 5657 Best steps / second = 604; Sum steps / second = 5639 [mrd@system ~]$ ./Unsync 10 +RTS -N3 Best steps / second = 702; Sum steps / second = 5846 Best steps / second = 692; Sum steps / second = 5865 Best steps / second = 717; Sum steps / second = 5884 Best steps / second = 679; Sum steps / second = 5893 Best steps / second = 745; Sum steps / second = 5913 [mrd@system ~]$ ./Unsync 10 +RTS -N4 Best steps / second = 949; Sum steps / second = 7133 Best steps / second = 958; Sum steps / second = 7198 Best steps / second = 989; Sum steps / second = 7189 Best steps / second = 906; Sum steps / second = 7155 Best steps / second = 964; Sum steps / second = 7181

Observations

Number of steps is proportional to number of processors, and inversely proportional to number of threads.

Synchronized threads, part I

Submitted by mrd on Wed, 01/03/2007 - 8:51pm.

I'm performing a small experiment with synchronization of threads: each thread is in a loop performing a "step" each time; the overall idea is to synchronize all threads such that each performs in parallel lock-step.

In this example, the threads are spawned by forkIO, and the synchronization is maintained with the use of the Software Transactional Memory library for MVars.


> import Control.Monad > import Control.Concurrent > import Control.Concurrent.STM > import Data.List > import System.Time > import System.Environment > import System.IO > import System.Random > import Text.Printf > import Ratio

oneThread executes the steps of one thread while remaining in synchronization with the rest. putTMVar will block until the TMVar is empty. Executes a supplied function inside of the synchronization logic, for every step.

> oneThread :: TMVar Int -> Int -> a -> (a -> a) -> IO () > oneThread syncv n v f = do > atomically $ putTMVar syncv n > let v' = f v > v' `seq` oneThread syncv (n + 1) v' f

sync performs one step of synchronization ensuring that all the threads are working on the same step number. Note that this function is written in the STM monad. It is meant to execute as one atomic block. That means it will block until all TMVars are filled by their threads. It won't stop other threads from running and filling in their TMVars, and it won't touch any of the TMVars until all of them are ready.

STM makes writing this a complete breeze. No worries about strange locking issues, it just does the right thing. The key portion is dead simple: mapM takeTMVar vars. It's functional, it's reusing monadic combinators, and it's easy.

> sync :: (Eq a) => [TMVar a] -> a -> STM Bool > sync vars n = do > vals <- mapM takeTMVar vars > return $ all (==n) vals

Initialize k threads each with a TMVar for synchronization.

> initialize :: Int -> a -> (a -> a) -> IO ([ThreadId], [TMVar Int]) > initialize k v f = do > vars <- atomically (forM [1..k] > (\_ -> newEmptyTMVar)) > thds <- forM vars > (\var -> forkIO (oneThread var 0 v f)) > return (thds, vars)

simpleSyncLoop only terminates if the threads ever become unsynchronized.

> simpleSyncLoop vars n = do > ok <- atomically $ sync vars n > if ok then do > printf "Synchronized at step = %d\n" n > simpleSyncLoop vars $ n + 1 > else > printf "Unsynchronized at step = %d\n" n

A computational time-waster to simulate "real work".

Pops a value off the random list and takes the factorial of it.

> computation l = let (v:l') = l > in fact v `seq` l' > > fact n = product [1..n]

A simple main function which starts 10 threads and runs the test forever. The computation is initialized with an infinite list of random numbers between 500 and 600.

> simpleMain = do > g <- newStdGen > (_,vars) <- initialize 10 (randomRs (500,600) g) computation > simpleSyncLoop vars 0

timingSyncLoop attempts to count the number of steps taken per second.

(Note: using the TOD (time-of-day) constructor directly like this is a GHC-specific extension)

> timingSyncLoop vars n = do > -- TOD seconds picoseconds > TOD s ps <- getClockTime > loop (fromIntegral s + ps%(10^12)) n n > where > noThds = length vars > loop prevTime prevN n = do > TOD s ps <- getClockTime > let now = fromIntegral s + ps%(10^12) > tdiff = now - prevTime > ndiff = fromIntegral $ n - prevN > sps = floor (ndiff / tdiff) :: Int > if tdiff >= 1 then > do printf "Steps / sec each: %d; Steps / sec total: %d\n" sps (sps * noThds) > hFlush stdout > loop now n n > else > do ok <- atomically $ sync vars n > if ok then do > loop prevTime prevN $ n + 1 > else > printf "Unsynchronized at step = %d\n" n

Examines the first command line argument to determine how many threads to create, defaulting with 10. Initializes the threads and runs the timingSyncLoop indefinitely.

> timingWithArgMain = do > args <- getArgs > let n = case args of > [] -> 10 > a:_ -> read a > g <- newStdGen > (_,vars) <- initialize n (randomRs (500,600) g) computation > timingSyncLoop vars 0
> main :: IO () > main = timingWithArgMain

System is a 4-way Xeon 3.6GHz.


[mrd@system ~]$ ghc --make -O2 -threaded Sync.lhs

[mrd@system ~]$ ./Sync 1 +RTS -N1 Steps / sec each: 2978; Steps / sec total: 2978 Steps / sec each: 2974; Steps / sec total: 2974 Steps / sec each: 2968; Steps / sec total: 2968 Steps / sec each: 2953; Steps / sec total: 2953 Steps / sec each: 2939; Steps / sec total: 2939 [mrd@system ~]$ ./Sync 1 +RTS -N2 Steps / sec each: 3301; Steps / sec total: 3301 Steps / sec each: 3297; Steps / sec total: 3297 Steps / sec each: 3279; Steps / sec total: 3279 Steps / sec each: 3286; Steps / sec total: 3286 Steps / sec each: 3254; Steps / sec total: 3254 [mrd@system ~]$ ./Sync 1 +RTS -N3 Steps / sec each: 3332; Steps / sec total: 3332 Steps / sec each: 3311; Steps / sec total: 3311 Steps / sec each: 3409; Steps / sec total: 3409 Steps / sec each: 3492; Steps / sec total: 3492 Steps / sec each: 3456; Steps / sec total: 3456 [mrd@system ~]$ ./Sync 1 +RTS -N4 Steps / sec each: 3374; Steps / sec total: 3374 Steps / sec each: 3515; Steps / sec total: 3515 Steps / sec each: 3471; Steps / sec total: 3471 Steps / sec each: 3452; Steps / sec total: 3452 Steps / sec each: 3418; Steps / sec total: 3418

[mrd@system ~]$ ./Sync 5 +RTS -N1 Steps / sec each: 659; Steps / sec total: 3295 Steps / sec each: 649; Steps / sec total: 3245 Steps / sec each: 655; Steps / sec total: 3275 Steps / sec each: 649; Steps / sec total: 3245 Steps / sec each: 653; Steps / sec total: 3265 [mrd@system ~]$ ./Sync 5 +RTS -N2 Steps / sec each: 947; Steps / sec total: 4735 Steps / sec each: 813; Steps / sec total: 4065 Steps / sec each: 874; Steps / sec total: 4370 Steps / sec each: 901; Steps / sec total: 4505 Steps / sec each: 803; Steps / sec total: 4015 [mrd@system ~]$ ./Sync 5 +RTS -N3 Steps / sec each: 1114; Steps / sec total: 5570 Steps / sec each: 914; Steps / sec total: 4570 Steps / sec each: 993; Steps / sec total: 4965 Steps / sec each: 1020; Steps / sec total: 5100 Steps / sec each: 983; Steps / sec total: 4915 [mrd@system ~]$ ./Sync 5 +RTS -N4 Steps / sec each: 994; Steps / sec total: 4970 Steps / sec each: 833; Steps / sec total: 4165 Steps / sec each: 899; Steps / sec total: 4495 Steps / sec each: 787; Steps / sec total: 3935 Steps / sec each: 878; Steps / sec total: 4390

[mrd@system ~]$ ./Sync 10 +RTS -N1 Steps / sec each: 286; Steps / sec total: 2860 Steps / sec each: 316; Steps / sec total: 3160 Steps / sec each: 314; Steps / sec total: 3140 Steps / sec each: 313; Steps / sec total: 3130 Steps / sec each: 302; Steps / sec total: 3020 Sync: interrupted [mrd@system ~]$ ./Sync 10 +RTS -N2 Steps / sec each: 563; Steps / sec total: 5630 Steps / sec each: 557; Steps / sec total: 5570 Steps / sec each: 562; Steps / sec total: 5620 Steps / sec each: 558; Steps / sec total: 5580 Steps / sec each: 563; Steps / sec total: 5630 [mrd@system ~]$ ./Sync 10 +RTS -N3 Steps / sec each: 568; Steps / sec total: 5680 Steps / sec each: 562; Steps / sec total: 5620 Steps / sec each: 561; Steps / sec total: 5610 Steps / sec each: 567; Steps / sec total: 5670 Steps / sec each: 550; Steps / sec total: 5500 [mrd@system ~]$ ./Sync 10 +RTS -N4 Steps / sec each: 555; Steps / sec total: 5550 Steps / sec each: 516; Steps / sec total: 5160 Steps / sec each: 436; Steps / sec total: 4360 Steps / sec each: 514; Steps / sec total: 5140 Steps / sec each: 488; Steps / sec total: 4880


When perfect all-encompassing systems get the rug pulled out from under them...

Submitted by metaperl on Sun, 07/16/2006 - 1:31pm.

So I'm here at home, pissed. I really want to crank out a website, but dont want to be limited to generating HTML. Some website generators produce PDF files. And some allow for adding validation. And some allow for tagging of document parts so that you can re-navigate the documented based on some combination of tags. And unfortunately, the perfect document system was written before the web came out: LaTeX.

So LaTeX's idea of device independant did not include the web device. And that excellent system of document references, BibTeX did not include any concept of hypertext media types.

Sigh.

And now we get to Haskell. Is it the perfect language for building websites automatically? If so, then why is this site done in Drupal instead of in Haskell?

Sluggishness

Submitted by itkovian on Thu, 07/13/2006 - 2:24am.

I've been struggling with the following issue for over three weeks. At this point, it seems like there's nothing I can improve to make certain the application runs faster or allocates memory bounded by O(n), n being the size of the file I'm processing.

The goal is to construct a tree structure from the data contained in a file. Each line in said file indicates an entry or exitpoint of a function that was called (the file contains an execution trace of a Java app). When processing an entry point, the relevant data is stored in a Method record (annotated with a pre (count) number) and the lot is pushed onto a stack. When an exit point is encoutered, the top of the stack is checked. If the functions match, the stack is popped, the Method is annotated with a post (count) number, and we store the annotated Method record in a queue. The queue then contains all the information needed to contruct a real Tree, using the pre and post numbers.

And additional complication is the fact that each file line also belongs to an execution thread, which is located in the line. We need to construct a tree for each thread. For this we use a Data.Map that maps the thread in (:: Int) to the relevant stack and queue.

Finally, we also have a mapping fro function ids to function names, also maintained in a Data.Map

I am using a State Monad with the state contained in a ParserState record. Each line with update the state via updateState, where I make a distinction between the possible kinds of line in the trace, by swithcing on the first field of each line. Fields are separated by a space. I'm using the Data.ByteString stuff to lazily read the file.

I've tried to get Haskell to evaluate each update to the State through succintly using the seq operator. Perhaps I overdid that.

The question remains where and how I need to change my code to

  • Make things faster
  • Use less memory.

A profiling run (after -O2) showing retained sets seem to indicate super-linear behaviour in retaining data.

All comments are appreciated.

I'm pasting the Main module contents here.


import Debug.Trace
import System.Environment
import System.IO
import Data.Map as M
import Data.Maybe
import Data.List (sortBy)
import Control.Monad.State

import qualified Data.ByteString.Lazy.Char8 as B


import Method
import Tree
import Algorithms

type Preorder  = Integer
type Postorder = Integer
type MethodMap = M.Map Integer B.ByteString
type ThreadMap = M.Map Integer [(Preorder, Postorder, Method)]


data ParserState = ParserState { methodStack :: !ThreadMap
                               , methodQueue :: !ThreadMap
                               , pre         :: !Integer
                               , post        :: !Integer
                               , methodMap   :: !MethodMap
                               , currentThread :: !Integer
                               } deriving (Show)

initialParserState :: ParserState
initialParserState = ParserState e e 0 0 e 0
  where e = M.empty :: Map Integer a

readInteger :: B.ByteString -> Integer
readInteger = fromIntegral . fst . fromJust . B.readInt


parseTraceMonadic :: [B.ByteString] -> ParserState
parseTraceMonadic ss = state { methodQueue = M.map reverse (methodQueue state) }
  where state = execState (mapM_ (\x -> modify (updateState x) ) ss) initialParserState
  {- I've pushed this through a >> get >>= (`seq` return()) too -} 

updateState :: B.ByteString -> ParserState -> ParserState
updateState s state = case (B.unpack $ head fields) of
  "M" -> updateStateMethod     fields state
  "E" -> updateStateException  fields state
  "C" -> updateStateEntry      fields state
  "R" -> updateStateExit       fields state
  where fields = B.splitWith (== ' ') s
  

updateStateMethod :: [B.ByteString] -> ParserState -> ParserState
updateStateMethod (_:methodId:methodName:_) state = 
  let methodMap' = M.insert (readInteger methodId) methodName (methodMap state)
  in methodMap' `seq` state { methodMap = methodMap' }

updateStateException :: [B.ByteString] -> ParserState -> ParserState
updateStateException _ state = state

updateStateEntry :: [B.ByteString] -> ParserState -> ParserState
updateStateEntry (_:ss) state = 
  let methodStack' = updateMap thread (methodStack state) (\x y -> Just (x:y)) (pre state, 0, method)
  in let pre' = ((+1) $! (pre state))
  in methodAtack' `seq` pre' `seq`
  state { methodStack = methodStack'
        , pre = pre' }
  where method = mkMethod (Prelude.map B.unpack ss)
        thread = Method.thread method

updateStateExit :: [B.ByteString] -> ParserState -> ParserState
updateStateExit (_:ss) state = 
  case updateMethod m (Prelude.map B.unpack ss) of
     Just um -> let methodStack' = updateMap thread 
                                   (methodStack state) 
                                   (\x y -> Just (tail y)) 
                                   (pre_, post state, um)
                in let methodQueue' = updateMap thread 
                                      (methodQueue state) 
                                      (\x y -> Just (x:y)) 
                                      (pre_, post state, um)
                in let post' = ((+1) $! (post state))
                in methodStack' `seq` methodQueue' `seq` post' `seq`
                state { methodStack = methodStack'
                      , methodQueue = methodQueue'
                      , post = post' }
     Nothing -> error $    "Top of the stack is mismatching! Expected " 
                        ++ (show m) ++ " yet got " ++ (show ss) 
                        ++ "\n" ++ (show state)
  where method = mkMethod (Prelude.map B.unpack ss)
        thread = Method.thread method    
        (pre_, _, m) = let x = M.lookup thread (methodStack state) 
                       in x `seq` case x of
                          Just stack -> head stack
                          Nothing    -> error $    "Method stack has not been found for thread " 
                                                ++ (show thread) ++ " -> fields: " ++ (show ss)
        

updateMap key map f value = case M.member key map of
                              True  -> M.update (f value) key map
                              False -> M.insert key [value] map


main = do
          [filename] <- System.Environment.getArgs
          file       <- System.IO.openFile filename System.IO.ReadMode
          contents   <- B.hGetContents file
          let parserState = parseTraceMonadic . B.lines $ contents
          print (methodQueue parserState)
          print (methodStack parserState)
          print (methodMap parserState)
          print (pre parserState)
          print (post parserState)

I think taking a peek at the Method module can;t hurt either, so:


data Method = Method { mid :: Integer
                     , thread :: Integer
                     , instruction_entry :: Integer
                     , instruction_exit :: Integer
                     } deriving (Eq, Show)

eM = Method 0 0 0 0

mkMethod :: [String] -> Method
mkMethod s = let [_thread, _id, _entry] = take 3 $ map (read :: String -> Integer) s 
             in [_thread, _id, _entry] `seq` Method { mid = _id
                                                    , thread = _thread
                                                    , instruction_entry = _entry
                                                    , instruction_exit = 0
                                                    }

updateMethod :: Method -> [String] -> Maybe Method
updateMethod (Method mid thread instruction_entry instruction_exit ) s
  | thread == _thread && mid == _id = _exit `seq` Just Method { mid = mid
                                                              , thread = thread
                                                              , instruction_entry = instruction_entry
                                                              , instruction_exit = _exit
                                                              }
  | otherwise = Nothing
  where [_thread, _id, _exit] = take 3 $ map (read :: String -> Integer) s

Haskell on Pocket PC?

Submitted by dokondr on Thu, 03/30/2006 - 6:37am.

Any ideas on how much work needs to be done for using Haskell on PPC Windows Mobile platform?
It would be interesting to use PPC as:
1) Haskell learning tool, so small code snipets could be entered and run directly on hand-held (REPL). How hard is it to port Hugs to PPC for this? Do any other (then Hugs) implementations exist that are easier to port?
2) Running on PPC Haskell applications cross-compiled on host PC. How much work must be done for GHC to support this?

3) There are several ways both for porting Haskell to PPC as well as cross-compiling Haskell code. Which one makes more sense to implement and will take less effort:
a) Porting/compiling to VM byte code (Java, Parrot)?
b) Porting/compiling to .NET CLR?

4) And finally, do any projects already exist in this area?

Newbie: Recursive lambda definitions?

Submitted by dokondr on Sat, 03/18/2006 - 1:04pm.

{-
Haskell newbie: Recursive lambda definitions?
Simon Thompson gives the following exercise (10.9) in his "Haskell. The Craft of Functional Programming" book:

10.9 Define a function total

total:: (Int -> Int) -> (Int -> Int)

so that total f is the function which at value n gives the total

f 0 + f 1 + ... + f n

I use 'where' clause to describe the resulting function 'tot':
-}

total:: (Int -> Int) -> (Int -> Int)
total f = tot 
    where
    tot n
	| n >= 0 = (f n) + (tot (n-1))
	| otherwise = 0

test = total f1 4

{-
Q: Is it possible instead of naming and defining a resulting function (such as 'tot' in this example) just use recursive lambda definition? In this example recursion is required to create a function which is a variable sum of another function applications like:

f 0 + f 1 + ... + f n

Giving function a name ('tot' in this case) makes recursive definition possible. But what about lambda recursion? Can it be defined?
-}