Planet Haskell

February 20, 2009

Alex Mason

AVar released (three times)

The other day, I put my AVar package on hackage. Doing so taught me more than i expected it would, mainly that i need to do more testing of cabal packages before submitting them, and also to make sure you've exported all the functions you need to actually use the package (I forgot to put putAVar in the module exports -_-). So i'm up to release 0.0.3, without much work being done at all (although, I can't think of much more to do really).

With the current release, i think that all exceptions that may occur from functions passed by the user to the variable should be caught by and handled correctly by the variable. I guess in a sense, AVars are smart variables that know what is and isn't good for them, and will refuse to hurt themselves (hopefully!).

If you're interested in seeing what AVar can do, check out the Hackage page. I really have no idea how it might be useful, but I'd love to hear others thoughts on it.

If you have any requests, please let me know, and I'll see what I can do (proper transactional ... transactions are not something I want to tackle, especially with uni starting on monday)

by Alex Mason at February 20, 2009 08:57 AM

February 19, 2009

Sean Leather

The strict danger of switching from pure to monadic Template Haskell

Due to several issues with the Template Haskell (TH) deriving in EMGM (which I knew were there, but needed significant motivation to fix), I realized it was time to convert much of my code from pure to monadic. From the beginning, I developed it to be as non-monadic (i.e. not in Q) as possible for all the reasons one is supposed to. This led to several challenges that were not too difficult to surmount at the time. Namely, reify and newName had to be used at the top level of my function hierarchy, and their values had be passed down. But now I really need reify in a few places in the depths of the code, and it is quite impractical to do otherwise. For example, I need to expand type synonyms, and if I do that at the top level, every name is now either a name or some adaptation of a type declaration.

Most of the refactoring was surprisingly easy. I simply changed uppercase constructors to their lowercase, monadic equivalents (see the docs for the difference). However, I ran into a problem in which a function specific to bifunctor types was getting applied to monomorphic types. This lead to strange errors (compile-time of course, since it's TH) that told me something had changed in the way the functions were used. It was very likely not the programming logic itself, because I was carefully migrating individual functions a few at a time and testing as I went. But somehow, once I reached the point in the code where I needed reify, I started getting these error reports (my code, though it was for unexpected inputs).

After several hours of tracing through with report, I found the problem. Here is the blah-ified (and simplified) original code:

-- Non-monadic:
blah :: ... -> ...
blah ... = ...

-- Monadic wrapper
blahM :: ... -> Q [...]
blahM ... = return [blah ...]

-- Exposed
fun :: ... -> Q ...
fun ... = do
  a - ...
  b - blahM ...
  let x =
        case ... of
          1 -> a
          2 -> b
          _ -> []
  return (... ++ x)

Most of the logic lies under blah, so it follows that I monadicized (monadified?) blah which required a minor changed to blahM:

blah :: ... -> Q ...
blah ... = ...

blahM :: ... -> Q [...]
blahM ... = do
  x - blah ...
  return [x]

Now, this didn't affect anything immediately. I kept converting my functions to the monadic religion, and at some point, I suppose I evangelized too much. Then, I believe that blah, which by the original design was meant to be called lazily, became too strict. It was getting called every time, instead of only when the case expression matched on 2. Once I realized this, it was evident that I needed to change fun.

fun :: ... -> Q ...
fun ... = do
  x -
    case ... of
      1 -> ...
      2 -> blahM ...
      _ -> return []
  return (... ++ x)

Now, everything is strictly normal again. No strange errors to keep me up at night. I believe now that blahM was always getting evaluated even though blah was not. So, as I pushed the monad down into the code, more and more things were getting strictly evaluated.

I keep learning that I don't understand laziness as well as I think I do. Or maybe it's that I don't understand strictness. Or perhaps I'm too lazy to strictly learn both.

I also resolve never to write non-monadic Template Haske11 code again (excluding small and/or simple functions, of course). The amount of work required is not worth the benefits gained.

by Sean Leather (noreply@blogger.com) at February 19, 2009 11:00 PM

Mads Lindstrøm

Using Mutable Arrays for Faster Sorting


Various people have tried improving the Data.List.sort function in Haskell, see Data.List.sort, not so good? and Sorting At Speed. In this post, I will also attempt improving sort performance. I will use a simple algorithm:

Mergesort with Mutable Arrays

Mergesort with Mutable Arrays

Below we will see why converting a linked list to an array improves sorting performance.

Linked lists versus mutable arrays

I have depicted a linked list graphically below. Data constructors are shown as boxes, pointers as arrows, and elements as ellipses. As seen we need two pointers for each element. As Haskell’s linked lists are immutable we must recreate the list if we want to change one or more elements.

A Singly Linked List

A Singly Linked List

A Haskell mutable array is depicted below. We only use one pointer per element and the lookup operation and the update operation are both O(1).

An Array

An Array

Mergesort

Mergesort for immutable linked lists reallocates (recreates) a new list for each traversal. That is, it recreates the list for each time it has visited all elements once. There are log(n) traversals. All these memory allocations and latter cleanups by the garbage collector takes time. See Sorting At Speed for GHC’s implementation of mergesort.

Mergesort, using mutable arrays, do not need to recreate the list for each traversal. It uses two list operations, update and lookup, which are both O(1). Like mergesort for immutable linked lists, mergesort for mutable arrays still needs to traverse the list log(n) times.

The use of one pointer per element and no need to reallocate the list for each traversal, makes it seem likely that converting a linked list to a mutable array, sorting and converting back again, may be faster than sorting a linked list directly.

Benchmarks

Up until now it has all been theory and I will need to do measurements to back up the claim, that we can sort faster by converting to a mutable array. I do not know all the idiosyncrasies of modern hardware or which optimizations GHC may or may not do. There may be GHC optimizations, which makes immutable linked lists a lot faster than I imagine.

I have therefore implemented a mergesort using mutable arrays. I have used this program to benchmark my implementation. The program was compiled with GHC 6.10.1 using the optimization flag -O2. And I ran the benchmark program as: “./Benchmark +RTS -K32388608 -RTS >/dev/null”. I have tested both with lists of Ints and list of strings.

The benchmark program calls System.Mem.performGC before and after sorting. The last call to System.Mem.performGC is measured as part of the sorting. In this way I am internalizing the cost of garbage collection into the sort function. I use this in stead of measuring memory use directly. The the first call is done, so that we start with a clean sheet before each measurement.

Int sort results
Iterations Number of elements Data.List.sort (ms) Array sort (ms) Speedup (%)
25000 10 264 272 -4
50000 10 684 572 16
100000 10 2396 2216 7
25000 20 1136 1056 7
10000 40 916 808 11
10000 50 1184 1016 14
10000 75 1872 1548 17
5000 100 1288 1048 18
5000 200 2912 2420 16
2000 400 2492 2024 18
2000 600 4000 3184 20
2000 800 5624 4276 23
1000 1000 3656 2744 24
20 10000 2276 1592 30
5 100000 8844 4260 51
2 1000000 62559 24677 60
String sort results

Iterations Number of elements Data.List.sort (ms) Array sort (ms) Speedup (%) 10000 10 304 312 -3 20000 10 604 624 -4 40000 10 1216 1252 -3 10000 20 524 504 3 5000 50 632 544 13 5000 100 1320 1072 18 2000 200 1156 980 15 1000 400 1236 1008 18 750 600 1504 1184 21 500 800 1404 1080 23 500 1000 1828 1404 23 10 10000 992 716 27 5 100000 8860 4296 51

As can be seen, the speedups for large lists are quite good, but not for small lists. The speedup is even slighty negative for some small lists. That the benefits are better for large lists is not surprising, when considering that the cost of converting to and from arrays is O(n), whereas the gains are O(n * log(n)).

Sorting Ints shows better speedup than sorting strings. I speculate, that this is due to strings being more expensive to compare than Ints. As both Data.List.sort and my own sorting algorithm uses the same number of comparisons, the actual compare operations are equally expensive for both algorithms. When a constant part, the compare operations, is larger, then the (percentage) speedup gets smaller.

Taking the beauty out of functional programming?

Some might argue that using mutable arrays removes the beauty from functional programming - and they would be right. I do not see a problem though, as the nasty mutable code can be hidden behind a nice functional interface. Furthermore, a sorting algorithm only needs to be implemented once, but can be used man times.

Future Improvements

Although my sorting algorithm is, in most cases, faster than the stock GHC one, there is still room for improvement.

As shown, we are converting a linked list to an array, and back to a linked list again. As we are converting to an array, we might as well convert to an array of unboxed types in stead. Using unboxed types would avoid one pointer per element. Initial experiments shows significant speedups, as compared to my current sorting algorithm. Of cause, this only works for types which can be unboxed, which fortunately includes popular types such as Int, Double and Float. Using rewrite rules we can even hide the choice of using unboxed types from the user of the sorting algorithm.

Haskell has other types of arrays, such as Parallel arrays (module GHC.PArr) which is claimed to be fast. Choosing another array implementations may improve sorting performance.

Lastly, as Don Stewart explains in his blogpost “A Journal of Haskell Programming Write Haskell as fast as C: exploiting strictness, laziness and recursion” we may use GHC core to gain better performance.

by Mads Lindstrøm at February 19, 2009 10:57 PM

Xmonad

Why tiling? Why xmonad?


A great post on the why you would want to use xmonad from Jesse Andrews: Getting Tiled with XMonad. A choice quote:

XMonad has defeated all other desktop environments

Enjoy!

by dons00 at February 19, 2009 05:45 AM

Conal Elliott

Denotational design with type class morphisms

I’ve just finished a draft of a paper called Denotational design with type class morphisms, for submission to ICFP 2009. The paper is on a theme I’ve explored in several posts, which is semantics-based design, guided by type class morphisms.

I’d love to get some readings and feedback. Pointers to related work would be particularly appreciated, as well as what’s unclear and what could be cut. It’s an entire page over the limit, so I’ll have to do some trimming before submitting.

The abstract:

Type classes provide a mechanism for varied implementations of standard interfaces. Many of these interfaces are founded in mathematical tradition and so have regularity not only of types but also of properties (laws) that must hold. Types and properties give strong guidance to the library implementor, while leaving freedom as well. Some of the remaining freedom is in how the implementation works, and some is in what it accomplishes.

To give additional guidance to the what, without impinging on the how, this paper proposes a principle of type class morphisms (TCMs), which further refines the compositional style of denotational semantics. The TCM idea is simply that the instance’s meaning is the meaning’s instance. This principle determines the meaning of each type class instance, and hence defines correctness of implementation. In some cases, it also provides a systematic guide to implementation, and in some cases, valuable design feedback.

The paper is illustrated with several examples of type, meanings, and morphisms.

You can get the paper and see current errata here.

The submission deadline is March 2, so comments before then are most helpful to me.

Enjoy, and thanks!

by conal at February 19, 2009 02:34 AM

February 18, 2009

happstack.com

SOCALFP Presentation Slides: “Happstack is better than X”


The SOCALFP presentation was a fun! Thank you to all who participated. The rough outline of the talk goes something like:

  • History of HAppS & happstutorial
  • Happstack announcement
  • Patch-Tag partnership announcement
  • Crash course in HAppS/Happstack
  • Comparative analysis of Happstack vs Rails
  • Job outlook of Haskell community in general

The slides are here. The videos are here. There are also pictures here.

by Matthew Elder at February 18, 2009 10:49 PM

Luke Palmer

Dependent types are ridiculously easy


After an inquiry about a combinatory calculus for dependent types, somebody in #haskell — unfortunately I don’t remember who — recommended I look at Illative Combinatory Logic. After studying the paper a bit, all I can say is Wow! It implements a (conjecturally) complete logical system in but three simple typing rules, together with the untyped lambda calculus conversion rules. I was able to write a dependent typechecker in 100 lines.

The specific system I’m working with in the paper is called system IG. The paper also introduces three weaker systems, which are also very nice and worth understanding.

As an example, here is a derivation of the identity function and its type. This is a backward proof, so each step is implied by the step after it. But reading it this way makes the algorithm clear.

    |- G L (\A. G A (\_. A)) (\A x. x)
    L a |- (\A. G A (\_. A)) a ((\A x. x) a)     (Gi)
    L a |- G a (\_. a) ((\A x. x) a)             (beta)
    L a |- G a (\_. a) (\x. x)                   (beta)
    L a, a b |- (\_. a) b ((\x. x) b)            (Gi)
    L a, a b |- a ((\x. x) b)                    (beta)
    L a, a b |- a b                              (beta)

The trick, which isn’t so much a trick as a beautiful deep connection I gather (although I don’t fully grok it), is that typing propositions are just applications. So if A is a type, then A b is the proposition “b has type A”. L is the type of types, and G is essentially Π (the product type constructor). So, for example, the fourth line in the above proof would be written as follows in a conventional system:

    a : Type  |-  (\x. x) : a -> a

I need to extend it with finite types and boxes, but I really don’t want to because it’s so pretty as is! :-)

by Luke at February 18, 2009 10:26 AM

Russell O'Connor

James R Meyer vs Kurt Gödel

James R. Meyer claims to have found an error in Gödel’s proof of the incompleteness theorem. Last June, James gave Henk Barendregt a free copy of his book and invited him to read about the flaw he discovered. Henk regularly gets emails from people claiming to have found errors in the incompleteness theorem. Henk wrote a polite response and mentioned that there are computer checked formal proofs of the incompleteness theorem and included me in the reply in case I might wish to respond.

A formal proof ought to assuage almost all doubts about the validity of a theorem. Essentially, the only ways that an error can occur is if the proof checking software is in error in such a way as to allow invalid proofs, or if the theorem is stated incorrectly.

James seemed like he had the competence necessary to understand the incompleteness theorem. Having formalized the theorem, I have quite a good understanding of the technicalities encountered in the proof. I hoped I could settle any doubts he had about the incompleteness theorem.

I wrote up a review of his paper pointing out several errors he makes. Then we engaged in a moderate email exchange where I would explain something and he would find some reason to dismiss what I had to say.

Eventually it became clear that James is only interested in finding a flaw in Gödel’s original paper. He does not seem to care about whether the theorem is valid or whether there are other proofs of the theorem. Thus, my formal proof does not interest him.

Of course, it much more difficult to argue that Gödel’s original paper is correct. I am not as familiar with Gödel’s original presentation. The original paper uses old notation that is quite different from modern presentations. Also, James chooses to attack Gödel’s proposition V, whose proof is only vaguely sketched in Gödel’s original paper. Let me quote Martin Hirzel.

Gödel’s famous proof is highly interesting, but may be hard to understand. Some of this difficulty is due to the fact that the notation used by Gödel has been largely replaced by other notation. Some of this difficulty is due to the fact that while Gödel’s formulations are concise, they sometimes require the readers to make up their own interpretations for formulae, or to keep definitions in mind that may not seem mnemonic to them.

I gave up arguing with James at this point. Defending’s Gödel’s original argument would require too much work. Furthermore, finding an error in the original proof is uninteresting (from a mathematical perspective). Even if Gödel’s orginal proof contained a minor error, there are plenty of modern (and computer verified) proofs that establish the theorem.

I was recently reminded about James, and I have been thinking him, wondering if he is a hopeless crank or if I might still be able to convince him that he is wrong. A little research turned up the answer to this question.

I found a sci.math thread from last July that discusses James’s argument. The thread is initiated by thirdmerlin@hotmail.com—who is likely a puppet of James himself—and eventually James “joins” in. In particular, MoeBlee correctly picks out the specific errors James makes, and MoeBlee probably does a better job arguing the case than I ever could.

Alas, James remains an inconvincible crank. Despite MoeBlee’s pointing out the flaws in James’s argument, he still claims that no one has found a flaw in his argument. At least James’s website no longer proudly claims that he is the first person to understand (and refute) Gödel’s incompleteness proof.


That’s my story, but what bothers me most was how upset I felt last summer in my inability to convince him of his error. Because of the time zone difference, we could only exchange one round of email per day. Each day I would put forth my best argument I could at the time given my limited understanding of his perspective. Each day I knew that no matter what I said, he would presumably find it insufficient. I would be anxious at about what way he would dismiss my argument. It also upset me a little that he took snippets of my email conversation with him and placed them out-of-context on his web-page (and occasionally completely rewording my statements).

However, I found it a great relief today to read that sci.math thread. Everyone there was saying the same things I said. Tim Chow even brought up my formal proof. I’m not sure why I felt so anxious when emailing him, nor am I entirely sure why I am relieved now.

I think my concern is that someone stumbles upon his website and gets the impression that this guy is on to something and has not received fair criticism. Damage is done by conspiracy theories that deny the moon landing (for example, high school teachers have a hard time countering these claims when they are brought up by students). Actual harm is done by bogus claims that there is a link between MMR vaccines and autism. Simply dismissing these people plays into their argument that they are being ignored, and engaging them is expensive and largely futile.

Granted, no one is going to die if people falsely believe that Gödel’s theorem is wrong, but I still do not know what is a good policy for dealing with cranks.

February 18, 2009 02:50 AM

John Goerzen (CosmicRay)

How To Think About Compression, Part 2

Yesterday, I posted part 1 of how to think about compression. If you haven’t read it already, take a look now, so this post makes sense.

Introduction

In the part 1 test, I compressed a 6GB tar file with various tools. This is a good test if you are writing an entire tar file to disk, or if you are writing to tape.

For part 2, I will be compressing each individual file contained in that tarball individually. This is a good test if you back up to hard disk and want quick access to your files. Quite a few tools take this approach — rdiff-backup, rdup, and backuppc are among them.

We can expect performance to be worse both in terms of size and speed for this test. The compressor tool will be executed once per file, instead of once for the entire group of files. This will magnify any startup costs in the tool. It will also reduce compression ratios, because the tools won’t have as large a data set to draw on to look for redundancy.

To add to that, we have the block size of the filesystem — 4K on most Linux systems. Any file’s actual disk consumption is always rounded up to the next multiple of 4K. So a 5-byte file takes up the same amount of space as a 3000-byte file. (This behavior is not unique to Linux.) If a compressor can’t shrink enough space out of a file to cross at least one 4K barrier, it effectively doesn’t save any disk space. On the other hand, in certain situations, saving one byte of data could free 4K of disk space.

So, for the results below, I use du to calculate disk usage, which reflects the actual amount of space consumed by files on disk.

The Tools

Based on comments in part 1, I added tests for lzop and xz to this iteration. I attempted to test pbzip2, but it would have taken 3 days to complete, so it is not included here — more on that issue below.

The Numbers

Let’s start with the table, using the same metrics as with part 1:

Tool MB saved Space vs. gzip Time vs. gzip Cost
gzip 3081 100.00% 100.00% 0.41
gzip -1 2908 104.84% 82.34% 0.36
gzip -9 3091 99.72% 141.60% 0.58
bzip2 3173 97.44% 201.87% 0.81
bzip2 -1 3126 98.75% 182.22% 0.74
lzma -1 3280 94.44% 163.31% 0.63
lzma -2 3320 93.33% 217.94% 0.83
xz -1 3270 94.73% 176.52% 0.68
xz -2 3309 93.63% 200.05% 0.76
lzop -1 2508 116.01% 77.49% 0.39
lzop -2 2498 116.30% 76.59% 0.39

As before, in the “MB saved” column, higher numbers are better; in all other columns, lower numbers are better. I’m using clock seconds here on a dual-core machine. The cost column is clock seconds per MB saved.

Let’s draw some initial conclusions:

  • lzma -1 continues to be both faster and smaller than bzip2. lzma -2 is still smaller than bzip2, but unlike the test in part 1, is now a bit slower.
  • As you’ll see below, lzop ran as fast as cat. Strangely, lzop -3 produced larger output than lzop -1.
  • gzip -9 is probably not worth it — it saved less than 1% more space and took 42% longer.
  • xz -1 is not as good as lzma -1 in either way, though xz -2 is faster than lzma -2, at the cost of some storage space.
  • Among the tools also considered for part 1, the difference in space and time were both smaller. Across all tools, the difference in time is still far more significant than the difference in space.

The Pretty Charts

Now, let’s look at an illustration of this. As before, the sweet spot is the lower left, and the worst spot is the upper right. First, let’s look at the compression tools themselves:

compress2-zoomed

At the extremely fast, but not as good compression, end is lzop. gzip is still the balanced performer, bzip2 still looks really bad, and lzma -1 is still the best high-compression performer.

Now, let’s throw cat into the mix:

compress2-big

Here’s something notable, that this graph makes crystal clear: lzop was just as fast as cat. In other words, it is likely that lzop was faster than the disk, and using lzop compression would be essentially free in terms of time consumed.

And finally, look at the cost:

compress2-efficiency

What happened to pbzip2?

I tried the parallel bzip2 implementation just like last time, but it ran extremely slow. Interestingly, pbzip2 notes.txt > notes.txt.bz2 took 1.002 wall seconds, but pbzip2 notes.txt finished almost instantaneously. This 1-second startup time for pbzip2 was a killer, and the test would have taken more than 3 days to complete. I killed it early and omitted it from my results. Hopefully this bug can be fixed. I didn’t expect pbzip2 to help much in this test, and perhaps even to see a slight degradation, but not like THAT.

Conclusions

As before, the difference in time was far more significant than the difference in space. By compressing files individually, we lost about 400MB (about 7%) space compared to making a tar file and then combining that. My test set contained 270,101 files.

gzip continues to be a strong all-purpose contender, posting fast compression time and respectable compression ratios. lzop is a very interesting tool, running as fast as cat and yet turning in reasonable compression — though 25% worse than gzip on its default settings. gzip -1 was almost as fast, though, and compressed better. If gzip weren’t fast enough with -6, I’d be likely to try gzip -1 before using lzop, since the gzip format is far more widely supported, and that’s important to me for backups.

These results still look troubling for bzip2. lzma -1 continued to turn in far better times and compression ratios that bzip2. Even bzip2 -1 couldn’t match the speed of lzma -1, and compressed barely better than gzip. I think bzip2 would be hard-pressed to find a comfortable niche anywhere by now.

As before, you can download my spreadsheet with all the numbers behind these charts and the table.

by John Goerzen at February 18, 2009 02:22 AM

February 17, 2009

Mark Jason Dominus

Second-largest cities

A while back I was in the local coffee shop and mentioned that my wife had been born in Rochester, New York. "Ah," said the server. "The third-largest city in New York." Really? I would not have guessed that. (She was right, by the way.) As a native of the first-largest city in New York, the one they named the state after, I have spent very little time thinking about the lesser cities of New York. I have, of course, heard that there are some. But I have hardly any idea what they are called, or where they are.

It appears that the second-largest city in New York state is some place called (get this) "Buffalo". Okay, whatever. But that got me wondering if New York was the state with the greatest disparity between its largest and second-largest city. Since I had the census data lying around from a related project (and a good thing too, since the Census Bureau website moved the file) I decided to find out.

The answer is no. New York state has only one major city, since its next-largest settlement is Buffalo, with 1.1 million people. (Estimated, as of 2006.) But the second-largest city in Illinois is Peoria, which is actually the punchline of jokes. (Not merely because of its small size; compare Dubuque, Iowa, a joke, with Davenport, Iowa, not a joke.) The population of Peoria is around 370,000, less than one twenty-fifth that of Chicago.

But if you want to count weird exceptions, Rhode Island has everyone else beat. You cannot compare the sizes of the largest and second-largest cities in Rhode Island at all. Rhode Island is so small that it has only one city, Seriously. No, stop laughing! Rhode Island is no laughing matter.

The Articles of Confederation required unanimous consent to amend, and Rhode Island kept screwing everyone else up, by withholding consent, so the rest of the states had to junk the Articles in favor of the current United States Constitution. Rhode Island refused to ratify the new Constitution, insisting to the very end that the other states had no right to secede from the Confederation, until well after all of the other twelve had done it, and they finally realized that the future of their teeny one-state Confederation as an enclave of the United States of America was rather iffy. Even then, their vote to join the United States went 34–32.

But I digress.

Actually, for many years I have said that you can impress a Rhode Islander by asking where they live, and then—regardless of what they say—remarking "Oh, that's near Providence, isn't it?" They are always pleased. "Yes, that's right!" The census data proves that this is guaranteed to work. (Unless they live in Providence, of course.)

Here's a joke for mathematicians. Q: What is Rhode Island? A: The topological closure of Providence.

Okay, I am finally done ragging on Rhode Island.

Here is the complete data, ordered by size disparity. I wasn't sure whether to put Rhode Island at the top or the bottom, so I listed it twice, just like in the Senate.


State Largest city and
its Population
Second-largest city
and its population
Quotient
Rhode Island Providence-New Bedford-Fall River 1,612,989
Illinois Chicago-Naperville-Joliet 9,505,748 Peoria 370,194 25.68
New York New York-Northern New Jersey-Long Island 18,818,536 Buffalo-Niagara Falls 1,137,520 16.54
Minnesota Minneapolis-St. Paul-Bloomington 3,175,041 Duluth 274,244 11.58
Maryland Baltimore-Towson 2,658,405 Hagerstown-Martinsburg 257,619 10.32
Georgia Atlanta-Sandy Springs-Marietta 5,138,223 Augusta-Richmond County 523,249 9.82
Washington Seattle-Tacoma-Bellevue 3,263,497 Spokane 446,706 7.31
Michigan Detroit-Warren-Livonia 4,468,966 Grand Rapids-Wyoming 774,084 5.77
Massachusetts Boston-Cambridge-Quincy 4,455,217 Worcester 784,992 5.68
Oregon Portland-Vancouver-Beaverton 2,137,565 Salem 384,600 5.56
Hawaii Honolulu 909,863 Hilo 171,191 5.31
Nevada Las Vegas-Paradise 1,777,539 Reno-Sparks 400,560 4.44
Idaho Boise City-Nampa 567,640 Coeur d'Alene 131,507 4.32
Arizona Phoenix-Mesa-Scottsdale 4,039,182 Tucson 946,362 4.27
New Mexico Albuquerque 816,811 Las Cruces 193,888 4.21
Alaska Anchorage 359,180 Fairbanks 86,754 4.14
Indiana Indianapolis-Carmel 1,666,032 Fort Wayne 408,071 4.08
Colorado Denver-Aurora 2,408,750 Colorado Springs 599,127 4.02
Maine Portland-South Portland-Biddeford 513,667 Bangor 147,180 3.49
Vermont Burlington-South Burlington 206,007 Rutland 63,641 3.24
California Los Angeles-Long Beach-Santa Ana 12,950,129 San Francisco-Oakland-Fremont 4,180,027 3.10
Nebraska Omaha-Council Bluffs 822,549 Lincoln 283,970 2.90
Kentucky Louisville-Jefferson County 1,222,216 Lexington-Fayette 436,684 2.80
Wisconsin Milwaukee-Waukesha-West Allis 1,509,981 Madison 543,022 2.78
Alabama Birmingham-Hoover 1,100,019 Mobile 404,157 2.72
Kansas Wichita 592,126 Topeka 228,894 2.59
Pennsylvania Philadelphia-Camden-Wilmington 5,826,742 Pittsburgh 2,370,776 2.46
New Hampshire Manchester-Nashua 402,789 Lebanon 172,429 2.34
Mississippi Jackson 529,456 Gulfport-Biloxi 227,904 2.32
Utah Salt Lake City 1,067,722 Ogden-Clearfield 497,640 2.15
Florida Miami-Fort Lauderdale-Miami Beach 5,463,857 Tampa-St. Petersburg-Clearwater 2,697,731 2.03
North Dakota Fargo 187,001 Bismarck 101,138 1.85
South Dakota Sioux Falls 212,911 Rapid City 118,763 1.79
North Carolina Charlotte-Gastonia-Concord 1,583,016 Raleigh-Cary 994,551 1.59
Arkansas Little Rock-North Little Rock 652,834 Fayetteville-Springdale-Rogers 420,876 1.55
Montana Billings 148,116 Missoula 101,417 1.46
Missouri St. Louis 2,796,368 Kansas City 1,967,405 1.42
Iowa Des Moines-West Des Moines 534,230 Davenport-Moline-Rock Island 377,291 1.42
Virginia Virginia Beach-Norfolk-Newport News 1,649,457 Richmond 1,194,008 1.38
New Jersey Trenton-Ewing 367,605 Atlantic City 271,620 1.35
Louisiana New Orleans-Metairie-Kenner 1,024,678 Baton Rouge 766,514 1.34
Connecticut Hartford-West Hartford-East Hartford 1,188,841 Bridgeport-Stamford-Norwalk 900,440 1.32
Oklahoma Oklahoma City 1,172,339 Tulsa 897,752 1.31
Delaware Seaford 180,288 Dover 147,601 1.22
Wyoming Cheyenne 85,384 Casper 70,401 1.21
South Carolina Columbia 703,771 Charleston-North Charleston 603,178 1.17
Tennessee Nashville-Davidson--Murfreesboro 1,455,097 Memphis 1,274,704 1.14
Texas Dallas-Fort Worth-Arlington 6,003,967 Houston-Sugar Land-Baytown 5,539,949 1.08
West Virginia Charleston 305,526 Huntington-Ashland 285,475 1.07
Ohio Cleveland-Elyria-Mentor 2,114,155 Cincinnati-Middletown 2,104,218 1.00
Rhode Island Providence-New Bedford-Fall River 1,612,989

Some of this data is rather odd because of the way the census bureau aggregates cities. For example, the largest city in New Jersey is Newark. But Newark is counted as part of the New York City metropolitan area, so doesn't count separately. If it did, New Jersey's quotient would be 5.86 instead of 1.35. I should probably rerun the data without the aggregation. But you get oddities that way also.

I also made a scatter plot. The x-axis is the population of the largest city, and the y-axis is the population of the second-largest city. Both axes are log-scale:

Nothing weird jumps out here. I probably should have plotted population against quotient. The data and programs are online if you would like to mess around with them.


I gratefully acknowledge the gift of Tim McKenzie. Thank you!

by Mark Dominus at February 17, 2009 08:29 PM

GHC / OpenSPARC Project

Thunderbirds are go

Alright, it's been a busy few days.

I've split the native code generator into architecture specific modules, and chopped the SPARC part into bite-sized chunks. There are still some #ifdefs around for other architectures, but most of the native code generator is compiled, independent of what the target architecture is.

I think I've squashed most of the bugs as well, but I'll have to wait overnight for a complete test run to finish.

Here are some inital nofib results.

The tests compare:

  • My 3Ghz Pentium4 Desktop

  • My 1.6Ghz Core2 Duo (Merom) MacBook Air

  • The 1.4Ghz SPARC T2


Take these results with a fair dose of salt, the libs on the T2 were built with -O2, but on the P4 and Merom I only used -O. I'll have some more comprehensive results in a few days. I'm not sure what's going on with "primetest", I'll have to run it again.

In short, with the current compiler, a Haskell program on a single T2 thread runs about 5x slower than on a P4 desktop. Remember that the T2 is totally set up for parallel processing, and has none of the instruction reordering or multiple issue of the P4. If we scale for the clock rate difference between the P4 and T2, then a T2 thread runs about 2.3 times slower than a P4 thread, clock for clock. On the other hand, 16 threads (2 per core) can be active at once on the T2.

Anyway, in regards to single thread performance on the T2, I think we're losing out big-time due to our total lack of instruction reordering.

Here is a piece of code from the nqueens test from nofib.

.LcFW:
add %i0,-20,%g1
cmp %g1,%i2
blu .LcFY
nop
add %i3,16,%i3 - dep
cmp %i3,%i4 -
bgu .LcFY
nop
sethi %hi(stg_upd_frame_info),%g1 - dep
or %g1,%lo(stg_upd_frame_info),%g1 -
st %g1,[%i0-8] -
st %l1,[%i0-4]
sethi %hi(sDJ_info),%g1 - dep
or %g1,%lo(sDJ_info),%g1 -
st %g1,[%i3-12] -
ld [%l1+12],%g1 - copy
st %g1,[%i3-4] -
ld [%l1+16],%g1 - copy
st %g1,[%i3] -
add %i3,-12,%g1
st %g1,[%i0-16]
ld [%l1+8],%g1 - copy
st %g1,[%i0-12] -
sethi %hi(base_GHCziNum_zdf6_closure),%l2 - dep
or %l2,%lo(base_GHCziNum_zdf6_closure),%l2 -
sethi %hi(sDK_info),%g1 - dep
or %g1,%lo(sDK_info),%g1 -
st %g1,[%i0-20]
add %i0,-20,%i0
call base_GHCziNum_zdp1Num_info,0
nop


A typical GHC compiled Haskell program spends most of its time copying data around memory. Such is the price of lazy evaluation, which we all know and love. The copies create a huge amount of memory traffic, and associated cache miss stalls. In addition, many of the instructions are directly dependent on the one just above them, which creates data hazard stalls.

At least for the T2, I expect that doing some basic instruction reordering will be a big win, so I'll try that first. Maybe some prefetching also, considering that we're moving so much data around memory.

by Ben Lippmeier (noreply@blogger.com) at February 17, 2009 08:13 PM

Magnus Therning

Python extensions: Please tell me there’s an easier way!

Dear Lazyweb,

Please tell me there’s an easier way of building Python C/C++ extensions (read shared objects) using automake than by using libtool. Please! Please!

I just want a frickin’ .so file, nothing complicated. Is the only way, besides using libtool, to write custom targets?

by Magnus at February 17, 2009 07:06 PM

Brent Yorgey

Typeclassopedia — a generic response


Thanks for all the fantastic feedback on the Typeclassopedia! Please keep it coming!

Such an outpouring of helpful comments and suggestions deserves a response, so I just wanted to write a quick note to say that I am reading every piece of feedback—whether here, on haskell-cafe, in #haskell, or on reddit—and fully intend to respond to each as appropriate. However, I probably won’t get around to it for a week or so, as at the moment I am focusing on digging myself out from all the other obligations that piled up while I was finishing the first draft. In the meantime, please keep sending me your suggestions!

However, there is one common suggestion I’ve received that I’d like to respond to now, which is that the Typeclassopedia should be put into wiki form. There are two main reasons I am submitting it for publication in the Monad.Reader, instead of creating it as a wiki in the first place:

  1. There is something about the permanence and elegance of a finely typeset, well-edited publication that a collection of wiki pages cannot capture. This isn’t just an issue of presentation; it also affects the content: writing for the Monad.Reader means that my writing and presentation are better than if I had created pages on a wiki.
  2. The Monad.Reader has a deadline; creating a wiki does not. Without a deadline, I probably never would have finished.

With that said, I think wikifying it after publication is a fantastic idea, and I hope that someone will take the initiative to do this. The Monad.Reader publishes all the source for each issue under a BSD license, so I don’t think this should be a problem.

by Brent at February 17, 2009 06:58 PM

Haskell Weekly News

Haskell Weekly News: February 17, 2009

Haskell Weekly News: February 17, 2009

Welcome to issue 105 of HWN, a newsletter covering developments in the Haskell community.

And here's the Belated Valentine's Day HWN! Motto: "Remembering that you love someone three days after you were supposed to is better than not remembering at all." Of course, it's late because I spent the weekend working on the Typeclassopedia (although you won't find a link to it in this HWN because I've only included things through Saturday). Much Haskell love to all!

Announcements

Plans for GHC 6.10.2. Ian Lynagh announced a quick summary of the plans for GHC 6.10.2. If there is a bug not on the high-priority list that is causing you major problems, please let the developers know. A release candidate is expected to be ready by the end of the week.

Bug fix to regex-tdfa, new version 0.97.3. ChrisK announced a new release of regex-tdfa which fixes some additional bugs. Three Cheers For QuickCheck!

Google Summer of Code 2009. Malcolm Wallace announced that haskell.org will once again be applying to be a Google Summer of Code mentor organization. Now is the time to begin discussing ideas for student projects. Also, if you wish to help publicize GSoC amongst students, there are official posters/fliers available. A long discussion of various project ideas followed, including some analysis of the factors which contribute to project success.

happs-tutorial 0.7. Creighton Hogg announced the release of happs-tutorial 0.7, the first release of happs-tutorial built against the new Happstack project. Creighton has now taken over development of the tutorial from Thomas Hartman.

first Grapefruit release. Wolfgang Jeltsch announced the first official release of Grapefruit, a library for Functional Reactive Programming (FRP) with a focus on user interfaces. With Grapefruit, you can implement reactive and interactive systems in a declarative style. User interfaces are described as networks of communicating widgets and windows. Communication is done via different kinds of signals which describe temporal behavior.

CFP: 5th Haskell Hackathon, April 17-19, Utrecht. Sean Leather issued a call for participation in the 5th Haskell Hackathon, which will be held in Utrecht, The Netherlands, from 17-19 April. The Haskell Hackathon is a collaborative coding festival with a simple focus: build and improve Haskell libraries, tools, and infrastructure. All are welcome! See the website for more information, or join the IRC channel (#haskell-hac5). Please register if you plan to attend!

Take a break: write an essay for Onward! Essays. Simon Peyton-Jones announced a call for submissions to Onward! Essays. An Onward! essay is a thoughtful reflection upon software-related technology. Its goal is to help the reader to share a new insight, engage with an argument, or wrestle with a dilemma. The deadline is 20 April.

Data.Stream 0.3. Wouter Swierstra announced a new version of the Data.Stream package, a modest library for manipulating infinite lists. Changes include support for lazy SmallCheck, an improved Show instance, stricter scans, various documentation fixes, and several new functions from Data.List.

X Haskell Bindings 0.1. Antoine Latter announced a new release of the X Haskell Bindings (XHB) library. The goal of XHB is to provide a Haskell implementation of the X11 wire protocol, similar in spirit to the X protocol C-language Binding (XCB).

Gtk2HS 0.10.0 released. Peter Gavin announced a new release of Gtk2HS, the Haskell GTK bindings. Notable changes include support for GHC 6.10, bindings to GIO and GtkSourceView-2.0, a full switch to the new model-view implementation using a Haskell model, and many others.

Discussion

Haskell.org GSoC. Daniel Kraft began a discussion about good topics for a Haskell GSoC project.

Painting logs to get a coloured tree. Joachim Breitner asked about elegant ways to annotate trees, leading to an interesting discussion.

Blog noise

Haskell news from the blogosphere.

Quotes of the Week

  • chrisdone: zipWith3 ($) (cycle [const,flip const]) "hai! haha!" "yarlysotense!"
  • quicksilver: I'm very unlikely to give the time of day to anything which doesn't let me continue to use emacs.
  • roconnor: don't let Float do your finance homework for you.
  • quicksilver: @go is made of STRING and FAIL.
  • drhodes: We're sorry Mr. Thunk, but this program is on a need to run basis, and you don't need to run. Now go away before I call the garbage collector.

About the Haskell Weekly News

New editions are posted to the Haskell mailing list as well as to the Haskell Sequence and Planet Haskell. RSS is also available, and headlines appear on haskell.org.

To help create new editions of this newsletter, please see the information on how to contribute. Send stories to byorgey at cis dot upenn dot edu. The darcs repository is available at darcs get http://code.haskell.org/~byorgey/code/hwn/ .

by byorgey at February 17, 2009 04:28 PM

Alex Mason

ASTM updates

Today, I've been talking with some people in #haskell about this ASTM thing, and I've had some great input, mainly from Stefan Ljungstrand (ski on #haskell), along with quicksilver and Simon Marlow, and I thought I'd share the changes I've put in with their help. I'm still not sure how useful this stuff is, but it's fun and I'm learning. If you're wondering what i'm on about, see this post.

So, the new features I've added are mainly to do with exception handling, so that variables don't 'die' if you call tail on [], they report the error, and don't change the 'state'. I've also deleted the Swap constructor, and replaced it with a more general Mod' constructor:

data Transaction a =
      Put a
    | Get (MVar a)
    | Mod (a -> a) (MVar (Maybe E.SomeException))
    | forall b. Mod' (a -> (a,b)) (MVar (Either E.SomeException b))
    | Atom (a -> Bool) (a -> a) (a -> a) (MVar Bool)

This you provide a function which takes the current 'state', possibly modifies it, and returns something else, and return that something else back to you. This works a lot like the State monad, but allows concurrency.

I've changed handler as well to look like this:

handler :: Chan (Transaction a) -> a -> IO b 
handler chan !x = do
  req <- readChan chan
  case req of
    Put a         -> handler chan a
    Get mvar      -> do
        putMVar mvar x
        handler chan x

    Mod f mvar    -> do
        let x' = f x
        p <- E.catch (E.evaluate x' >> return Nothing)
                     (\e -> return (Just e))
        putMVar mvar p
        case p of
          Nothing -> handler chan x'
          _       -> handler chan x

    Mod' f mvar    -> do
          let y@(a,b) = f x
          p <- E.try (E.evaluate a >> E.evaluate b)
          case p of
              Right _  -> do
                  putMVar mvar (Right b)
                  handler chan a
              (Left e) -> do
                  putMVar mvar (Left e)
                  handler chan x

    Atom test y n res ->
      if test x
        then do
              putMVar res True
              handler chan (y x)
        else do
              putMVar res False
              handler chan (n x)
    

As you can see, I've added some exception handling, but I still need to add some more to the Atom/condModAVar case. What I want is something that can keep running even after there's been an exception. I mean, who wants a mutable variable to just stop working huh?. I think once I get that done, along with haddock docs, I'll stick it on hackage.

by Alex Mason at February 17, 2009 02:21 PM

London Haskell Users Group

Lemmih: LHC - past, present and future

Here’s the abstract for Friday’s talk:

GHC is the undisputed master of high-level Haskell optimizations. With its fine-tuned simplifier and user-programmable rewriting rules, GHC has shown that Haskell can be very competitive when it comes to performance. However, woefully little attention has been directed at low-level optimizations which are becoming more significant as high-level optimization opportunities become scarce.

This talk is about the LHC Haskell Compiler and how it attempts to bring another level of optimizations to Haskell programs. I will cover why LHC was created, how far we’ve come with its development and what features we’re aiming at including.

by ganesh at February 17, 2009 08:56 AM

Arch Haskell News

hipmunk: 2D physics for Haskell


hipmunk is a nice Haskell binding to the 2D physics library, chipmunk. It’s now packaged up for Arch Linux, with demos:

Here’s a demo installing the packages from AUR and running the physics demo:

by dons00 at February 17, 2009 04:16 AM

John Goerzen (CosmicRay)

How To Think About Compression

… and the case against bzip2

Compression is with us all the time. I want to talk about general-purpose lossless compression here.

There is a lot of agonizing over compression ratios: the size of output for various sizes of input. For some situations, this is of course the single most important factor. For instance, if you’re Linus Torvalds putting your code out there for millions of people to download, the benefit of saving even a few percent of file size is well worth the cost of perhaps 50% worse compression performance. He compresses a source tarball once a month maybe, and we are all downloading it thousands of times a day.

On the other hand, when you’re doing backups, the calculation is different. Your storage media costs money, but so does your CPU. If you have a large photo collection or edit digital video, you may create 50GB of new data in a day. If you use a compression algorithm that’s too slow, your backup for one day may not complete before your backup for the next day starts. This is even more significant a problem when you consider enterprises backing up terabytes of data each day.

So I want to think of compression both in terms of resulting size and performance. Onward…

Starting Point

I started by looking at the practical compression test, which has some very useful charts. He has charted savings vs. runtime for a number of different compressors, and with the range of different settings for each.

If you look at his first chart, you’ll notice several interesting things:

  • gzip performance flattens at about -5 or -6, right where the manpage tells us it will, and in line with its defaults.
  • 7za -2 (the LZMA algorithm used in 7-Zip and p7zip) is both faster and smaller than any possible bzip2 combination. 7za -3 gets much slower.
  • bzip2’s performance is more tightly clustered than the others, both in terms of speed and space. bzip2 -3 is about the same speed as -1, but gains some space.

All this was very interesting, but had one limitation: it applied only to the gimp source tree, which is something of a best-case scenario for compression tools.

A 6GB Test
I wanted to try something a bit more interesting. I made an uncompressed tar file of /usr on my workstation, which comes to 6GB of data. My /usr contains highly compressible data such as header files and source code, ELF binaries and libraries, already-compressed documentation files, small icons, and the like. It is a large, real-world mix of data.

In fact, every compression comparison I saw was using data sets less than 1GB in size — hardly representative of backup workloads.

Let’s start with the numbers:

Tool MB saved Space vs. gzip Time vs. gzip Cost
gzip 3398 100.00% 100.00% 0.15
bzip2 3590 92.91% 333.05% 0.48 pbzip2 3587 92.99% 183.77% 0.26 lzma -1 3641 91.01% 195.58% 0.28 lzma -2 3783 85.76% 273.83% 0.37

In the “MB saved” column, higher numbers are better; in all other columns, lower numbers are better. I’m using clock seconds here on a dual-core machine. The cost column is clock seconds per MB saved.

What does this tell us?

  • bzip2 can do roughly 7% better than gzip, at a cost of a compression time more than 3 times as long.
  • lzma -1 compresses better than bzip2 -9 in less than twice the time of gzip. That is, it is significantly faster and marginally smaller than bzip2.
  • lzma -2 is significantly smaller and still somewhat faster than bzip2.
  • pbzip2 achieves better wall clock performance, though not better CPU time performance, than bzip2 — though even then, it is only marginally better than lzma -1 on a dual-core machine.

Some Pretty Charts

First, let’s see how the time vs. size numbers look:

compress-zoomed

Like the other charts, the best area is the lower left, and worst is upper right. It’s clear we have two outliers: gzip and bzip2. And a cluster of pretty similar performers.

This view somewhat magnifies the differences, though. Let’s add cat to the mix:

compress-big

And finally, look at the cost:

compress-efficiency

Conclusions

First off, the difference in time is far larger than the difference in space. We’re talking a difference of 15% at the most in terms of space, but orders of magnitude for time.

I think this pretty definitively is a death knell for bzip2. lzma -1 can achieve better compression in significantly less time, and lzma -2 can achieve significantly better compression in a little less time.

pbzip2 can help even that out in terms of clock time on multicore machines, but 7za already has a parallel LZMA implementation, and it seems only a matter of time before /usr/bin/lzma gets it too. Also, if I were to chart CPU time, the numbers would be even less kind to pbzip2 than to bzip2.

bzip2 does have some interesting properties, such as resetting everything every 900K, which could provide marginally better safety than any other compressor here — though I don’t know if lzma provides similar properties, or could.

I think a strong argument remains that gzip is most suitable for backups in the general case. lzma -1 makes a good contender when space is at more of a premium. bzip2 doesn’t seem to make a good contender at all now that we have lzma.

I have also made my spreadsheet (OpenOffice format) containing the raw numbers and charts available for those interested.

Update

Part 2 of this story is now available, which considers more compression tools, and looks at performance compressing files individually rather than the large tar file.

by John Goerzen at February 17, 2009 03:10 AM

February 16, 2009

Arch Haskell News

Arch Haskell News: Feb 16 2009


A regular update of Haskell in Arch Linux

Arch now has 926 Haskell packages in AUR.

That’s an increase of 27 new packages in the last 8 days, or 3.38 new Haskell apps a day. Well done everyone!

Noteworthy updates

Installing Packages from AUR

To install AUR packages, we recommend yaourt, as in:

yaourt --noconfirm  --lightbg --aur -S haskell-haha

You may want to alias that command line. Here’s an example from this week’s releases:

The reason to use yaourt over cabal-install is that AUR packages correctly resolve all versions and, more importantly, C library and other system dependencies. Packages will also be pulled from the binary releases in [extra] and [community] where available, saving you build times.

New and Updated Packages

We now present package info sorted by category — let us know if this helps!

Algorithm

Codec

Compilers

Control

Cryptography

Data

Database

HSQL

HDBC

HaskellDB

Devel

Graphics

Gui

Language

Math

Network

System

Text

Web

  • haskell-hsp-0.4.5: Haskell Server Pages is a library for writing dynamic server-side web pages.

The Arch Haskell Team maintains the Haskell toolchain on Arch Linux. You can join us in #arch-haskell on freenode.org, or on the mailing list.

by dons00 at February 16, 2009 09:47 PM

Ulisses Costa

Eric Kow (kowey)

announcing: burrito tutorial support group

It's really for the best if you leave these sorts of things out in the open.



The first step is to ask for forgiveness, right?

by kowey (noreply@blogger.com) at February 16, 2009 04:56 PM

Alex Mason

ASTM: redundant STMish fun

So, tonight, I had an idea for something that I'm not sure if it's either useful, efficient, interesting or anything other than a waste of time. It was an idea for the emulation of mutable variables, using functions as a way of storing the values in an accumulating parameter of sorts. They could safely be shared between threads, and could (and sort of do) support atomic actions.

It turned out to be really simple to implement, and I think just showing you the code would explain what I'm on about more than anything else. I don't know how else this could be extended (I'm sure it could be though, for some fairly interesting ideas), and since it has been written in the wee hours of the morning, I may be doing some pretty stupid stuff...

So, I'd love to hear some discussion (though yes, I do already know this could probably be done with MVars or TVars or what have you) and ideas, and here's the code:

module ASTM where
import Control.Concurrent
import Control.Concurrent.MVar
import Control.Concurrent.Chan

data Transaction a =
      Put a
    | Get (MVar a)
    | Mod (a -> a)
    | Atom (a -> Bool) (a -> a) (a -> a) (MVar Bool)

data AVar a = AVar (Chan (Transaction a)) 

newAVar :: a -> IO (AVar a)
newAVar x = do
    chan <- newChan :: IO (Chan (Transaction a))
    forkIO (handler chan x)
    return (AVar chan)
  where
      handler chan x = do
          req <- readChan chan
          case req of
              Put a         -> handler chan a
              Get mvar      -> do
                  putMVar mvar x
                  handler chan x
              Mod f         -> handler chan (f x)
              Atom test y n res ->
                if test x
                  then do
                        putMVar res True
                        handler chan (y x)
                  else do
                        putMVar res False
                        handler chan (n x)

putAVar (AVar chan) x = writeChan chan (Put x)
modAVar (AVar chan) f = writeChan chan (Mod f)
getAVar (AVar chan)   = do
    res <- newEmptyMVar
    writeChan chan (Get res)
    takeMVar res
condModAVar (AVar chan) p t f = do
    res <- newEmptyMVar
    writeChan chan (Atom p t f res)
    takeMVar res

by Alex Mason at February 16, 2009 04:47 PM

happstack.com

Announcing the launch of the Patch-Tag blog


Patch-Tag  now has a blog for product news and updates. Patch-taggers are encouraged to visit often as we would like to solicit as much feedback as possible from our user community!

by Matthew Elder at February 16, 2009 04:34 PM

Colin Ross

Haskell resource: Typeclassopedia

Brent Yorgey has published a first draft of what looks to be a fantastic resource for the Haskell programmer who wants to unserstand what all those strange type classes like Applicative, Monoid and Functor actually mean.

I am in the process of reading though it and the quote

Hmm, it doesn’t compile … maybe I’ll stick in an fmap here… nope, let’s see… maybe I need another (.) somewhere? … umm …

describes me all too well at times.

While it may not yet be complete, it is still quite a meaty piece of work, weighing in at 48 pages, including a full 111 useful references.

Read it now: The Typeclassopedia. Alternatively, the announcement.

All it needs now is a name which I can type successfully on the first attempt.

Related posts:

  1. XML parsing with Haskell Although I have been aware of the existence of XML,...

by Colin Ross at February 16, 2009 01:23 PM

XML parsing with Haskell

Although I have been aware of the existence of XML, I have never had any real experience of working with it. It looks like that is changing.

It all started when, on a whim, I purchased XSLT by Doug Tidwell. As I began reading it, typing in various bits and pieces of XML, I came to the conclusion that that I really needed to sit down and learn what XML is actually all about.

Up until that point my idea of XML was as a relatively simple format with tags, and so long as the tags match, everything is ok. How hard could it be to create an XML parser? It surely  must be pretty straightforward, and could be achieved in a few dozen lines of code.

And so began journey into the depths of the XML 1.0 specification. My code is currently just creeping over 2000 lines and has yet to pass my initial test suite, although it is getting closer.

I used the parsec library to do the parsing of the file together with the compact-string library to deal with encodings and they worked pretty smoothly once I figured out what I was trying to achieve with them. In fact, getting the initial XML parser was relatively straightforward - just some grunt work to implement it all. The problems mainly occurred with various well-formedness constraints and (something I have yet to tackle at all) the validity constraints. Additionally, since there are some nice tests to go with the specification, my focus is currently on getting them to pass, and in particular writing out my parsed XML document in canonical form.

My development of the XML parser has (will have!) the following stages:

  • Read the file as UTF16
  • Preprocess to get rid of carriage returns
  • Parse the basic structure
  • Expand various entities and make sure they also parse correctly
  • Ensure the various well-formedness constraints are satisfied
  • Ensure the various validity constraints are satisfied
  • Completion!

I am currently in the middle of stage 5 partly because I keep getting distracted by making the canonical export work (it is needed for checking results of some tests). Unfortunately, I believe I am still doing the easy stuff and that the most difficult stage is the next one where the validity constraints have to be enforced.

Nonetheless, it has been a valuable learning experience - my knowledge of XML has increased many-fold as has my familiarity with parsec and compact-string libraries.

One thing I have noticed with parsec is that I probably over-use the “try” combinator. I took a very lazy approach and basically implemented my own version of the parsec combinators which scatter “try”s like there is no tomorrow, to ensure I didn’t have to do any hard thinking about when they are actually required. While this means that parsing successfully is easy, it does seem to mean that if there is a parse error, I get almost no clue where the error was, which is somewhat unfortunate. Still, hopefully as time goes on, I can start to remove the “try”s bit by bit and gain some performance improvements along the way.

I did come up with a perhaps-useful combinator of my own during the process of implementing the XML specification. At several stages, there is a rule of the form

NotVowel = Char - [aeiou]

which should match any character except a vowel. My first attempt to implement this used “manyTill” like so

notVowel = do
   manyTill char vowel

but this has the unfortunate effect of “eating” the first vowel encountered. Instead, it should be implemented something like this:

notVowel = do
   m <- optionMaybe $ C.lookAhead vowel
   case m of
      Just _ -> P.unexpected "Vowel encountered"
      Nothing -> char

or, in its more general form:

type Parser = P.Parsec Input XmlState
butNot :: (Parser a) -> (Parser b) -> (Parser a)
butNot p e = do
   m <- optionMaybe $ C.lookAhead e
   case m of
      Just _ -> P.unexpected "butNot failure"
      Nothing -> p

This seems to do the job marvellously well. Basically, it looks for the “bad” input and if it finds it, fails. If it doesn’t find the “bad” input, then it happily parses “good” input.

Related posts:

  1. Creating a minimal HTTP server in Haskell I have been spending quite a lot of time lately...

by Colin Ross at February 16, 2009 01:08 PM

Brent Yorgey

The Typeclassopedia — request for feedback


I have just submitted a draft article for inclusion in the Monad.Reader entitled “The Typeclassopedia”. I will let the abstract speak for itself:

The standard Haskell libraries feature a number of type classes with algebraic or categorical underpinnings. Becoming a fluent Haskell hacker requires intimate familiarity with them all, yet acquiring this familiarity often involves combing through a mountain of tutorials, blog posts, mailing list archives, and IRC logs.

The goal of this article is to serve as a starting point for the student of Haskell wishing to gain a firm grasp of its standard type classes. The essentials of each type class are introduced, with examples, commentary, and extensive references for further reading.

I would love feedback from anyone, from the newest newb to the expertest expert, who would be kind enough to take a look. Particular types of feedback I would appreciate include:

  • Are there parts that are confusing or could be worded more clearly?
  • Are there parts that are stated incorrectly?
  • Do you know of any additional references that could be included?

I am looking for more references for Foldable, Traversable, and Comonad in particular, so if you know of any good resources/examples/papers related to any of those, please let me know.

At 48 pages and 110 citations, the article is rather hefty, so I certainly don’t expect most people to read through all of it anytime soon—but even if you only take a look at a section or two about which you are particularly interested and/or knowledgeable, your feedback would be greatly appreciated! I hope that this can become a valuable reference for the Haskell community.

Without further ado: The Typeclassopedia.

by Brent at February 16, 2009 09:12 AM

Sean Leather

Incremental fold, a design pattern

I recently read the article "How to Refold a Map" by David F. Place in The Monad.Reader Issue 11. I've been thinking about incremental algorithms in Haskell for some time, and I realized that Place has written a specific instance (and optimization) of a more general concept: the incremental fold.

In this article, I demonstrate a design pattern for converting a datatype and related functions into an incremental fold. The pattern is not difficult to comprehend, but it would be nice to improve upon it. I explore a few improvements and issues with those improvements. Ultimately, I'd like to see this functionality in a program instead of a design pattern.

Note: This is a literate Haskell article. You can copy the text of the entire article, paste it into a new file called IncrementalTreeFold.lhs, and load it into GHCi.


> {-# LANGUAGE MultiParamTypeClasses #-}
> {-# LANGUAGE FlexibleInstances #-}
> {-# LANGUAGE ScopedTypeVariables #-}

> module IncrementalTreeFold where
> import Prelude hiding (elem)
> import qualified Data.Char as Char (ord)

Introducing a Typical Binary Tree

Before we get to the conversion, let's choose an appropriate datatype. Place adapted the Map type used in Data.Map (or Set in Data.Set). To simplify my presentation, I will use an ordered binary tree with labeled nodes.


> data Tree a
>   = Tip
>   | Bin a (Tree a) (Tree a)
>   deriving Show

Next, let's introduce some useful functions. An incremental fold is not necessarily like applying a fold function (a.k.a. a catamorphism, not a crush function that has become known as a fold) to a value directly. Instead, as I will later show, it integrates into existing functions that manipulate values. That said, we should have some functions for building Trees. Here is the beginning of a Tree API. (There are a number of other operations, e.g. delete and lookup, that can easily be added but do not contribute much to the discussion.)

empty builds a tree with no elements.


> empty :: (Ord a) => Tree a
> empty = Tip

singleton builds a tree with a single element.


> singleton :: (Ord a) => a -> Tree a
> singleton x = Bin x Tip Tip

insert puts a value in the appropriate place given a left-to-right ordering of values in the tree.


> insert :: (Ord a) => a -> Tree a -> Tree a
> insert x t =
>   case t of
>     Tip ->
>       singleton x
>     Bin y lt rt ->
>       case compare x y of
>         LT -> Bin y (insert x lt) rt
>         GT -> Bin y lt (insert x rt)
>         EQ -> Bin x lt rt

fromList creates a tree from a list of values.


> fromList :: (Ord a) => [a] -> Tree a
> fromList = foldr insert empty

elem determines if a value is an element of a tree.


> elem :: (Ord a) => a -> Tree a -> Bool
> elem x t =
>   case t of
>     Tip ->
>       False
>     Bin y lt rt ->
>       case compare x y of
>         LT -> elem x lt
>         GT -> elem x rt
>         EQ -> True

Now, using our library of sorts, we can create binary search tree and check if a value is in the tree.


> test1 = 37 `elem` fromList [8,23,37,82,3]

Tree Folds

Suppose that we now want the size of the tree. For good abstraction and high reuse, we create a fold function.


> data Alg a b = Alg { ftip :: b, fbin :: a -> b -> b -> b }

> fold :: Alg a b -> Tree a -> b
> fold alg = go
>   where
>     go Tip           = ftip alg
>     go (Bin x lt rt) = fbin alg x (go lt) (go rt)

fold allows us to write a simple size function.


> size :: Tree a -> Int
> size = fold (Alg 0 (\_ lr rr -> 1 + lr + rr))

I use the datatype Alg here to contain the algebra of the fold. In size, we simply replace each constructor in the algebra of Tree with a corresponding element from the algebra of integer addition. Since you're reading this article, you're probably a Haskell programmer and already familiar with the sorts of functions that can be written with folds. Here are a few others.


> filter :: (a -> Bool) -> Tree a -> [a]
> filter f = fold (Alg [] (\x lr rr -> if f x then [x] else [] ++ lr ++ rr))

> ord :: Tree Char -> Tree Int
> ord  = fold (Alg Tip (\x lt rt -> Bin (Char.ord x) lt rt))

Incremental Change

Now that we have a grasp on using a fold on a datatype, I would like to show how to extend my binary tree "library" defined above to support an incremental fold. The incremental fold can (I believe) do everything a traditional fold can do, but it does it during Tree construction instead of externally in a separate function. This means that every time we produce a new Tree (via singleton, insert, or fromList for example), we get a new result of the incremental fold.

Transforming our library into an incremental calculating machine involves several steps. The first step is extending the datatype to hold the incremental result. Since we want to be polymorphic in the result type, we add a type parameter r to the Tree type constructor. And since each constructor may possibly have an incremental result, it must also be extended with a place holder for r.


> data Tree' a r
>   = Tip' r
>   | Bin' a (Tree' a r) (Tree' a r) r
>   deriving Show

For convenience and possibly to hide the modified constructors from the outside world, we add a function for retrieving the increment result.


> result' :: Tree' a r -> r
> result' (Tip' r)       = r
> result' (Bin' _ _ _ r) = r

As I mentioned earlier, the machinery of the fold is now in the construction. To implement this second step, we use smart constructors.


> tip' :: Alg a r -> Tree' a r
> tip' alg = Tip' (ftip alg)

> bin' :: Alg a r -> a -> Tree' a r -> Tree' a r -> Tree' a r
> bin' alg x lt rt = Bin' x lt rt (fbin alg x (result' lt) (result' rt))

Both tip' and bin' construct new values of Tree' a r and using the algebra, calculate the incremental result to be stored in each value. Thus, the actual fold operation is "hidden" in the construction of values.

Now, in order to put the incremental fold to work in a function, we simply (1) add the algebra to the function's arguments, (2) add an wildcard pattern for the result field in constructor patterns, and (3) replace applications of the constructors with that of their incremental cousins. Here's an example of the singleton and insert functions modified for incremental folding.


> singleton' :: (Ord a) => Alg a r -> a -> Tree' a r
> singleton' alg x = bin' alg x (tip' alg) (tip' alg)

> insert' :: (Ord a) => Alg a r -> a -> Tree' a r -> Tree' a r
> insert' alg x t =
>   case t of
>     Tip' _ ->
>       singleton' alg x
>     Bin' y lt rt _ ->
>       case compare x y of
>         LT -> bin' alg y (insert' alg x lt) rt
>         GT -> bin' alg y lt (insert' alg x rt)
>         EQ -> bin' alg x lt rt

Comparing these functions with the initial versions, we see that the changes are readily apparent. Modify every other Tree'-hugging function in the same manner, and you have a design pattern for an incremental fold!

Improving the Incremental Implementation

Of course, you may complain that there's some amount of boilerplate work involved. For example, we have to add this alg argument everywhere. Let's try to replace that with a type class.


 class Alg'' a r where
   ftip'' :: r
   fbin'' :: a -> r -> r -> r

And we redefine our smart constructors.


 tip'' :: (Alg' a r) => Tree' a r
 tip'' = Tip' ftip''

But there's a problem here! GHC reports that it Could not deduce (Alg'' a r) from the context (Alg'' a1 r). The poor compiler cannot infer the type of the parameter a since ftip'' has only type r.

Let's try another version of the class. In this one, we add a dummy argument to ftip' in order to force GHC to correctly infer the full type.


> class Alg'' a r where
>   ftip'' :: a -> r
>   fbin'' :: a -> r -> r -> r

> tip'' :: forall a r . (Alg'' a r) => Tree' a r
> tip'' = Tip' (ftip'' (undefined :: a))

> bin'' :: (Alg'' a r) => a -> Tree' a r -> Tree' a r -> Tree' a r
> bin'' x lt rt = Bin' x lt rt (fbin'' x (result' lt) (result' rt))

This provides one (not very pretty) solution to the problem. I'm able to get around the need to require an argument for tip'' by using lexically scoped type variables. But it doesn't remove the ugly type from ftip'', and the user is forced to ignore it when writing an instance.

The functions can now be rewritten with the Alg'' constraint.


> empty'' :: (Ord a, Alg'' a r) => Tree' a r
> empty'' = tip''

> singleton'' :: (Ord a, Alg'' a r) => a -> Tree' a r
> singleton'' x = bin'' x tip'' tip''

> insert'' :: (Ord a, Alg'' a r) => a -> Tree' a r -> Tree' a r
> insert'' x t =
>   case t of
>     Tip' _ ->
>       singleton'' x
>     Bin' y lt rt _ ->
>       case compare x y of
>         LT -> bin'' y (insert'' x lt) rt
>         GT -> bin'' y lt (insert'' x rt)
>         EQ -> bin'' x lt rt

> fromList'' :: (Ord a, Alg'' a r) => [a] -> Tree' a r
> fromList'' = foldr insert'' empty''

These versions look more like the non-incremental implementations above. To use them, we need to declare an instance of Alg'' with an appropriate algebra for our desired incremental result. Here's how we would rewrite size.


> newtype Size = Size { unSize :: Int }

> instance Alg'' a Size where
>   ftip'' _ = Size 0
>   fbin'' _ lr rr = Size (1 + unSize lr + unSize rr)

> size'' :: Tree' a Size -> Int
> size'' = unSize . result'

> test2 = size'' $ insert'' 's' $ insert'' 'p' $ insert'' 'l' $ fromList'' "onderzoek"

Size is still defined as a fold, but the result is incrementally built with each application of a library function. This can have a nice performance boost as Place also found in his article.

Generic Thoughts

On reflecting over my implementation, I really don't like the dummy arguments required by constructors like Tip. There are other approaches to dealing with this, but I haven't yet found a better one. If you use a functional dependency such as r -> a in the definition of Alg'', then a would be uniquely determined by r. In the case of size'', we would have to specify a concrete element type for Tree' instead of the parameter a (or use undecidable instances). Perhaps, dear reader, you might have a better solution?

The incremental fold pattern is great for documenting an idea, but it has several downsides: (1) The obvious one is that it requires modifying a datatype and code. This is not always desirable and often not practical. (2) Implementing an incremental fold can involve a lot of boilerplate code and many, small changes that are monotonous and boring. It's very easy to make mistakes. In fact, I made several copy-paste-and-forget-to-change errors while writing this article.

As Jeremy Gibbons and others have shown us, design patterns are better as programs. Since the code is so regular, it seems very receptive to some generic programming. I plan to explore this further, possibly using one of the many generics libraries available for Haskell or designing a new one. Suggestions and feedback are welcome.

by Sean Leather (noreply@blogger.com) at February 16, 2009 08:06 AM

Mark Jason Dominus

Milo of Croton and the sometimes failure of inductive proofs

Ranjit Bhatnagar once told me the following story: A young boy, upon hearing the legend of Milo of Croton, determined to do the same. There was a calf in the barn, born that very morning, and the boy resolved to lift up the calf each day. As the calf grew, so would his strength, day by day, until the calf was grown and he was able to lift a bull.

"Did it work?" I asked.

"No," said Ranjit. "A newborn calf already weighs like a hundred pounds."

Usually you expect the induction step to fail, but sometimes it's the base case that gets you.

by Mark Dominus at February 16, 2009 05:00 AM

Arch Haskell News

haskelldb: high level, type safe database queries for Haskell


The venerable haskelldb high level database interface for Haskell is now packaged up for Arch.

HaskellDB is a combinator library for expressing queries and other operations on relational databases in a type safe and declarative way. All the queries and operations are completely expressed within Haskell, no embedded (SQL) commands are needed.

The code base is around a decade now, and quite mature, but it has only recently been brought into the cabal and hackage world, making it trivial to package up and distribute. You can find all the packages here:

This release of haskelldb is layered over medium-level database interface suite, hdbc., so it can reuse the hdbc backends. The layers of Haskell database libs packaged up looks something like:

  1. High level: haskelldb, Takusen
  2. “Normal” level: HDBC, hsql
  3. Low level: sqlite, anydbm, hsSqlite3, PostgreSQL, BerkeleyDB

Low level ones typically just wrap the C interfaces underneath, providing few new safety guarantees. Medium level ones generally present a “sensible” Haskell API to the exposed db libraries, while the high level ones attempt to abstract out significant safety or productivity by embedding concepts deeper into the language.

Different libraries support different C backends, I’ll attempt to break that down here:

mysql postgres sqlite odbc oracle notes
hdbc Documented in RWH
haskelldb
High level
takusen Chooses backend(s) via compile time flag
hsql ? ? Less active?

Also of note is haskell-couchdb , and even haskell-hs3, for a different storage needs.

Finally, if you want to step away from calling out  to C altogether, and go for something purely in Haskell, there’s haskell-tcache, a transactional cache with configurable persistence in 100% Haskell using transactional memory.

by dons00 at February 16, 2009 03:36 AM

Manuel M T Chakravarty

Comparison of type families with functional dependencies.

Comparison of type families with functional dependencies.: This is a haskell-cafe post of a brief summary of the commonalities and differences of the two language features.

February 16, 2009 03:10 AM

Darcs

darcs weekly news #2

2009-02-16 This is a back-posting of an older darcs weekly news article from before the creation of blog.darcs.net.

News and discussions

  1. Growing the darcs team: The darcs unstable repository is coming back, with David Roundy as its maintainer. Eric will be taking care of stable and keeping in closely in synch.
  2. Shiny new IRC logs: Thanks to Moritz Lenz, the #darcs and #darcs-theory IRC channels are now being logged with fancy formatting and search capability
  3. Hacking darcs: Petr Ročkai shares his recent hopes and experiences as a darcs user turned developer. Come share the excitement!

Reviewers

Thanks to our patch reviewers for this week for giving David a hand!

  • Jason Dagit
  • Nathan Gray
  • Eric Kow
  • Petr Ročkai

Issues resolved in the last week (1)

issue966 Dmitry Kurochkin

fix apply_inv_to_matcher_inclusive. http://bugs.darcs.net/issue966

Patches applied in the last week (37)

2008-08-31 David Roundy
  • don't show ssh stderr output unless we're passed --debug.
  • fix bug in --list-options (tab completion).
  • fix bug in makeRelative.
2008-08-30 Ganesh Sittampalam
  • add warning to configure about Haskell zlib speed
  • make use of Haskell zlib dependent on bytestring
  • add option to use Haskell zlib package
2008-08-22 Eric Kow
  • Remove unused FileSystem module.
  • Add a link to a repository browser for darcs's code.
2008-08-29

kili at outback dot escape dot de
  • Replace grep invocation by perl code
2008-08-24 David Roundy
  • clean up network/get.sh test.
  • fix type of withRepository and friends.
  • fix recent bug in --list-options.
2008-08-28 Dmitry Kurochkin
  • Check for package random on windows, used in Ssh module.
  • Debug messages in curl module.
2008-08-28 David Roundy
  • TAG working version.
2008-08-27 Dmitry Kurochkin
  • Use InclusiveOrExclusive instead of Bool in apply_inv_to_matcher.
2008-08-27 David Roundy
  • add more modules to make witnesses.
2008-08-27 Jason Dagit
  • updates to Darcs.Patch.Unit for type witnesses
2008-08-27 Dmitry Kurochkin
  • Refactor get_matcher and apply_inv_to_matcher functions from Darcs.Match module.
  • Resolve issue966: fix apply_inv_to_matcher_inclusive.
  • Simplify withCurrentDirectory.
2008-08-27 Jason Dagit
  • updates to Sealed.lhs to support type witness refactor in commands
  • updates to Ordered.lhs to support type witness refactor in commands
  • make Annotate.lhs compile with type witnesses
2008-08-27 David Roundy
  • fix type witnesses in Internal.
2008-08-27 Jason Dagit
  • updates to Repository.Internal to fix conflicts and support type witness refactor in commands
  • fix error in Properties due to new commuteFL
  • fix minor type witness compile error with new commuteFL
  • fix conflicts with get_extra changes
  • improve reporting for bug in get_extra
  • Finish refactor of Unrevert as well as making it pass double-unrevert.sh
  • add double-unrevert.sh test
  • partial type witnesses in Unrevert
2008-08-26 Eric Kow
  • More ChangeLog entries since 2.0.2
2008-08-27 David Roundy
  • fix bug in defaultrepo.
2008-08-26 Jason Dagit
  • fix accidental reversal in tentativelyAddToPending
  • minor refator to get_extra improve comments

by kowey (noreply@blogger.com) at February 16, 2009 12:42 AM

darcs weekly news #3

2009-02-16 This is a back-posting of an older darcs weekly news article from before the creation of blog.darcs.net.

News and discussions

  1. Venues confirmed for the darcs hacking sprint, 25-26 October. Brighton and Portland are CONFIRMED; Paris is likely. Come hack with us!
  2. Planning darcs 2.0.3. We have started making steps towards a release for the end of September. Eric thinks we are only a buildbot and couple of bugfixes away from a prerelease.
  3. Darcs patch theory. Ian Lynagh continues his patch theory research. He has written up a nice explanation and a working prototype of a darcs-like patch theory.
  4. Retiring GHC 6.4. The darcs team would like to know if anybody is still using GHC 6.4 to compile darcs, so that we can focus on later versions (6.6 and 6.8).

Reviewers

Thanks to our patch reviewers for this week for giving David a hand!

  • Jason Dagit
  • Trent Buck

Issues resolved in the last week (7)

issue844 David Roundy
issue924 Eric Kow
issue1015 Ganesh Sittampalam
issue1037 Dmitry Kurochkin
issue1049 David Roundy
issue1050 Eric Kow
issue1063 Eric Kow

Patches applied in the last week (72)

See the darcs weekly news #3 email for the full list.

by kowey (noreply@blogger.com) at February 16, 2009 12:42 AM

darcs weekly news #4

2009-02-16 This is a back-posting of an older darcs weekly news article from before the creation of blog.darcs.net.

News and discussions

  1. First pre-release of darcs 2.0.3. This version of darcs has some very nice bug fixes on offer. A few more user-friendliness tweaks are planned for the actual release.
  2. Third venue confirmed for darcs hacking sprint, 25-26 October. Brighton, Portland and now Paris are all CONFIRMED. Come hack with us!
  3. code.haskell.org upgrades to darcs 2! /usr/bin/darcs is now darcs 2.0.2 on this server. No action is needed on the user's part.
  4. Retiring GHC 6.4. Nobody seems to be using GHC 6.4 to compile darcs after all, so we shall be dropping support for it.

Reviewers

Thanks to our patch reviewers for this week for giving David a hand!

  • Jason Dagit
  • Nathan Gray
  • Trent W. Buck

Issues resolved in the last week (6)

issue691 Dmitry Kurochkin
issue709 David Roundy
issue885 David Roundy
issue1012 David Roundy
issue1054 Dmitry Kurochkin
issue1057 David Roundy

Patches applied in the last week (86)

See 2008-09-17 text entry for details

by kowey (noreply@blogger.com) at February 16, 2009 12:42 AM

February 15, 2009

Antoine Latter

MaybeT - The CPS Version

> {-# LANGUAGE Rank2Types #-}
> import Control.Monad
I think I finally understand writing code into continuation passing style. I've understood it at an academic level for some time - but that's different from being able to write the code.

This post presents a different implementation of the Maybe monad transformer - usually presented as so:

data MaybeT m a = MaybeT {runMaybeT :: m (Maybe a)}
which can be used to add the notion of short-circuiting failure to any other monad (sortof a simpler version of ErrorT from the MTL).
I first came across MaybeT in a page on the Haskell Wiki.
This presentation of MaybeT uses the Church encoding of the data-type:
> newtype MaybeT m a = MaybeT {unMaybeT :: forall b . m b -> (a -> m b) -> m b}
Note the similarity to the Prelude function maybe. We can unwrap the transformer like so:

> runMaybeT :: Monad m => MaybeT m a -> m (Maybe a)
> runMaybeT m = unMaybeT m (return Nothing) (return . Just)
This runMaybeT should be a drop-in replacement for the old one.
The advantage here is that we can write the Monad and MonadPlus instances without calling bind or return in the underlying monad m, and without doing any case analysis on Just or Nothing values:
> instance Monad (MaybeT m) where
> return x = MaybeT $ \_ suc -> suc a
>
> m >>= k = MaybeT $ \fail suc ->
> unMaybeT m fail $ \x ->
> unMaybeT (k x) fail suc
>
> fail _ = mzero

> instance MonadPlus (MaybeT m) where
> mzero = MaybeT $ \fail _ -> fail
>
> m `mplus` n = MaybeT $ \fail suc ->
> unMaybeT m (unMaybeT n fail suc) suc
It's just a matter of threading the failure and success continuations to the right place at the right time.
To show that this is equivalent to the old implementation, here's a re-write of the old MaybeT data constructor from above:

> fromMaybe :: Monad m => m (Maybe a) -> MaybeT m a
> fromMaybe m = MaybeT $ \fail suc -> do
> res - m
> case res of
> Nothing -> fail
> Just x -> suc x

So anything you can do with the other version, you can do with this version. And for most things it should be a drop-in replacement.

by noreply@blogger.com (Antoine) at February 15, 2009 07:24 PM

Dan Piponi (sigfpe)

Beyond Monads

The state monad gives an elegant way to thread state information through Haskell code. Unfortunately it has an annoying limitation: the state must have the same type throughout the monadic expression. In this post I want to look at how to fix this. Unfortunately, fixing State means it's no longer a monad, but we'll discover a new abstraction that replaces monads. And then we can look at what else this abstraction is good for. The cool bit is that we have to write virtually no new code, and we'll even coax the compiler into doing the hard work of figuring out what the new abstraction should be.

This is all based on an idea that has been invented by a bunch of people independently, although in slightly different forms. I'm being chiefly guided by the paper Parameterized Notions of Computation.

The problem with the state monad is that it is defined by

newtype State s a = State { runState :: s -> (a, s) }

The state going into and out of one of these values is the same, s. We can't vary the type of the state as we pass through our code. But that's really easy to fix, just define:


> import Prelude hiding (return,(>>=),(>>),(.),id,drop)
> import Control.Category

> newtype State s1 s2 a = State { runState :: s1 -> (a, s2) }


I can now just copy and paste the definitions (with name changes to avoid clashes) out of the ghc prelude source code


> return' a = State $ \s -> (a, s)
> m >>>= k = State $ \s -> let
> (a, s') = runState m s
> in runState (k a) s'

> get = State $ \s -> (s, s)
> put s = State $ \_ -> ((), s)


We don't have to change a thing! The old code exactly matches the new type. We can now write code using the new State:


> test1 = return' 1 >>>= \x ->
> return' 2 >>>= \y ->
> get >>>= \z ->
> put (x+y*z) >>>= \_ ->
> return' z
> go1 = runState test1 10


But we're now also able to write code like:


> test2 = return' 1 >>>= \x ->
> return' 2 >>>= \y ->
> get >>>= \z ->
> put (show (x+y*z)) >>>= \_ ->
> return' z
> go2 = runState test2 10


The state starts of as an Integer but ends up as a String.

Problem solved! Except that this definition of State doesn't give us a monad and so we lose the benefits of having an interface shared by many monads. Is there a new more appropriate abstraction we can use? Rather than scratch our heads over it, we can just ask ghci to tell us what's going on.

*Main> :t return'
return' :: a -> State s1 s1 a
*Main> :t (>>>=)
(>>>=) :: State s1 s11 t -> (t -> State s11 s2 a) -> State s1 s2 a

This immediately suggests a new abstraction:


> class ParameterisedMonad m where
> return :: a -> m s s a
> (>>=) :: m s1 s2 t -> (t -> m s2 s3 a) -> m s1 s3 a

> x >> f = x >>= \_ -> f


It's a lot like the usual Monad class except that we're now parameterising uses of this class with a pair of types. Our new >>= operator also has a compatibility condition on it. We can think of an element of m s1 s2 as having a 'tail' and 'head' living in s1 and s2 respectively. In order to use >>= we require the head of the first argument to match the tail given by the second argument.

Anyway, we have:


> instance ParameterisedMonad State where
> return = return'
> (>>=) = (>>>=)


We didn't really design this class, we just used what ghci told us. Will it turn out to be a useful abstraction?

First a category theoretical aside: in this post I talked about how monads were really a kind of abstract monoid. Well ParameterisedMonad is a kind of abstract category. If we were to implement join for this class it would play a role analogous to composition of arrows in a category. In a monoid you can multiply any old elements together to get a new element. In a category, you can't multiply two arrows together unless the tail of the second matches the head of the first.

Now we can generalise the writer monad to a ParameterisedMonad. But there's a twist: every monoid gives rise to a writer. This time we'll find that every category gives rise to a ParameterisedMonad. Here's the definition. Again, it was lifted straight out of the source for the usual Writer monad. The main change is replacing mempty and mappend with id and flip (.).


> data Writer cat s1 s2 a = Writer { runWriter :: (a,cat s1 s2) }
> instance (Category cat) => ParameterisedMonad (Writer cat) where
> return a = Writer (a,id)
> m >>= k = Writer $ let
> (a, w) = runWriter m
> (b, w') = runWriter (k a)
> in (b, w' . w)
> tell w = Writer ((),w)
> execWriter m = snd (runWriter m)


It's just like the usual Writer monad except that the type of the 'written' data may change. I'll borrow an example (modified a bit) from the paper. Define some type safe stack machine operations that are guaranteed not to blow your stack:


> push n x = (n,x)
> drop (_,x) = x
> dup (n,x) = (n,(n,x))
> add (m,(n,x)) = (m+n,x)
> swap (m,(n,x)) = (n,(m,x))


We can now 'write' the composition of a bunch of these operations as a 'side effect':


> test3 = tell (push 1) >>
> tell (push 2) >>
> tell dup >>
> tell add >>
> tell swap >>
> tell drop
> go3 = execWriter test3 ()


I guess there's one last thing I have to find. The mother of all parameterised monads. Again, we lift code from the ghc libraries, this time from Control.Monad.Cont. I just tweak the definition ever so slightly. Normally when you hand a continuation to an element of the Cont type it gives you back an element of the continuation's range. We allow the return of any type. This time the implementations of return and (>>=) remain completely unchanged:


> newtype Cont r1 r2 a = Cont { runCont :: (a -> r2) -> r1 }
> instance ParameterisedMonad Cont where
> return a = Cont ($ a)
> m >>= k = Cont $ \c -> runCont m $ \a -> runCont (k a) c

> i x = Cont (\fred -> x >>= fred)
> run m = runCont m return

> test4 = run $ i (tell (push 1)) >>
> i (tell (push 2)) >>
> i (tell dup) >>
> i (tell add) >>
> i (tell swap) >>
> i (tell drop)

> go4 = execWriter test4 ()


So what's going on here? The implementations of these instances require almost trivial changes to the original monads, or in two cases no changes at all apart from the type signature. I have my opinion: Haskell programmers have been using the wrong type class all along. In each case the type signature for return and >>= was too strict and so the functionality was being unnecessarily shackled. By writing the code without a signature, ghci tells us what the correct signature should have been all along. I think it might just possibly be time to consider making ParameterisedMonad as important as Monad to Haskell programming. At the very least, do-notation needs to be adapted to support ParameterisedMonad.

Update: You *can* use do-notation with ParameterisedMonad if you use the NoImplicitPrelude flag.

Update2: Some credits and links:


  1. The Polystate Monad is one of the independent discoveries I mentioned above.
  2. A more general approach to Parameterized Monads in Haskell.
  3. A comment on Parameterized Monads that shows explicitly how to make this work with NoImplicitPrelude.
  4. Oleg's Variable (type)state `monad'.
  5. Wadler discovered this design pattern back in 1993 in Monads and composable continuations.


I didn't contribute anything, this article is just advocacy.

by sigfpe (noreply@blogger.com) at February 15, 2009 04:14 PM

Gregg Reynolds

Intergalactic Telefunctors and Quantum Entanglement

In a previous article I argued against the pernicious Container Fiction. Some respondents have quite reasonably responded that this seems a bit pedantic; it may be true that e.g. a list is not really a container, but it's such a useful metaphor that only a pedant would insist on banning it.

Indeed it is a very useful metaphor, but the motivation for exposing it as a "pernicious" myth is not linguistic fascism, but rather pedagogical clarity. The Container Fiction is only pernicious insofar as it interferes with a clear understanding of the underlying abstraction it attempts to capture: the functor as a special kind of relation that enables communication between two different and mutually incomprehensible universes. This is bound to happen, since the container fiction is deeply embedded in the world of set theory, and the key to understanding Haskell is category theory, which is a whole nother thing.

The list is probably not the best example, since it involves a lot of complexity, what with the free monad and so forth. A simpler example would be a pair (a,b). This can obviously considered a kind of container, but as metaphors go a somewhat less pernicious image is the chemical compound. A chemical compound has different properties than its consituents; carbon monoxide (CO) is quite a different thing than carbon and oxygen. It's not a container of its constituents, it's their compound. The relation of (the denoted value) of "(a,b)" to its "components" a and b is similar. It's a mereological relation, not a containership relation.

But even that obscures the true nature of the functor (). The value denoted by "(a,b)" is not a compound, it is a primitive, whole, opaque value. (Disregard for the sake of argument whether it is dependent on the human mind.) The compound is the expression "(a,b)" itself.

My proposition is that a category theoretic explanation can be clearer and simpler than such metaphorical expositions, leading to a solid articulated intuition of the structural nature of functors without resorting to colorful metaphors. Well, maybe one, but it's arguably not a metaphor. A full exposition would take some very careful writing and a bunch of diagrams, but here's a sketch of how it would work.

Start with a, b, and (). Symbols 'a' and 'b' name things in a home universe; '()' is (the name of) an intergalactic "telefunctor" that relates the home universe to an alien universe of pair values. "(a,b)" takes two primitive values from home to a third primitive value in the alien universe. It doesn't convey a and b to the alien universe; rather, it entangles them. IOW, "(a,b)" is a kind of name or definite description of a value that is just as primitive and indivisible as the value denoted by "a" but that lives in an alien universe. We could say that "(a,b)" represents the quantum entanglement of a and b with the value denoted by "(a,b)". Call that value x. It lives in an alien universe; we know nothing about its internal structure, nor what it looks like in its universe, nor how it relates to other elements of its universe. But we do know something about how it relates to values in our home universe. We obviously know it is related - via () - to a and b together. But we also know, because of the way we define () - since this is just a brief sketch I omit this definition - we know that x is related to a and b individually. Our definition of () goes with two other definitions: fst (a,b) = a, and snd (a,b) = b.

Now we have defined the value of () purely in terms of how it relates things across intergalactic (ok, couldn't resist a metaphor) boundaries - morphisms. We could go further and show how a and b can also be defined as morphisms - after all, they're just names denoting values, and those values are just as opaque and unapproachable as the value of "(a,b)". Our knowledge of how all these things behave is expressed in terms not of what they are, but in how they relate. You can judge a man by his friends; you can understand mathematical values by their relations to other values.

A diagram might represent values as blackened circles. I believe this approach leads to a very clear, simple, and reasonably complete exposition. The metaphor of alien universes and intergalactic telefunctors could of course be dispensed with, but it does add color without introducing semantic distortion.

The real virtue of this approach becomes more clear when we complement the above exposition of the object component of a functor with a similar account of the morphism component that takes functions from one realm to functions in the alien realm. The pedagogical payoff is the realization that a functor allows us to use what we know about values in one realm to "manipulate" values in another realm. The best metaphor for the functor is neither containment nor mereology, but quantum entanglement.

by gargar

February 15, 2009 04:06 PM

In Praise of Elitism

A respondent to one of my earlier posts complained that approaching Haskell by way of category theory is a "radical approach that would lead to elitism", since such an approach is likely to scare off all but the mathematical sophisticate.

That may or may not be true - in my opinion a well-written CT-oriented intro to Haskell need be no more terrifying than any other - but I take mild exception to the implied assertion that "elite" is somehow bad.

The community of Haskell programmers (and functional language programmers in general) is a natural, self-selecting elite. There's nothing wrong with that; on the contrary, the elite status of the Haskell Master should be celebrated. Haskell is hard, there's no sense in denying it, but so are most things worth doing. It's hard to master the piano, or fly-fishing, or brain surgery, or a foreign language, and nobody sensible would pretend otherwise. Why should the highly sophisticated art of functional programming be any different? Elite does not mean snide, or exclusionary, or condescending, or selfish; it means excellence, and the truly elite are open-minded, inclusive, and generous with their hard-earned knowledge.

I came to Haskell with years of imperative programming under my belt. I became a pretty "advanced" programmer, but I never really felt like I was doing anything a clever monkey couldn't do. A C programmer spends most of his time doing much what an auto mechanic does - diagnosing and fixing problems in a sophisticated machine. There's nothing wrong with being an auto mechanic or a C programmer; but it's not exactly an elite.

On my third try I've finally begun to appreciate the beauties of Haskell. The turning point for me was category theory, which lead to a sea change in my thinking. I'm not sure I'll ever become a master Haskell programmer - one of the great things about it is you can acquire a pretty good understanding of how the language works without writing Haskell programs - but it's clear that those who do master it are a different kind of programmer. Show me a great C programmer and I'll show you a Thomas Edison; show me a great Haskell programmer and I'll show you a J. S. Bach. (Idea for a logo: a measure of musical notation with a lambda clef, and notes tied by arrows.)

The message to newcomers should not be "don't worry, it's just like PHP, only different". It would be more honest to state right up front that this is a different game: entree to the elite is open to anybody, but not for free. You have no right to demand excellence without effort. You have to work; you have to master some mathematical ways of thinking that can in fact be difficult even for those with a good deal of math. You can do this; many others have. But if you're the type to throw a fit the first time you discover that your customary ways of thinking won't work, then please, go away. This is for grown-ups.

If you value excellence, and are motivated by the prospect of rising above the common dross and attaining excellence yourself, then you are in for a great intellectual adventure of deep insights and dazzling discoveries. And you will find lots of help. There is a plethora of material on the web that will help you, and the community of those who have gone before you is open and more than willing to help those in their apprenticeship.

In my experience the best, most imaginative and talented people are stimulated by a challenge to excel. They want the hard stuff, and they're the ones who should be evangelized.

The message to business people should be similar. No, Haskell is not PHP on steroids, it's a different beast altogether. It's a major paradigm shift, with major benefits that are well worth the costs. You hire expensive, highly-trained MBAs to professionally manage your company's financial assets; why would you not hire elite programmers to manage its information assets? The importance of husbanding knowledge assets to gain competitive advantage is only going to increase; treat it as mere data processing and your competitors will eat you alive. Yes, it's harder to find a good Haskell programmer than it is to find 100 mediocre PHP hackers, but aside from being more productive, the Haskell programmer comes with a disciplined, highly sophisticated way of thinking about information structures and algorithms. This makes it much more likely that your Haskell staff will do a much better job of figuring out how to turn your raw data into real capital that returns value.

(Fortunately I don't have any money riding on my sales pitch.)

by gargar

February 15, 2009 12:17 PM

Arch Haskell News

Functional reactive grapefruit


Grapefruit is a new suite of libraries for functional reactive-style GUIs layered on top of GTK (via gtk2hs), announced today. Besides being a modern FRP gui library, it notably uses arrow syntax to describe gui components.

Arrow syntax is a bit of a rarity in Haskell code:

    addA f g = proc x -> do
                    y <- f -< x
                    z <- g -< x
                    returnA -< y + z

Will build the computation:

All the components are packaged here for Arch Linux.

In other funky Haskell gui news, haskell-haha has also been released and packaged for Arch, and lets us do vector graphics in ascii in the terminal…. hell yeah!
Here’s a video of haha at work, and how to get it via cabal (yaourt also works fine):

by dons00 at February 15, 2009 08:22 AM

Mark Jason Dominus

Stupid crap, presented by Plato

Yesterday I posted:

"She is not 'your' girlfriend," said this knucklehead. "She does not belong to you."
Through pure happenstance, I discovered last night that there is an account of this same bit of equivocation in Plato's Euthydemus. In this dialogue, Socrates tells of a sophist named Dionysodorus, who is so clever that he can refute any proposition, whether true or false. Here Dionysodorus demonstrates that Ctesippus's father is a dog:

You say that you have a dog.

Yes, a villain of a one, said Ctesippus.

And he has puppies?

Yes, and they are very like himself.

And the dog is the father of them?

Yes, he said, I certainly saw him and the mother of the puppies come together.

And is he not yours?

To be sure he is.

Then he is a father, and he is yours; ergo, he is your father, and the puppies are your brothers.

So my knuckleheaded interlocutor was not even being original.


I gratefully acknowledge the gift of Thomas Guest. Thank you very much!

by Mark Dominus at February 15, 2009 06:40 AM

Stupid crap

This is a short compendium of some of the dumbest arguments I've ever heard. Why? I think it's because they were so egregiously stupid that they've been bugging me ever since.

Anyway, it's been on my to-do list for about three years, so what the hell.


Around 1986, I heard it claimed that Ronald Reagan did not have practical qualifications for the presidency, because he had not been a lawyer or a general or anything like that, but rather an actor. "An actor?" said this person. "How does being an actor prepare you to be President?"

I pointed out that he had also been the Governor of California.

"Oh, yeah."

But it doesn't even stop there. Who says some actor is qualified to govern California? Well, he had previously been president of the Screen Actors' Guild, which seems like a reasonable thing for the Governor of California to have done.


Around 1992, I was talking to a woman who claimed that the presidency was not open to the disabled, because the President was commander-in-chief of the army, he had to satisfy the army's physical criteria, and they got to disqualify him if he couldn't complete basic training, or something like that. I asked how her theory accommodated Ronald Reagan, who had been elected at the age of 68 or whatever. Then I asked how the theory accommodated Franklin Roosevelt, who could not walk, or even stand without assistance, and who traveled in a wheelchair.

"Huh."


I was once harangued by someone for using the phrase "my girlfriend." "She is not 'your' girlfriend," said this knucklehead. "She does not belong to you."

Sometimes you can't think of the right thing to say at the right time, but this time I did think of the right thing. "My father," I said. "My brother. My husband. My doctor. My boss. My congressman."

"Oh yeah."


My notes also suggest a long article about dumb theories in general. For example, I once read about someone who theorized that people were not actually smaller in the Middle Ages than they are today. We only think they were, says this theory, because we have a lot of leftover suits of armor around that are too small to fit on modern adults. But, according to the theory, the full-sized armor got chopped up win battles and fell apart, whereas the armor that's in good condition today is the armor of younger men, not full-grown, who outgrew their first suits, couldn't use them any more, and hung then on the wall as mementoes. (Or tossed them in the cellar.)

I asked my dad about this, and he wanted to know how that theory applied to the low doorways and small furniture. Heh.

I think Herbert Illig's theory is probably in this category, Herbert Illig, in case you missed it, believes that this is actually the year 1712, because the years 614–911 never actually occurred. Rather, they were created by an early 7th-century political conspiracy to rewrite history and tamper with the calendar. Unfortunately, most of the source material is in German, which I cannot read. But it would seem that cross-comparisons of astronomical and historical records should squash this theory pretty flat.

In high school I tried to promulgate the rumor that John Entwistle and Keith Moon were so disgusted by the poor quality of the album Odds & Sods that they refused to pose for the cover photograph. The rest of the band responded by finding two approximate lookalikes to stand in for Moon and Enwistle, and by adopting a cover design calculated to obscure the impostors' faces as much as possible.

This sort of thing was in some ways much harder to pull off successfully in 1985 than it is today. But if you have heard this story before, please forget it, because I made it up.


I would like to acknowledge the generous gift of Jack Kennedy. Thank you very much!

This acknowledgement is not intended to be apropos of this blog post. I just decided I should start acknowledging gifts, and this happened to be the first post since I made the decision.

[ Addendum 20090214: A similar equivocation of "your" is mentioned by Plato. ]

by Mark Dominus at February 15, 2009 06:40 AM

Erik de Castro Lopo

Ten Years of libsndfile.

Today, February 15th 2009, is the ten year anniversary of the first release of libsndfile.

Like most FOSS projects, libsndfile started off as an urge to scratch an itch. I was interested in Digital Signal Processing (DSP) and wanted an easy way to get digital audio into and out of software I was writing to try out various DSP algorithms. Secondly, I wanted to a sound file editor and one important part of such an editor is an ability to read and write various sound file formats. I did however look at a couple of existing sound file editors and found that most of them available at the time had buggy and incorrect WAV file handling. So I started out getting that part fixed. Nowadays, most sound file editors on Linux and many on other platforms use libsndfile for file I/O.

In its 10 years of existence, libsndfile has grown from some 5000 lines of code to over 45000 lines of code (not counting the test suite and the example programs). The earliest versions could read WAV, AIFF and AU file formats while the latest version supports 25 formats and is still growing.

It was originally written to run on Linux and other UNIX-like systems but soon ended up running on windows and Mac OS9 (the old non-Unix Apple Macintosh) operating system. Fortunately Mac OS9 has been assigned to the dustbin of history leaving windows as the only operating system that was difficult or painful to support. Recently, the windows development has moved to a system where the only way I support building of libsndfile for that OS is to cross compile from Linux, with the test suite being run under Wine. This has made my life significantly easier since I also release pre-compiled windows binaries.

One surprise for me was that a Wikipedia entry as added in 2006. The page says:

"libsndfile is a widely-used [citation needed] C library"

and I think that the ten year anniversary of the first release may be a good time to look at where libsndfile is actually being used. With a little research and some help from the libsndfile mailing lists, this is what I found (in no particular order):

  • Major computer music programming language and environments such as ChucK, Csound, MusicKit, Nyquist, PureData, and SuperCollider. Most of these apps are cross platform and require the use of libsndfile on all the platforms they support.
  • Ardour, the premier cross platform (*nix and MacOSX), Free Software Digital Audio Workstation
  • Audacity, the ubiquitous, cross platform (*nix, Mac and windows) audio editor.
  • The Pulse Audio sound server uses libsndfile and is part of most modern Linux systems running the Gnome environment and hence libsndfile is installed by default on all those systems.
  • Linux media players like Alsaplayer, Aqualung, Audacious, MPlayer and XMMS, either by default or as an optional plugin.
  • Winamp one of the more popular and certainly one of the oldest media players on the windows platform.
  • The Ecasound, Ecawave and Ecamegapedal suite of Free Software programs.
  • The Levelator, a tool for podcasters that automatically adjusts the levels of spoken-word recordings (Windows, Mac and Linux).
  • Linux and Unix sound file editors like Sweep and MhWaveEdit.
  • Overtone Analyzer, a sound visualization tool for singing teachers, speech therapists, instrument builders and overtone singers.
  • Linux based software audio synthesizers and samplers such as the Amsynth software synthesizer, Freecycle, Freewheeling, the Galan synthesis environment, Horgand, the Hydrogen drum machine, Sooperlooper, and the Specimen sample player.
  • Linux trackers like Aldrin and Soundtracker.
  • Mixxx, the Linux DJ program.
  • The FreeSWITCH open source communications platform which runs natively on Windows, Mac OSX, Linux, *BSD, and other Unix flavors.
  • The Baselight (commercial product) colour grading system used worldwide for commercials, episodic television and feature film digital intermediate.
  • Linux based audio/midi sequencers like GNUSound, MusE, Qtractor and Wired.
  • APTDecoder, Free Software (GPL) for recording and decoding signals transmitted by NOAA POES APT enabled weather satellites.
  • The One Laptop Per Child machines come with CSound and hence also include libsndfile.
  • X Lossless Decoder, a Lossless audio decoder for Mac OS X.
  • As part of Meyer Sound's Wild Tracks hard-drive based multitrack audio playback and recording system.
  • AudioMove a GUI-based batch audio file converter/copier program (GPL).

On top of that there are language bindings for Fortran 77, Free Pascal, Haskell, Perl, Python ( PySndfile, AudioLab, libsndfile-python and possibly others ), Ruby and probably many others.

Overall its been a fun ten years. I've learnt a lot about writing reliable and portable cross platform code and become a much better coder for it. Having libsndfile as a hobby project has definitely helped my employment prospects and my career as a professional software engineer.

The next ten years of libsndfile will mainly be maintenance, but new file formats (I'm currently working on Ogg/Speex) and features will be added as needed.

February 15, 2009 12:31 AM

February 14, 2009

Magnus Therning

Well-Typed.Com

Cabal ticket #500

I just opened the 500th Cabal ticket! What, you mean there’s no prize?

I’ll ignore the possibility that this is a sign that Cabal is full of bugs and take the positive view that 500 tickets is a sign of an active, useful project. Nobody bothers complaining about useless projects.

As it happens, the 500th ticket is not a bug but an idea for a project. There are over 1,000 packages on Hackage now and the question is how many of them can be installed simultaneously? This is not just an idle statistic. If two packages cannot be installed with consistent dependencies then it is unlikely that you can use both together in your next project. That is of course a wasted opportunity for code re-use.

The idea is if we can work out the set of packages on Hackage that can all be installed together consistently then we can mark package pages with that information. Basically we would be handing out brownie points. Hopefully we can also influence maintainers of other packages to adjust their dependencies so that their package can also join the happy collection of packages that can all agree on their dependencies.

Actually calculating the maximal set of consistent packages is a bit tricky. It is almost certainly NP-complete in general but in practice is probably doable and we can probably live with approximations.

In fact it might make quite a good Haskell.org Google Summer of Code project. If you are interested, get in touch.

by duncan at February 14, 2009 07:02 PM

Mark Jason Dominus

The junk heap of (blog) history

A couple of years ago, I said:

I have an idea that I might inaugurate a new section of the blog, called "junkheap", where unfinished articles would appear after aging in the cellar for three years, regardless what sort of crappy condition they are in.
Some of the stuff in the cellar is in pretty good shape. Some is really trash. I don't want to publish any of it on the main blog, for various reasons; if I did, I would have already. But some of it might have some interest for someone, or I wouldn't be revisiting it at all.

Here's a summary of the cellared items from February-April 2006, with the reasons why each was abandoned:

  1. Two different ways to find a number n so that if you remove the final digit of n and append it to the front, the resulting numeral represents 2n. (Nothing wrong with this one; I just don't care for it for some reason.)

  2. The first part in a series on Perl's little-used features: single-argument bless (Introduction too long, I couldn't figure out what my point was, I never finished writing the article, and the problems with single-argument bless are well-publicized anyway.)

  3. A version of my article about Baroque writing style, but with all the s's replaced by ſ's. (Do I need to explain?)

  4. Frequently-asked questions about my blog. (Too self-indulgent.)

  5. The use of mercury in acoustic-delay computer memories of the 1950's. (Interesting, but needs more research. I pulled a lot of details out of my butt, intending to follow them up later. But didn't.)

  6. Thoughts on the purpose and motivation for the set of real numbers. Putatively article #2 in a series explaining topology. (Unfinished; I just couldn't quite get it together, although I tried repeatedly.)

I would say that the aggregate value of these six articles is around 2.5 articles-worth. In all, there are 23 items on the junkheap of calendar year 2006.

I invite your suggestions for what to do with this stuff. Mailing list? Post brief descriptions in the blog and let people request them by mail? Post them on a wiki and let people hack on them? Stop pretending that my every passing thought is so fascinating that even my failures are worth reading?

The last one is the default, and I apologize for taking up your valuable time with this nonsense.

by Mark Dominus at February 14, 2009 06:48 PM

Gregg Reynolds

Pernicious Myth No. 1: The Container Fiction

Newcomers to Haskell quickly learn that lots of containers are involved. Lists and tuples are containers; a monad is like a container; constructed data contain the arguments used in construction, and so forth.

It's a useful fiction, but it is a fiction. A value of type "[a]" does not contain values of type 'a', or anything else, for that matter. The Container Fiction is pernicious insofar as it retards progress toward a deeper understanding of how the notation works and why category theory provides such a powerful semantic framework.

All values are ontologically primitive.

This is obvious if you look at "simple" values like integers. Is 3 primitive? Some mathematicians would disagree. The number three, they might argue, is constructed using {} and a successor function. Or they might argue that it's a sequence of lambda expressions of some kind. There are probably lots of other ways to describe the meaning of '3' using various mathematical constructions.

These are all just different ways of describing a mathematical object; but as one of my college professors (expert in comparative religion) was fond of saying, map is not territory. Description of an object does not an object make. If these various and sundry descriptions all describe the same thing, then that thing must be independent of the descriptions.

Constructive mathematics does not construct its objects, it describes them. It would be the height of hubris to suggest otherwise; after all, numbers do not depend on the exertions of mathematicians for their continued existence.

The vitality of the Container Fiction demonstrates the power of the Iconic Fallacy. Values do not contain, but syntactic expressions do. We think that an ordered pair (a,b) contains a and b. It doesn't, but the graphical form, using parentheses, strongly implies that containment is involved. This is the Iconic Fallacy: false inference about the nature of the thing signified drawn from the form of the signifier. An expression like [1,2,3] "looks like" a list of integers; it does not therefore follow that it is (or denotes) a list of integers. It would be more accurate to say it is a construction that uses a list of integers to denote a value. The expression "[1,2,3]" represents application of a morphism (the [] functor) to an argument; if its denoted value contains 1, 2, and 3, then does the denoted value of \sqrt 4 contain 4?

Part of the problem is that "List" (i.e. []) is misnamed, implying that '[a]' is a list. It's named after the target end of the arrow; a proper name would be something like "TypToList", thus emphasizing that it is a morphism.

This may seem like so much philosophical splitting of hairs, but it's not. On the contrary, it correlates with one of the fundamental insights of category theory, namely, elements don't matter. I believe it's very important for learners of Haskell (or any FPL with lazy evaluation) not only to learn to think in terms of mathematics, but also to learn to think about how mathematical notation works. I speak from experience; when I first picked up Haskell I used a book that insisted that something like "x = Foo 1 (2,3) 'a'" means that x contains 1, and (2,3), and 'a'. That didn't match up with the ideas I had formed about algebraic data types, so I eventually ended up dropping the whole thing in exasperation.

More specifically: it's important (essential?) to realize that we can only talk about values indirectly. On the one hand that means we have to use a language with syntax, obviously. But it's deeper than that. We can only talk about mathematical objects by "triangulating" using other, related mathematical objects. As a concrete example consider an ordered pair (1,2). Disregarding syntax, lambda expressions, etc., the value (1,2) is a primitive object that is the image of 1, 2 under the mapping ( ). The only way we can talk about it is to use these three things. Not the "contents" of (1,2) - it has no contents - but the things we used to construct (describe) it , which are completely distinct from the thing itself.

The most important reason to learn to think like this is that it is the primary idiom of category theory. For example, in CT terms, something like (1,2) is treated as an opaque object together with two projection arrows fst and snd. No contents involved, just an object and two mappings. The internal structure of the object is irrelevant. Saunders MacLane says somewhere that CT is about "learning to live without elements"; applied to Haskell, that means learning to live without containers.

by gargar

February 14, 2009 03:35 PM

London Haskell Users Group

Next Meeting: Lemmih (David Himmelstrup) on LHC

The next meeting of the London Haskell User Group will be on Friday 20th February from 6:30PM at City University. Apologies for the short notice.

Lemmih (David Himmelstrup) will be talking about LHC, a recent fork of the JHC compiler. Full title and abstract to follow.

As usual see the venue page for full location information.

by ganesh at February 14, 2009 01:38 PM

Erik de Castro Lopo

Security Hyperventilating.

Just today, David Cournapeau and Lev Givon found a bug in all versions of libsamplerate up to and including 0.1.6. The bug causes a segfault and is basically the same as a bug I thought I fixed last year that resulted in the following entry in the ChangeLog:


  2008-07-02  Erik de Castro Lopo  <erikd AT mega-nerd DOT com>

     * src/src_sinc.c
     Fix buffer overrrun bug at extreme low conversion ratios. Thanks to Russell
     O'Connor for the report.

That bug fix went into version 0.1.4 of libsamplerate which was released on July 2nd, 2008. As a result, I was contacted by computer security firm Secunia Research on July 3rd and asked the following questions:

  • What is the maximum impact of this "buffer overrun"?
  • Can this be exploited by malicious people to e.g. cause a DoS (Denial of Service) or compromise a vulnerable system?
  • Under which circumstance is this exploitable and are there any mitigating factors?

I replied with a reasonably full explanation and stated that while this bug, if triggered, would crash the program, it was not, in my opinion, exploitable. Secunia Research was happy with my explanation and analysis and I thought that was that.

However, in November of 2008 there was a flurry of security advisories which quoted the above ChangeLog entry but got the security implications completely wrong. The curious thing was that no-one, not a single person contacted me or the project mailing list to ask about the severity of the problem.

The earliest of these advisories I can find was dated November 3rd and appeared on the Openwall OSS-Security mailing list. However, by December 2nd, the Gentoo security team was saying:

"A remote attacker could entice a user or automated system to process a specially crafted audio file possibly leading to the execution of arbitrary code with the privileges of the user running the application."

I on the other hand, remain convinced that this bug is not exploitable under anything other than purely theoretical circumstances.

Since I have now found another variant of the same bug I decided I should document the problem more fully than last time. The problem occurs deep in a rather complicated piece of code that looks like this:


  static void
  prepare_data (SINC_FILTER *filter, SRC_DATA *data, int half_filter_chan_len)
  {   int len = 0 ;
  
      /* Calculation of value of len elided. */
  
      len = MIN (filter->in_count - filter->in_used, len) ;
      len -= (len % filter->channels) ;
  
      memcpy (filter->buffer + filter->b_end, data->data_in + filter->in_used,
                          len * sizeof (float)) ;

The problem is that under conversion ratios near the lower bound of allowed values, the variable len can end up as a small negative value (I saw values in the range [-20, -1]). That small negative number then gets multiplied by 4 (sizeof float) and then passed as the third parameter to memcpy.

However, the third parameter to memcpy is of type size_t which is an unsigned value the same size as sizeof (void*). In the C programming language, when a small signed value is converted to an unsigned value, it gets converted into a very large positive value very near the maximum representable positive unsigned value, ie 4Gig on 32 bit systems or 2 to the power of 64 on 64 bit systems.

Due to the conversion, the memcpy tries to write to a huge chunk of memory (nearly 4 Gig on 32 bit systems, and a hell of a lot more on 64 bit systems). Under a protected memory system (Linux, Windows NT or later and Mac OSX), the only way this bug could possibly exploitable would be if the memcpy returns.

However, since the memcpy is trying to overwrite the vast majority of the CPU's memory space, the chances of the memcpy returning are essentially zero for any sane operating system. Instead, the process containing the call into libsamplerate will attempt to write outside its allocated memory space and will therefore be terminated by the operating system with a segmentation fault.

I have now fixed the function containing the memcpy so that it checks the value of len and returns from the function if it is outside a sane range.

Now I do think that security researchers and security specialists at Linux distributions do a very important and rather thankless job. I also think that in this case some of them fell down rather badly. Secunia Research did the right thing and asked me about the implications of the bug. The others, extrapolated incorrectly, from very little information and got it wrong, without ever contacting me. I'm hoping that the ChangeLog entry (below)


  2009-02-14  Erik de Castro Lopo  <erikd AT mega-nerd DOT com>

      * src/src_sinc.c
      Fix a segfault which occurs when memcpy is passed a bad length parameter.
      This bug has zero security implications beyond the ability to cause a
      program hitting this bug to exit immediately with a segfault.
      See : http://www.mega-nerd.com/erikd/Blog/2009/Feb/14/index.html
      Thanks to David Cournapeau.

will prevent the kind of security hyperventilating I saw last time. The new version of libsamplerate, version 0.1.7, has just been released.

Update : 2009-02-15 11:19

David Cournapeau informs me that Lev Givon, as a user of David's libsamplerate Python bindings, reported this bug to him and that it was actually Lev that found the bug.

February 14, 2009 11:58 AM

apfelmus

Random Permutations and Sorting

Introduction

The standard algorithm for shuffling a deck of cards, or generating a random permutation of a finite set with n elements in general, is the Fisher-Yates shuffle. Conventionally, the elements are stored in a mutable array and then randomly swapped a few times. More specifically, they are swapped n times, so the algorithm runs in O(n) time. Of course, the point is that these swaps are chosen carefully such that each permutation is equally likely.

In a message to the Haskell beginners mailing list, Jan Snajder presented a short program that implements exactly this, with mutable arrays and all. His post made me wonder whether there is a purely functional way to do this, one without mutable arrays and indexes but with similar time complexity?

Yes, there is! The main idea is that shuffling a list is essentially the same as sorting a list; the minor difference being that the former chooses a permutation at random while the latter chooses a very particular permutation, namely the one that sorts the input. In other words, the idea is to take a generic sorting algorithm like merge sort and turn it into a shuffle algorithm by simply replacing each comparison with a random choice.

Thus, in the following article, we are going to transform merge sort into a random permutation generator.

Random Numbers

Before we begin, a few words about random number generation. Jan used the IO monad to obtain random numbers, giving the shuffle algorithm the type

permute :: [a] -> IO [a]

This is both pretty and ugly at the same time; ugly in that IO is used as ragbag for side effects that don't seem to fit elsewhere, but pretty in that the usual procedure of carrying around and updating a random seed is hidden behind an abstraction. We will drop the ugly part by using a new monad R

permute :: [a] -> R [a]

which works like IO but allows only random number creation. In other words, the only side effects available in R are functions like

getRandomR :: (Int,Int) -> R Int

which generates a random integer in the given range.

Note that the restriction to random numbers gives R a a meaning on its own; we can interpret R a as "a collection of values a of which one will be picked at random when the program is run" or for the mathematically inclined as "a random variable of type a".

You can implement it as type R a = IO a if you like, but we will use the MonadRandom package and set

import Control.Monad.Random
type R a = Rand StdGen a

Samples can be generated with the functions evalRand and evalRandIO.

Merge Sort

Recall how merge sort works: the list is divided in half, both halves are sorted individually and then merged to give the result. Let us capture the second phase of the algorithm with a designated data type SortedList a that represents sorted lists. Of course, we can simply implement it as ordinary list, with the convention that the elements appear in order:

type SortedList a = [a]

empty :: SortedList a
empty = []

singleton :: a -> SortedList a
singleton x = [x]

merge :: Ord a => SortedList a -> SortedList a -> SortedList a
merge []     ys     = ys
merge xs     []     = xs
merge (x:xs) (y:ys) =
    if x <= y
        then  x : ( xs  `merge` y:ys)
        else  y : (x:xs `merge`  ys )

With these preliminaries, the whole algorithm reads:

mergesort :: Ord a => [a] -> SortedList a
mergesort = fromList
    where
    fromList []  = empty
    fromList [x] = singleton x
    fromList xs  = (fromList l) `merge` (fromList r)
        where (l,r) = splitAt (length xs `div` 2) xs

Random Lists

To generate random permutations, we now replace sorted lists with "random lists", i.e. some kind of list structure that presents its elements in random order. The straightforward choice

type RandomList a = R [a]

will do the trick. Trivially, we have

empty :: RandomList a
empty = return []

singleton :: a -> RandomList a
singleton x = return [x]

Merge

Now, we want to merge random lists. This process is entirely analogous to merging sorted lists: we select the first element and then combine the tails with merge. But instead of always putting the smallest element in front, we toss a coin and select an element at random. In Haskell pseudo code, this would look something like this:

merge (x:xs) (y:ys) = do
    k <- getRandomR (1,2)   -- toss a coin
    if k == 1
        then  x : ( xs  `merge` y:ys)
        else  y : (x:xs `merge`  ys )

That being said, giving each list an equal probability of 1/2 is unfair when the lists have different sizes. For instance, if the first list has only 1 element and the second list is a random permutations of 5 elements, then the single element would have a probability of 1/2 to appear as first element in the result. In a fair permutation, this probability should be only 1/6.

The selection can be made fair if we weight the lists by their sizes. In our example, this means giving the first list a probability of 1/(5+1) and the second one a probability of 5/(5+1). By keeping track of the list sizes and adjusting the random selection accordingly, we obtain the following implementation:

merge :: RandomList a -> RandomList a -> RandomList a
merge rxs rys = do
        xs <- rxs
        ys <- rys
        merge' (length xs, xs) (length ys, ys)
    where
    merge' (0 , [])   (_ , ys)   = return ys
    merge' (_ , xs)   (0 , [])   = return xs
    merge' (nx, x:xs) (ny, y:ys) = do
        k <- getRandomR (1,nx+ny)
        if k <= nx
            then (x:) `liftM` ((nx-1, xs) `merge'` (ny, y:ys))
            else (y:) `liftM` ((nx, x:xs) `merge'` (ny-1, ys))

Clearly, this function needs O(n) time to merge two random lists.

Permute

The final algorithm to generate a random permutation has exactly the same structure as merge sort:

permute :: [a] -> RandomList a
permute = fromList
    where
    fromList []  = empty
    fromList [x] = singleton x
    fromList xs  = (fromList l) `merge` (fromList r)
        where (l,r) = splitAt (length xs `div` 2) xs

And just like merge sort, this implementation will take O(n log n) time to generate a random permutation. After all, the new merge has the same time complexity and the old analysis applies.

The time complexity may seem like a regress compared to O(n) for the Fisher-Yates shuffle, but the connection to sorting shows that without arrays, O(n log n) is optimal. After all, there are n! permutations in total, so we need at least O(n log n) bits to encode them and we will need equally many steps to pick one if we may only decide one bit at a time.

Where to go from here

I hope you have enjoyed this excursion into sorting and functional programming. For your convenience, I have packaged the implementation of random lists into a tiny module.

I would like remark that it is Haskell's first class treatment of computations like R a that makes the RandomList abstraction possible at all. Also, purity is a boon; I don't think that an impure language treating random numbers as a side effect can convey the abstraction of random variables R a this convincingly.

Quicksort

Merge sort is not the only sorting algorithm that can be turned into a random permutation generator. How about trying the same with quicksort?

Fairness

The merge function looks fair, but can you actually prove that? Probabilistic Functional Programming by Erwig and Kollmansberger to the rescue! Available on Hackage.

Incremental Generation

I'll end with another challenging problem: how about an incremental algorithm that generates random elements on demand? For instance, we want

head `liftM` permute

to return a random element in O(n) time and

take k `liftM` permute

to return elements in say O(n + k log n) time.

For sorting, this question is explored in Quicksort and k-th Smallest Elements. Note that the merge sort implementation presented here is too inefficient at constructing the call tree for merge.

Also, the RandomList implementation has to be changed unless the random monad R is sufficiently lazy. In the spirit of Inductive Reasoning about Effectful Data Types by Filinski and Støvring, try a variant of

data RandomList a = Nil | Cons (R (a, RandomList a))

to achieve the desired behavior.

February 14, 2009 10:49 AM

Darcs

darcs weekly news #5

2009-02-14 This is a back-posting of an older darcs weekly news article from before the creation of blog.darcs.net. I'll be trickling these in to minimise disruption to people's RSS readers

News and discussions

  1. Second pre-release of darcs 2.1.0 (formerly known as 2.0.3) This version of darcs will produce darcs-2 format repositories by default
  2. New issue manager - Thorkil Naur. The darcs team now has an official Issue Manager role. Thorkil will be ensuring that incoming reports are responded to in a timely manner, and that all bugs are eventually moved to a resolved state.
  3. Hoogling the darcs source?

Issues resolved in the last week (5)

issue27 David Roundy
issue53 Eric Kow
issue805 David Roundy
issue1039 Dmitry Kurochkin
issue1041 Vlad Dogaru

Patches applied in the last week (54)

See text entry for details.

by kowey (noreply@blogger.com) at February 14, 2009 10:47 AM

February 13, 2009

GHC / OpenSPARC Project

Refactoring

untie the knots
soften the glare
write the program
that was always there

by Ben Lippmeier (noreply@blogger.com) at February 13, 2009 08:40 PM

Gregg Reynolds

Fixing Haskell IO

No, Haskell IO isn't broken; that's just a shameless bid for attention. But the metalanguage commonly used to describe Haskell IO is broken.

Here are a few typical examples of how IO in Haskell is described:

A value of type IO a is an “action” that, when performed, may do some input/output, before delivering a value of type a. (Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, p. 5)

a type IO a denoting actions that when performed may do some IO and then return a value of type a. (Imperative Functional Programming, p. 3)

The key idea is to treat a value of type IO a as a “computation” that, when performed, might perform input and output before delivering a value of type a. (A History of Haskell: Being Lazy With Class, p. 25):

We can summarize the SDIOH (Standard Definition of IO in Haskell) as "a value of type IO a is a value, that performs, then delivers a value of type a".

Now consider how one might describe a run-of-the-mill non-IO value: "a value of type T a is … a value of type T a". All definitions are tautologies. By definition. If the SDIOH is a true definition, then IO values are not like other values, and we have a two classes of value in Haskell. If it is not a tautology, then it is not a definition, and we still don't know what an IO value is.

Since it is clearly undesirable to have two different kinds of value, it must be that the SDIOH is in fact not a definition. Then what is an IO value?

Part of the problem with the SDIOH is its use of ambiguous terms. It's impossible to discern exactly what it means by "value" and "computation". But that's only part of the problem. The deeper problem, which is related to the terminological problem, is that the semantic model (for lack of a better term) behind the SDIOH adopts a particular perspective on the semantic operations involved in evaluation that forces us to mix being and doing.

The current idiom portrays an IO value as an agent that dynamically performs some kind of action. The GHC implementation of IO operators express this concretely by modeling IO as a state transformer that acts on the RealWorld. This "works" well enough; GHC manages to perform IO. But it doesn't fly mathematically. Mathematical objects never act, sing, dance, or do anything. They just are. A value that acts is an oxymoron.

Fixing this requires a shift in perspective and a more refined elaboration of the mental model we use to think about IO in Haskell. The trick is to reverse the perspective. Instead of viewing the program as an agent that acts on the world, we view the world as an agent that provides an interpretation for program. We refine the model by dividing semantics into two parts: internal semantics encompass the mapping from Haskell expressions to lambda expressions, along with lambda conversion of expressions; the external semantics cover the assignment of an interpretation to the lambda expressions.

For example, we can account for the semantics of '3' as follows: the internal mapping takes the Haskell expression '3' to the lambda expression '_3' (using prefixed _ to mark symbols in the metalanguage). The World in turn interprets the program text, mapping '_3' to the integer of that value. If we wish we can define a World metalanguage. Using a Haskell-like syntax, we say '_3' is interpreted as "Z 3" of type "W Z Int".

This gives us a clear, simple account of the semantics of IO values without any notion of action. An IO a value is just an IO a value; no different than any other kind of value. Semantics comes from interpretation. The internal semantics map non-IO expressions to constant (bound) lambda expressions. To account for IO expressions, we use lambda variables. For example, "getChar" maps to something like $v : IO Char$ (assuming our metalanguage uses : to indicate type). In other words, the internal semantics takes an IO expression to a free variable in the metalanguage. Now free variables range over all values of their type; so the World's interpretation of such a free variable is the set of mappings from the variable to the World values of the World type corresponding to the argument of the IO type (the 'a' in IO 'a'). In other worlds, the set of all possible bindings of $v : IO Char$ to World values of type "World Char"; for getChar, something like "Char 'c'".

The meaning of the program then becomes the set of all possible World interpretations of it. The notion of actors and actions has been completely eliminated. The notion of "value of type IO a" has been replaced by a description of the way IO expressions are interpreted. The SDIOH is replaced by something like:

An expression of type IO a is bound to a free variable in the metalanguage, which is bound to a (World) value of type a in each interpretation of the program

Naturally, for this to work we would need to rework other parts of the metalanguage, and we would want to come up with some kind of metalanguage for referring to World types and values. In particular, we need to complement the definition of IO values with a definition of (non-IO) values:

a expression of type T a is bound to an expression in the metalanguage that contains no free variables …

This definition would have to be refined, but the basic idea is to distinguish between lambda expressions whose Head Normal Forms have a constant binding to World values, and those that are free.

  • the role of the lambda calculus as a metalanguage is made explicit
  • IO expressions bind to free vars in the lambda metalanguage
  • a World metalanguage provides a model for interpretations
  • Executing a program means having the World give it an interpretation

by gargar

February 13, 2009 05:26 PM

"FP Lunch"

Djinn, monotonic

On my way to check the plumbing, I dropped in to see how people were doing and told a bit of a story about proof search in implicational logic. You may have encountered the problem before in the context of Roy Dyckhoff’s contraction-free sequent calculi, which Lennart Augustsson turned into Djinn. Here’s a Haskell rendering of the basic idea. An implicational formula is an atom or an implication.

data Fmla
  = Atom Atom
  | Fmla :-> Fmla

type Atom = String

Let’s write a checker to see if a Fmla follows from a bunch of hypotheses. Step one, introduce the hypotheses, reducing the problem to testing if an atom holds.

fmla :: [Fmla] -> Fmla -> Bool
fmla hs (h :-> g) = fmla (h : hs) g
fmla hs (Atom a) = atom hs a

Step two: scan the hypotheses, trying to derive the atom from each.

atom :: [Fmla] -> Atom -> Bool
atom hs a = try [] hs where
  try js [] = False
  try js (h : hs) = from h a (js ++ hs) || try (h : js) hs

Step three: test whether a given hypothesis (&lsqhoin the stoup’) delivers the atom.

from :: Fmla -> Atom -> [Fmla] -> Bool
from (Atom b) a hs = b == a
from (g :-> h) a hs = from h a hs && fmla hs g

That’s to say, to use an implicational hypothesis, show the premise holds and use the conclusion. But from which context should we show the premise? If you look carefully, you’ll see that atom passes in the whole of its context, bar the hypothesis in the stoup. That stops us getting in a loop when we try to deduce A from (A → A). We haven’t thrown away any theorems, because any proof which uses the same hypothesis twice on a path in the tree can be shortened to cut out the loop.

But is that enough to ensure termination? Sure is. How might we see that? The problem is quite nasty, because if we want to show

(A → B → C) → D, A → C |- D

backchaining actually increases the length of the context: we end up showing

A → C, A, B |- C

but even so, you might get the feeling that the problem is getting smaller somehow. And you’d be right: we got rid of a higher-order hypothesis but acquired more at lower order. We can make that clear with a wee bit of indexing.

Here are formulae, now in Agda:

data Fmla : Nat -> Set where
  atom : Atom -> {n : Nat} -> Fmla n
  _=>_ : {n : Nat} -> Fmla n -> Fmla (suc n) -> Fmla (suc n)

The index is a loose bound on the order (arrow-left-nestedness) of the formula. Never use tight bounds when loose bounds will do—it’s too much hassle keeping tight bounds accurate. Now we can collect formulae in buckets according to their order. Let’s use this handy structure

Tri : (Nat -> Set) -> Nat -> Set
Tri T zero     = One
Tri T (suc n)  = T n * Tri T n

which I’ve defined recursively today for ease of iso. To see why these are sort-of triangles, instantiate T to vectors. Also T = Fin·suc goes with a bang! But I digress… Vectors can be seen as degenerate triangles.

Vec : Set -> Nat -> Set
Vec X = Tri \ _ -> X

Now we can say what a bucket of formulae of a given order might be.

List : Set -> Set
List X = Sig Nat (Vec X)   -- Sig is the usual dependent pair type
Bucket : Nat -> Set
Bucket n = List (Fmla n)

And now a context is a triangle of buckets:

Ctxt : Nat -> Set
Ctxt = Tri Bucket

So our checker repeatedly makes higher-order buckets smaller, at the cost of making lower-order buckets larger, but that’s a perfectly respectable way to be monotonically decreasing.

Agda’s termination checker isn’t so good at spotting that this is what’s going on, but before we had Agda’s bag on the side, there was a language called Epigram which resorted to Type Theory as its language for explaining termination. Gasp!

It’s gone 5pm on Friday and I’m still in school. (Thorsten and Graham are away today: they’d never allow this!) I’m just going to link to this inscrutable lump of code and finish this post later.

by Conor at February 13, 2009 05:19 PM

Gregg Reynolds

"Computation" considered harmful. "Value" not so hot either.

The term "computation" has at least six different senses, all of which are commonly used in technical literature:

  • a dynamic computing process
  • the result of a computational process
  • an algorithm that describes a computational process
  • a formal description of an algorithm in a specific language
  • a formal description of the semantics of a computational process; e.g. a lambda expression
  • a dynamic process that converts a lambda expression to normal form
  • a formal description of lambda conversion

One could probably come up with additional technical uses for the term. Even worse, "computation" is an ordinary word with well-understood if inexact semantics. Readers come to a technical text with a well-formed idea of what the word means, and thus no reason to think their notion is incorrect.

"Value" is even worse. It too carries multiple technical meanings in the literature, and it is even more common in ordinary language. Same for "evaluation".

These terms are ambiguous. They should be banned from technical discourse.

Usually this ambiguity is tolerable, at least for subject matter experts. But when it becomes a problem, it's a big problem. It cost me many exasperating hours of head-scratching when I decided to finally get to the bottom of monads and IO in Haskell.

The texts that flummoxed me are Moggi's paper on "notions of computation" and the standard idiom used to describe IO in Haskell.

Moggi (Notions of computation and monads, p. 3):

In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation , since it abstracts away from the type of values computations may produce.

A typical example of how IO is described in Haskell (A History of Haskell: Being Lazy With Class, p. 25):

The key idea is to treat a value of type IO a as a “computation” that, when performed, might perform input and output before delivering a value of type a.

Obviously this language is "good enough", since Moggi's paper was very influential, and Haskell is very successful. But both passages immediately struck me as hazy and somewhat absurd. Try as I might, I could find no way to assign a precise meaning to them. It took a lot of research and a flurry of messages on the haskell-cafe mailing list to figure out why they didn't work for me and discover what the authors (probably) meant.

Needless to say, part of the problem was the ambiguity of the terms "computation" and "value". I came to the texts thinking that a value is either a "datum" like 3 or a function like sqrt. They're just static mathematical objects, so I could not conceive of how a value could "be" a computation, or could "be performed".

The scales fell from my eyes when I came across the following passage buried in the Wikipedia article on Theory of Computation:

A computation consists of an initial lambda expression (or two if you want to separate the function and its input) plus a finite sequence of lambda terms, each deduced from the preceding term by one application of Beta reduction.

I was already familiar with the lambda calculus, but I had never thought of a lambda expression as a "computation". I still don't like it; a lambda expression is not a computation, it's a formal representation of a mathematical object (a value). Lambda conversion is a purely syntactic calculation that yields a different notational representation of the same value. The lambda calculus is a formal model of computation; the same computation could be represented in a different formalism. So it's just wrong to say that a computation is a sequence of lambda expressions.

Nonetheless, it's clear why one might think in these terms and use this language, and I think that is what's going on in the passages quoted above. My ideas of computation and value were based on the idea of a direct mapping from expression to mathematical object. Even though I was quite familiar the notions of language and metalanguage, I thought of a metalanguage as serving mainly to clarify meaning; once you understand the semantics of the language, you can disregard the metalanguage and think directly in terms of abstract semantic objects (e.g. numbers and functions.)

But in Haskell that's not good enough; to understand how lazy evaluation works, you need to keep lambda calculus (or the equivalent) in mind, because denotation has to pass through lambda expressions in various states of reduction before arriving at normal form and then semantic objects. You cannot disregard the lambda metalanguage, because the different forms lambda expressions may take constitute part of the semantic universe. Make it explicit and things become more clear. The above definition of Haskell IO becomes:

The key idea is to treat a value of type IO a as a “lambda expression” that, when converted to normal form, might perform input and output before delivering a value of type a.

Unfortunately, that's not good enough: how can a lambda expression in normal form "be performed" and "deliver" a value?

That is the subject of my next post, wherein I will discuss weaknesses in Haskell's informal metalanguage and suggest replacements for "computation", "value", and "evaluation".

by gargar

February 13, 2009 03:50 PM

Darcs

darcs weekly news #6

2009-02-13 This is a back-posting of an older darcs weekly news article from before the creation of blog.darcs.net. I'll be trickling these in to minimise disruption to people's RSS readers

News and discussions

  1. Third pre-release of darcs 2.1.0. Release pushed back to 17 October latest for more testing. We're getting very close to the finish line!
  2. Darcs ideas in other VCS. Kirill Smelkov has kind words for us on behalf of the NAVY project, which is moving away from darcs. Best of luck to Kirill with whatever revision control system NAVY choose! While we are delighted that "Good ideas behind [darcs] were adopted by youth", we still have a thing or two to show these whippersnappers.
  3. Haddock + Hoogle == Javadoc on steroids. Simon Michael has combined haddock and hoogle to give us a lovely darcs code browser. In the meantime, Florent Becker has been adding value to this browser by sending in lots of haddock patches. Many thanks to Simon and Florent!
  4. Patch theory update. Ian gives us his latest progress on documenting, prototyping and improving darcs patch theory. "[S]ome proofs are finally starting to appear, albeit rather handwavey for now". Go Ian!

Reviewers

Thanks to our patch reviewers for this week for giving David a hand!

  • Simon Michael

Issues resolved in the last week (5)

issue1003 David Roundy
issue1043 David Roundy
issue1078 Dmitry Kurochkin
issue1102 Eric Kow
issue1110 David Roundy

Patches applied in the last week (47)

See text entry for details.

by kowey (noreply@blogger.com) at February 13, 2009 02:15 PM