Lambda the Ultimate

Over at lwn there is an currently a discussion going on about the little things in programming languages that make a difference. Commas, decimal points, braces, etc.

The content is subscriber only for the first week so won't be generally available until the June 16th.

The deadline is July 6th (just a week away) for submitting papers to the annual ACM conference on High Integrity Language Technology (HILT 2013). The conference will be in Pittsburgh November 10-14, in close proximity to the Software Engineering Institute and CMU. We have four great keynotes/invited speakers for this conference (Jeannette Wing, Ed Clarke, John Goodenough, and Michael Whalen), several interesting tutorials (on SMT solvers, Model Checking, etc.), and we are expecting some great papers as well (so get cracking!).

Conference website is:

http://www.sigada.org/conf/hilt2013

PDF Call for papers is at:

http://www.sigada.org/conf/hilt2013/HILT2013-CFP.pdf

-Tucker Taft
Program Chair, HILT 2013

Continuation calculus ("CC") is an alternative to lambda calculus, where the order of evaluation is determined by programs themselves. CC is a constrained term rewriting system, designed such that continuations are no unusual terms. This makes it natural to model programs with nonlocal control flow, as is the case with exceptions and call-by-name functions. The resulting system has very simple operational semantics.

Because no real pattern matching is possible in CC, we can only examine data through its reduction behavior. This in turn allows us to define values that are compatible to natural numbers or lists, but whose deconstruction requires computation. Such values are similar to call-by-name function applications.

For an introduction, look at the presentation. Details can be found in the paper. You may also experiment with the online evaluator, which has some example programs.

In future work, I will describe a scheme to translate functional programs to continuation calculus. I also plan to describe an applicable type system, but the details have yet to be worked out.

In order to get a mathematical definition of recursive functions one needs fixpoints.

The following article describes how a certain class of recursive functions can be described via a functional whose fixpoint defines mathematically the recursive function. Furthermore it is shown that this class of recursive functions are defined via a unique fixpoints (i.e. the corresponding functional has only one fixpoint).

The article is based on the previous articles Complete lattices and closure systems, Functions and complete partial orders and Closures and fixpoints.

Part of the EScala, REScala, JEScala systems, a paper on REScala:

Traditionally, object-oriented software adopts the Observer pattern to implement reactive behavior. Its drawbacks are well-documented and two families of alternative approaches have been proposed, extending object-oriented languages with concepts from functional reactive and dataflow programming, respectively event-driven programming. The former hardly escape the functional setting; the latter do not achieve the declarativeness of more functional approaches. In this paper, we present RESCALA, a reactive language which integrates concepts from event-based and functional-reactive programming into the object-oriented world. RESCALA supports the development of reactive applications by fostering a functional declarative style which complements the advantages of object- oriented design.

There's example code available from the projects' web page.

While not strictly related to programming languages, some people might be interested in Computability Logic, which purports to generalize classical, linear and intuitionistic logics in a unified formal theory of computability. Brief overview:

Computation and computational problems in Computability Logic are understood in their most general, interactive sense, and are precisely seen as games played by a machine (computer, agent, robot) against its environment (user, nature, or the devil himself). Computability of such problems means existence of a machine that always wins the game. Logical operators stand for operations on computational problems, and validity of a logical formula means being a scheme of "always computable" problems. [...] The classical concept of truth is nothing but a special case of computability -- computability restricted to problems of zero interactivity degree.

Looks like an interesting approach, and intuitively appealing, at least to me. Here's a link to the first paper Introduction to computability logic, by Giorgi Japaridze:

