Lambda the Ultimate

A recent correspondent asks jokingly "I suppose static typing allows for solving the halting problem as well?". This reminded me of an article where Mark-Jason Dominus (the Perl guy) describes how the type checker in ML found an infinite loop bug in a simple sort routine - - well, "found" in the sense of "gave enough information for it to be apparent to anyone paying attention that something was wrong".

I wonder then whether this is a one-off, or whether people who use ML and similar languages frequently find that the type checker points them towards bugs that even a dynamic-typing-language programmer would regard as genuine - - that is to say, errors, like infinite loops, that are not on the face of it just type violations? Does anyone have other examples?

Some of you might be interested to learn that Oz got a basic macro facility.

A bit more information can be found in the mailing list.

Good stuff here, especially if you want to learn more about Ada 2005.

Robert Dewar's talk on Ada 2005 & high integrity systems should be of general interest. The main argument is that quality depends at least as much, if not more, on the language culture than it does on specific language features. Dewar presents some of the elements that contribute to Ada's success in the mission critical world which demands high quality software. Among them: emphasis on readability, static typing, the package construct and the ability to subset the language (e.g., SPARK and RAVENSCAR). The talk isn't about the technical aspects of these features, but on how they influence the way programmers approach their tasks.

Alan Burns discusses the Real time issues in Ada 2005. This revision of the language adds many important features (such as CPU monitoring and accounting, budgeting for the execution time of groups of tasks, and new scheduling polices including non-premeption, round robin, and Earliest Deadline First) to an already rich concurrency model. The non surprising conclusion is that Ada is the best language for RT programming not only on earth, but in the entire universe...

Brendan Eich, JavaScript 2 and the Future of the Web, XTech 2006

Motivation:

• Fix problems in JS1 that bug people daily
• A type system to enforce invariants
• Programming in the large
• Support bootstrapping and metaprogramming

Brendan Eich presented these slides recently at a conference on the future of web technology.

This whole book by Ulrich Breymann is online (I don't think I've seen this mentioned here before).

Hi there,

I have read a lot about the Curry-Howard isomorphism, but its relevance is not yet clear to me. I know there are experts on this topic here in this board, so please enlighten me :-)

Technically, I understand the relation between simply-typed lambda calculus and constructive logic and how the isomorphism between proofs and programs works.

However, what does Curry-Howard mean in general? Why is it significant? Does it say anything about a setting different from simply-typed lambda calculus/constructive logic?

I understand that one interpretation of CH is this: If I have a function of type t -> t', then the function body is a constructive proof that it is possible to construct a t' value from a t value.

However, this "type inhabitation" question seems to have a trivial answer in almost any real programming language: You can construct a value/function for whatever type you want (e.g., in Haskell you can just use "undefined")

I have never seen any type in a program that expresses an interesting, non-trivial proposition, but maybe I have not looked closely enough?

Would it be possible to take an arbitrary mathematical theorem (let's say: "string concatenation is associative", or Fermat's little theorem) and express it as a type?

I am also still a bit confused about conceptually viewing a type as a proposition. I think of types (of functions) as partial specifications, whereby the type checker checks conformance of the implementation to this partial specification. How does this fit together?