Lambda the Ultimate

I this paper, we describe an extended static checking tool for Haskell, named ESC/Haskell, that is based on symbolic computation and assisted by a few novel properties. One novelty is our use of Haskell as the specification language itself for pre/post conditions.

Joel Spolsky in Can Your Programming Language Do This? (Aug 1, 2006):

Java required you to create a whole object with a single method called a functor if you wanted to treat a function like a first class object. Combine that with the fact that many OO languages want you to create a whole file for each class, and it gets really klunky fast. If your programming language requires you to use functors, you're not getting all the benefits of a modern programming environment. See if you can get some of your money back.

Bracha, Gafter, Gosling, and Ahé in Closures for Java (Aug 18, 2006):

Modern programming languages provide a mixture of primitives for composing programs. C#, Javascript, Ruby, Scala, and Smalltalk (to name just a few) have direct language support for function types and inline function-valued expression, called closures. A proposal for closures is working its way through the C++ standards committees as well. Function types provide a natural way to express some kinds of abstraction that are currently quite awkward to express in Java. For programming in the small, closures allow one to abstract an algorithm over a piece of code; that is, they allow one to more easily extract the common parts of two almost-identical pieces of code. For programming in the large, closures support APIs that express an algorithm abstracted over some computational aspect of the algorithm. We propose to add function types and closures to Java. We anticipate that the additional expressiveness of the language will simplify the use of existing APIs and enable new kinds of APIs that are currently too awkward to express using the best current idiom: interfaces and anonymous classes.

3APL is a programming language for implementing cognitive agents. It provides programming constructs for implementing agents' beliefs, goals, basic capabilities (such as belief updates, external actions, or communication actions) and a set of practical reasoning rules through which agents' goals can be updated or revised. The 3APL programs are executed on the 3APL platform. Each 3APL program is executed by means of an interpreter that deliberates on the cognitive attitudes of that agent. The EBNF specification of 3APL and the deliberation cycle are available through the following links:

Can't find any mention of the 3APL language so I thought I would mention it. There are quite a few papers and a fun download with toy examples.

Oh, and there is also a mobile version 3APL-M, and a Wikipedia entry.

In a post about Ruby's dynamic typing, I made the claim:

Meta-programming makes the type inference problem equivalent to the halting problem.

Am I wrong? Basically, I am wondering if there are type inference algorithms (or better still, implementations) that can handle programming languages where the operations permitted with respect to a variable (a/k/a types) change at run time.

Your corrections and pointers to current research and/or implementations would be greatly appreciated.

Thanks in advance...

Came across the Pure Pattern Calculus a little while ago, and it seemed to provide a simple, yet promising synthesis of many diverse language patterns. I haven't seen it discussed here, so perhaps it will be of interest:

Abstract. The pure pattern calculus generalises the pure lambda-calculus by basing computation on pattern-matching instead of beta-reduction. The simplicity and power of the calculus derive from allowing any term to be a pattern. As well as supporting a uniform approach to functions, it supports a uniform approach to data structures which underpins two new forms of polymorphism. Path polymorphism supports searches or queries along all paths through an arbitrary data structure. Pattern polymorphism supports the dynamic creation and evaluation of patterns, so that queries can be customised in reaction to new information about the structures to be encountered. In combination, these features provide a natural account of tasks such as programming with XML paths.
As the variables used in matching can now be eliminated by reduction it is necessary to separate them from the binding variables used to control scope. Then standard techniques suffice to ensure that reduction progresses and to establish confluence of reduction.

Bondi is their experimental programming language based on the pure pattern calculus.

I'm working my way through An Introduction to Lambda Calculus (Barendregt & Barendsen, 1994) and I was wondering if there is an answer sheet available, or a forum where I could talk with someone about the problems in the text. In particular, problem 2.11

Show

    ∀ C[, ] ∃ F ∀ x Fx = C[F, x]

and take another look at the exercizes 2.8, 2.9 and 2.10

has me stumped. I don't understand the bracketing convention used following C, and I don't get what's so special about the result shown in this exercize.

Hi all -

though I hardly have an academic background (or the age to have programmed Haskell) I wanted your opinions on a aspect oriented language thing I developed using Microsoft's dsl toolkit.

have a look at: http://bloggingabout.net/blogs/olaf/archive/2006/08/13/13363.aspx

Looking forward to your reactions - thanks

Here, care to discuss.

The Extreme Markup 2006 conference has finished and the proceedings are up. If you have any interest in the intersection of programming and markup languages, there were a few papers worth looking at. Here's my choice:

• Higher-Order Functional Programming with XSLT 2.0 and FXSL shows how to implement a good part of Haskell 98 Prelude in XSLT 2.0. Unfortunately, the presentation didn't do a very good job of explaining why that is a good thing: most of attendees seemed to conclude it was only usable for numerical calculations.

• Datatypes for XML: the Datatyping Library Language (DTLL) presents a small schema language for defining new primitive data types.

• <plug>
  Streaming component combinators presents an embedded language / combinator framework for building and reusing XML-streaming components.
  </plug>

• Rabbit/duck grammars: a validation method for overlapping structures might be interesting if you're into theory of formal languages and parsers.

• Conveying Meaning through Space and Time using XML has nothing to do with programming languages directly. Still, I guess some people around here will find it interesting, since it's trying to apply machinery of Category Theory to some difficult real-world problems.

Doea anyone knows a complete and good implementation of lambda calculus in (preferably) java? (I do not mean java byte-code, rather I mean java itself.)