Eliminating Array Bound Checking through Non-dependent types

Oleg posted this pertinent message on the Haskell mailing list. It's always nice to see cool examples such as this.

Having saiod that, I must also say that I agree with Conor McBride who wrote that anyone who would argue (and I'm not saying you do) that work to try to make more advanced type systems and stronger static guarantees more convenient and well-supported is not necessary because it happens to be possible to bang out this or that example in Haskell as it stands if you think about it hard enough, is adopting the position of the ostrich.

Making type systems more expressive is a worthy goal. You want them to remain decidable (i.e., static), of course. Can we at least agree on that? ;-)

A Visual Environment for Developing Context-Sensitive Term Rewriting Systems

(via an interesting discussion on the types list)

A Visual Environment for Developing Context-Sensitive Term Rewriting Systems. Matthews, Findler, Flatt, Felleisen. International Conference on Rewriting Techniques and Applications (RTA) 2004.

Over the past decade, researchers have found context-sensitive term-rewriting semantics to be powerful and expressive tools for modeling programming languages, particularly in establishing type soundness proofs. Unfortunately, developing such semantics is an error-prone activity. To address that problem, we have designed PLT Redex, an embedded domain-specific language that helps users interactively create and debug context-sensitive term-rewriting systems. We introduce the tool with a series of examples and discuss our experience using it in courses and developing an operational semantics for R5RS Scheme.

Seems like a nice tool (it's DrScheme based, of course). I guess I should try it out.

TyPiCal: Type-based static analyzer for the Pi-Calculus

TyPiCal is a type-based static analyzer for the pi-calculus. The current version of TyPiCal provides four kinds of program analyses or program transformations: lock-freedom analysis, deadlock-freedom analysis, useless-code elimination, and information flow analysis.

Type system is an ordinary type system extended so that channel types carry precise information about how each channel is used. This allows a type inferencer to obtain information about the behavior of a process.

Tail of Nil and Its Type

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.

Alan Kay: The Early History of Smalltalk

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.

Partial Continuations

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.

Category Theory for Dummies - slides available

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.

Introduction to MDX Scripting in Microsoft SQL Server 2005 Beta 2

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...

Three interesting discussions

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).

Francis Crick (1916-2004)

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.