Lambda the Ultimate

Parallel Haskell programming has entered the mainstream with support now included in GHC for multiple parallel programming models, along with multicore execution support in the runtime. However, tuning programs for parallelism is still something of a black art. Without much in the way of feedback provided by the runtime system, it is a matter of trial and error combined with experience to achieve good parallel speedups. This paper describes an early prototype of a parallel profiling system for multicore programming with GHC. The system comprises three parts: fast event tracing in the runtime, a Haskell library for reading the resulting trace files, and a number of tools built on this library for presenting the information to the programmer. We focus on one tool in particular, a graphical timeline browser called ThreadScope. The paper illustrates the use of ThreadScope through a number of case studies, and describes some useful methodologies for parallelizing Haskell programs.

Back in university, I only learned to analyse running times of simple imperative algorithms. I don't see how the techniques extend to higher order algorithms, or ones that rely on lazy evaluation. I've looked at papers describing lazy algorithms, but their running times are only analysed in hand-waving form. Is that the best anyone can do, or are there better ways? I haven't seen anything even attempt to describe the running time of higher order algorithms.

I'm exploring for my own interest adding support for proofs of worst-case running time to a lazy language with first-class functions, possibly using dependent types, and I'm trying to see what notation and techniques are already used out there for doing the proofs by hand.

So, got any papers or languages relevant to this?