Discussion
Coq and The Monad Laws: Introduction
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.
- mrd's blog
- Login to post comments
Haskell and XML
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.
- mrd's blog
- Login to post comments
Chess in Haskell
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!
- chessguy's blog
- Login to post comments
Dynamic Programming in Haskell
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
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.
- mrd's blog
- Login to post comments
Synchronized threads, part I
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
- mrd's blog
- Login to post comments
When perfect all-encompassing systems get the rug pulled out from under them...
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
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?
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?
{-
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?
-}