This work is an attempt to lay foundations for a theory of interactive computation and bring logic and theory of computing closer together. It semantically introduces a logic of computability and sets a program for studying various aspects of that logic. The intuitive notion of (interactive) computational problems is formalized as a certain new, procedural-rule-free sort of games (called static games) between the machine and the environment, and computability is understood as existence of an interactive Turing machine that wins the game against any possible environment. The formalism used as a specification language for computational problems, called the universal language, is a non-disjoint union of the formalisms of classical, intuitionistic and linear logics, with logical operators interpreted as certain, — most basic and natural, — operations on problems. Validity of a formula is understood as being “always computable”, and the set of all valid formulas is called the universal logic. The name “universal” is related to the potential of this logic to integrate, on the basis of one semantics, classical, intuitionistic and linear logics, with their seemingly unrelated or even antagonistic philosophies. In particular, the classical notion of truth turns out to be nothing but computability restricted to the formulas of the classical fragment of the universal language, which makes classical logic a natural syntactic fragment of the universal logic. The same appears to be the case for intuitionistic and linear logics (understood in a broad sense and not necessarily identified with the particular known axiomatic systems). Unlike classical logic, these two do not have a good concept of truth, and the notion of computability restricted to the corresponding two fragments of the universal language, based on the intuitions that it formalizes, can well qualify as “intuitionistic truth” and “linear-logic truth”. The paper also provides illustrations of potential applications of the universal logic in knowledgebase, resourcebase and planning systems, as well as constructive applied theories. The author has tried to make this article easy to read. It is fully self-contained and can be understood without any specialized knowledge of any particular subfield of logic or computer science.

Edit: I just realized there was an LtU post on this in the past (and another one), but if you haven't seen it already, it's worth a look!

An old paper that seems quite retro by today's standards:

DIALOG is an algebraic language for online use with a graphical input-output console device. It is a computational aid for the casual user, which provides basic facilities for graphical and numeric input and display, online and offline program preparation and storage, and hard copy presentation of results. Use of the system requires a minimum of experience or instruction, since the growth of an overlaying system control language has been prevented, and there are no processor-oriented statements, like variable type or dimension declarations. Moreover, in the online situation the processor interacts with the graphical keyboard on a character-by-character basis so as to restrict the programmer's choice of input symbols to those which are syntactically correct. DIALOG has been in daily operation at the MIT Research Institute since February, 1966.

The scanned paper is behind a paywall, but you can check here.

Nimrod is a statically typed, imperative programming language that tries to give the programmer ultimate power without compromises on runtime efficiency. This means it focuses on compile-time mechanisms in all their various forms.

Beneath a nice infix/indentation based syntax with a powerful (AST based, hygienic) macro system lies a semantic model that supports a soft realtime GC on thread local heaps. Asynchronous message passing is used between threads, so no "stop the world" mechanism is necessary. An unsafe shared memory heap is also provided for the increased efficiency that results from that model.

I would like to share this language here as it has recently had a new version released. Nimrod resembles Python in that it uses whitespace to delimit blocks and Pascal because of the way that types are defined (TType). It supports metaprogramming with macros and templates. Code example:

# compute average line length
var count = 0
var sum = 0

for line in stdin.lines:
  count += 1
  sum += line.len

echo "Average line length: ",
  if count > 0: sum / count else: 0

By C. Lutz and H. Derby circa 1982. Header:

JANUS was written by myself and Howard Derby for a class at Caltech in 1982 (or thereabouts). The class had nothing to do directly with this project. We did it out of curiosity over whether such an odd animal as this was possible, and because we were interested in knowing where we put information when we programmed. JANUS forced us to pay attention to where our bits went since none could be thrown away.

This is class report but also a great design exercise in reversible programming language constructs. For example, I love how they make if conditions reversible:

if   num # 1
then i += 1        ; Put last prime away, if not done
     fact[i] : num ; and zero num
else num -= 1
fi fact[i] # fact[i-1]

Note that # means not equals; colon is used for swap (!!). The "fi" condition must match the truth value of the "if" condition so the condition can be played backwards. Loop constructs are similarly organized so they can play backwards, the language has procedures but all variables are global :).

Sadly, although there are a few follow on papers (e.g. by Yokoyama et al.) and some esoteric reversible languages like Kayak, there doesn't seem to be any other good examples of high-level serious reversible programming languages.

(via awelonblue)

"Plain English Programming" care of the Osmosian order.

We intend to supplant, in turn, the programming languages, operating systems, and hardware configurations currently in widespread use. Our initial goal is to see Plain English (and other natural-language variants). ... We offer our Plain English compiler as both "proof of concept" and a first step in the right direction. Our integrated development environment includes an elegant desktop interface, a simplified file manager, an efficient text editor, the compiler, and the page-layout routines used to produce all of our documentation, the illustrations for our web site, and this manifesto. It should be noted that all this functionality is embodied in a single, stand-alone, native-code executable less than one megabyte in size. The program runs on the Wintel Kluge, was written entirely in Plain English, and re-compiles itself in less than three seconds.