Lambda the Ultimate

People often wonder about Y in Haskell, so I think it is worth to have this link in the archive. Nothing new here for Haskell mavens, though.

Using the well-known categorical notion of `functor' one may define the concept of datatype (algebra) without being forced to introduce a signature, that is, names and typings for the individual sorts (types) and operations involved. This has proved to be advantageous for those theory developments where one is not interested in the syntactic appearance of an algebra.

Does it sound like "a module without a signature"?

If you like programming with bananas, lenses, and other weird things you might like this paper as well.

PS: OTOH, if you are sceptic about bialgebraic programming, then dialgebraic is definitely not for you.

This ongoing attempt to reproduce an efficient implementation of FFT using staging and abstract interpretation attempts to answer the question "How can we get the raw performance of hardware without giving up the expressivity and clarity of software?"

Here's how Oleg describes the contribution of this paper,

One may think that generating truly optimal power-of-two FFT is straightforward: we generate the naive radix-2 FFT code, and then optimize it, removing trivial multiplications (x*1), trivial additions (x+0), etc. That was the approach demonstrated previously.

And the bottom line is: the improved code is better than the original, but still worse than the best (FFTW) code. Here's why: if we consider an expression, (sin(pi/4) * x + cos(pi/4) * y), we may think that it can be optimized to sin(pi/4)*(x+y) thus saving one multiplication. Alas, computed sin(pi/4) and cos(pi/4) are not _exactly_ equal. Therefore, no optimizer is able to detect that they are the common factor. The previous paper BTW did handle the case of sin(pi/4) -- and still fell short of FFTW. To achieve optimum, more complex trigonometric transformations have to be applied.

This paper shows that to achieve the best quality of the generated code, we have to use domain knowledge. In case of FFT, we use the fact that it is a linear transform whose factors are roots of unity. This gives us an abstract representation of terms amenable to exact trigonometry. We can essentially symbolically manipulate the terms, and then concretize our abstract representation into the code. In the end, we generated FFT code that exactly matches the number of FP operations of FFTW. Somewhat unexpectedly, when we changed the function that generates the code for general complex multiplication, we obtained `split-radix FFT' -- another well-known FFT technique.

Oleg points out that the point isn't that they managed to reproduced the FFTW results. The crucial point is that we know exactly which identities (i.e., axioms) contributed to the optimum. The search was principled rather heuristic, and the code is generated in only one pass. There are no manipulations on the code: it is generated just right.

Why Dependent Types Matter
Conor McBride, James McKinna, Thorsten Altenkirch

Abstract:
We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system using refinements of a well known program, merge sort, as a running example. We discuss the relationship to other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.

via The Types Forum.