Lambda the Ultimate

Via the plt-scheme mailing list:

We are pleased to announce the first public release [beta 7] of ACL2
in DrScheme, a combination of the ACL2 theorem prover system with the
DrScheme programming environment. The objective of this project is
to provide a development environment for ACL2 suitable for novice
users as well as enhancements of ACL2 that are attractive for the
typical undergraduate student (graphics, interactive games, sound).

There's a tutorial with screenshots and some examples on the ACL2 in DrScheme web page.

I'm always happy to see reasoning about programs introduced at the undergraduate level. I wonder what the LtU community would do with a tool like this. What cool things would you teach with a beginner's theorem prover?

This announcement has been made in various places, including comp.lang.scheme:

March 7, 2006

Since the last report of the Steering Committee, a number of important changes have taken place.

First, Marc Feeley and Manuel Serrano have resigned from the Editors Committee. We have accepted their resignations with regret, and with gratitude for the efforts they have expended to produce a revised Scheme standard.

In light of these changes, the Steering Committee has amended the Charter to:

(a) change the number of Editors from seven to five.

(b) replace the office of Editor-in-Chief by a Chair and a Project Editor. The Chair is responsible for organizing meetings and other activities and ensuring that the process makes progress in an orderly fashion. The Project Editor is responsible for producing standardization documents.

The five editors have chosen their Chair and Project Editor. They are:

Chair: Kent Dybvig
Project Editor: Mike Sperber

The Editors Committee has now produced a progress report, which is available at schemers.org. In it they state their intention to deliver to the Steering Committee a complete draft R6RS by September 1, 2006.

The Steering Committee looks forward to receiving their draft.

Alternate links to the Editors' Progress Report:

http://www.cs.indiana.edu/~dyb/r6rs/status.pdf
http://www.cs.indiana.edu/~dyb/r6rs/status.html

---The Scheme Language Steering Committee:
Alan Bawden
Guy Steele
Mitch Wand

Features of a programming language, whether syntactic or semantic, are all part of the language's user interface. And a user interface can handle only so much complexity or it becomes unusable. This is also the reason why Python will never have continuations, and even why I'm uninterested in optimizing tail recursion.

Thus spoke Guido - as LtU readers already know.

Now, not even four weeks later, it has become clear that turning tail recursions into iterations can be achieved by an innocent little decorator in pure Python. No Rube Goldberg machine(s) in sight.

I haven't read this really, but it's in the queue for such a long time I might as well pass it along...

Jeremy Gibbons (2006). Fission for Program Comprehension. Submitted for publication.

Fusion is a program transformation that combines adjacent computations, flattening structure and improving efficiency at the cost of clarity. Fission is the same transformation, in reverse: creating structure, ex nihilo. We explore the use of fission for program comprehension, that is, for reconstructing the design of a program from its implementation. We illustrate through rational reconstructions of the designs for three different C programs that count the words in a text file.

The paper works through the examples meticulously and highlights their recursion schemes. The claim is that the three different wordcount programs might all have arisen from the same high-level design, namely the composition length o words.

The more audacious claim is that [i]f one accepts the claim that design patterns in object-oriented programming correspond to recursion patterns in generic functional programming, then this is further support for Johnson’s slogan that ‘patterns document architectures’.

A constraint-based approach to guarded algebraic data types

We study HMG(X), an extension of the constraint-based type system HM(X) with deep pattern matching, polymorphic recursion, and guarded algebraic data types. Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, (first-class) phantom types, and equality qualified types, and are closely related to inductive types. Their characteristic property is to allow every branch of a case construct to be typechecked under different assumptions about the type variables in scope. We prove that HMG(X) is sound and that, provided recursive definitions carry a type annotation, type inference can be reduced to constraint solving. Constraint solving is decidable, at least for some instances of X, but prohibitively expensive. Effective type inference for guarded algebraic data types is left as an issue for future research.

Constraint-based type inference for guarded algebraic data types

Guarded algebraic data types subsume the concepts known in the literature as indexed types, guarded recursive datatype constructors, and first-class phantom types, and are closely related to inductive types. They have the distinguishing feature that, when typechecking a function defined by cases, every branch may be checked under different assumptions about the type variables in scope. This mechanism allows exploiting the presence of dynamic tests in the code to produce extra static type information.

We propose an extension of the constraint-based type system HM(X) with deep pattern matching, guarded algebraic data types, and polymorphic recursion. We prove that the type system is sound and that, provided recursive function definitions carry a type annotation, type inference may be reduced to constraint solving. Then, because solving arbitrary constraints is expensive, we further restrict the form of type annotations and prove that this allows producing so-called tractable constraints. Last, in the specific setting of equality, we explain how to solve tractable constraints.

To the best of our knowledge, this is the first generic and comprehensive account of type inference in the presence of guarded algebraic data types.

Haskell' (pronounced "Haskell prime") is being formulated while we sleep. While the committee wants to incorporate into the new standard only "tried-and-true language features", a quick glance at the mailing list shows quite a few unimplemented ideas being tossed around.

The same thing happens with the C++ standardization process. Is it a good idea to keep language standardization conservative? Herb Sutter would perhaps argue so, since the export feature in C++98 was so rarely implemented.

So, is conservatism right for C++0x? Is it right for Haskell'?

The essence of ML type inference is an expanded version of Chapter 10 of the beloved Advanced Topics in Types and Programming Languages. It weighs in as the heaviest non-dissertation, non-book academic paper I've ever seen, but it's still a great introduction to HM type inference with some extensions.

The extensions are based on contraints, and are closely related to HM(X) and Chameleon. Along the way, the authors deal with row types, equirecursive types, and subtyping. Fun for the whole family!

Haskell is not not ML. Ben Rudiak-Gould, Alan Mycroft, and Simon Peyton Jones. European Symposium on Programming 2006 (ESOP'06).

We present a typed calculus IL ("intermediate language") which supports the embedding of ML-like (strict, eager) and Haskell-like (non-strict, lazy) languages, without favoring either. IL's type system includes negation (continuations), but not implication (function arrow). Within IL we find that lifted sums and products can be represented as the double negation of their unlifted counterparts. We exhibit a compilation function from IL to AM --- an abstract von Neumann machine --- which maps values of ordinary and doubly negated types to heap structures resembling those found in practical implementations of languages in the ML and Haskell families. Finally, we show that a small variation in the design of AM allows us to treat any ML value as a Haskell value at runtime without cost, and project a Haskell value onto an ML type with only the cost of a Haskell deepSeq. This suggests that IL and AM may be useful as a compilation and execution model for a new language which combines the best features of strict and non-strict functional programming.

The authors start from the claim that most of the differences between SML and Haskell are independent of evaluation order. Is it possible, they wonder, to design a hybrid language which in some way abstracts over possible evaluation orders?

This papers leaves the language design for future work, and concentrates on the implementation costs. The results seem positive, so one hopes this project will mature and end the civil war between lazy and eager functional programming...

More information on this project is likely to appear here.