Lambda the Ultimate

Epigram: practical programming with dependent types

Find the type error in the following Haskell expression:

if null xs then tail xs else xs

Found it? Of course you haven't. But this program is obviously nonsense! Unless you're a typechecker, that is. The trouble is that only certain computations make sense if the null xs test is True, whilst others make sense if it is False. However, as far as the type system is concerned, the type of the then branch is the type of the else branch is the type of the entire if . . . then . . . else . . ..

Statically, the test is irrelevant. Which is odd, because if the test really were irrelevant, we wouldn't bother doing it.

We mentioned this issue in discussions. LtU recently featured Epigram with emphasis on its interactive programming abilities, but I would like to add that Conor McBride's papers are mostly about practical use of dependent types for programming. They are also fun to read, though I can easily imagine how his experiments with presentation, like this one, can annoy some people.

by way of lispmeister
(PDF scan or HTML)

Smalltalk's design--and existence--is due to the insight that everything we can describe can be represented by the recursive composition of a single kind of behavioral building block that hides its combination of state and process inside itself and can be dealt with only through the exchange of messages.

Really double-extra good.

A nice introduction by Chris Double.

In the previous example we've effectively called the continuation and then returned back to the caller of that continuation. What we really want to do is capture a 'partial continuation' or 'subcontinuation'. That is, not the entire continuation but a section of it and then return back to the caller.

The 'splitter' operator mentioned in the header to this article implements exactly that. It marks the point at which a continuation should be captured up to, instead of the entire continuation. A 'partial continuation' can then be reified up to this point.

From the discussion group:

For those interested in a brief introduction to category theory, James Cheney has recently posted some PDF slides titled Category Theory for Dummies on his home page.

These slides are introductory, and don't contain advanced techniques, but they seem to be nicely done.

This document describes how Multidimensional Expressions (MDX) for Microsoft SQL Server 2005 Beta 2 can be applied to common business problems.

Given the interest in database integration exhibited in the past, I guess this may be of interest to some readers.

MDX is the server-based calculation engine provided by SQL Server's Analysis Services. MDX scripts appear to execute like programs, however the MDX script does not really "run." It is a declared set of commands that are always in effect. The contents of the cube are always consistent with the script. The scripting language is explained along with examples.

You might call it declarative programming...

Since we are having a slow week, I thought it might be a good idea to mention three interesting threads from the discussion group. Most regulars read the discussion group, but not everyone is aware of it, and we are still working on an RSS feed for new discussion group messages. So, in case you missed them, you might want to check out,

1. Understanding continuations.
2. Explaining monads.
3. Why type systems are interesting (this is a long thread, so consider starting a new one if you want to move the discussion in a new direction).

This is a bit offtopic, but Francis Crick was an esteemed man of science and we should all be saddened to hear of his death.

Crick co-discovered the the structure and properties of DNA in 1953, along with James Watson.

His work leading to the understanding of the genetic code is, however, more closely related to our areas of interest. These classic experiments were an astonishing example of scientific discovery at its best.

In recent years Crick was interested in the questions of neurobiology, and published the provocative book Astonishing Hypothesis which tackled the question of human consciousness.

Udell reports:

"When you think about it," Hugunin said, "why would the CLR be worse for dynamic languages than the JVM, given that Microsoft had the second mover advantage?" And in fact, while he had to do plenty of extra work to support dynamic features that the CLR doesn't natively offer, he notes that the massive engineering resources invested in the CLR make it highly optimized along a number of axes. So, for example, the CLR's function call overhead is apparently less than the native-code CPython's function call overhead, and this is one of the reasons why IronPython benchmarks well against CPython.

If you look carefully you'll see that items on the home page now have an "other blogs" link along with the comment link, department link etc.

The "other blogs" link invokes a Technorati search which hopefully shows all blogs referencing the LtU item (if there are any).

Thanks, Anton!

Parallel Programming with Control Abstraction. Lawrence A. Crowl and Thomas J. LeBlanc. ACM Transactions on Programming Languages and Systems 16(3): 524-576, May 1994

Since control abstraction separates the definition of a construct from its implementation, a construct may have several different implementations, each exploiting a different subset of the parallelism admitted by the construct. By selecting an implementation for each control construct using annotations, a programmer can vary the parallelism in a program to best exploit the underlying hardware without otherwise changing the source code. This approach produces programs that exhibit most of the potential parallelism in an algorithm, and whose performance can be tuned simply by choosing among the various implementations for the control constructs in use.

There were some queries regarding parallel programming constructs, so this paper may be of interest.