Lambda the Ultimate

Google open sources Szl - compiler and runtime for Sawzall Language:

Sawzall is a procedural language developed for parallel analysis of very large data sets (such as logs). It provides protocol buffer handling, regular expression support, string and array manipulation, associative arrays (maps), structured data (tuples), data fingerprinting (64-bit hash values), time values, various utility operations and the usual library functions operating on floating-point and string values. For years Sawzall has been Google's logs processing language of choice and is used for various other data analysis tasks across the company.

The original paper from Rob Pike et al.

Edward Fredkin and Tommoasso Toffoli from the MIT Labratory for Computer Science present Conservative Logic...

a comprehensive model of computation which explicitly reflects a number of fundamental principles of physics, such as the reversibility of the dynamical laws and the conservation of certain additive quantities (among which energy plays a distinguished role). Because it more closely mirrors physics than traditional models of computation, conservative logic is in a better position to provide indications concerning the realization of high-performance computing systems, i.e., of systems that make very efficient use of the "computing resources" actually offered by nature. In particular, conservative logic shows that it is ideally possible to build sequential circuits with zero internal power dissipation. After establishing a general framework, we discuss two specific models of computation. The first uses binary variables and is the conservative-logic counterpart of switching theory; this model proves that universal computing capabilities are compatible with the reversibility and conservation constraints. The second model, which is a refinement of the first, constitutes a substantial breakthrough in establishing a correspondence between computation and physics. In fact, this model is based on elastic collisions of identical "balls," and thus is formally identical with the atomic model that underlies the (classical) kinetic theory of perfect gases. Quite literally, the functional behavior of a general-purpose digital computer can be reproduced by a perfect gas placed in a suitably shaped container and given appropriate initial conditions.

This paper has a small discussion in a forum thread mostly saying the paper should be on the front page.

Conrad Barski's Lisp book, Land of Lisp, is out. There's an example chapter implementing a Hunt the Wumpus remake. The book was previously mentioned with an April's 1st special, War of the Worlds.

Comments? Critiques?

Blurb:

Lisp has been hailed as the world’s most powerful programming language, but its cryptic syntax and academic reputation can be enough to scare off even experienced programmers. Those dark days are finally over—Land of Lisp brings the power of functional programming to the people!

With his brilliantly quirky comics and out-of-this-world games, longtime Lisper Conrad Barski teaches you the mysteries of Common Lisp. You’ll start with the basics, like list manipulation, I/O, and recursion, then move on to more complex topics like macros, higher order programming, and domain-specific languages. Then, when your brain overheats, you can kick back with an action-packed comic book interlude!

Along the way you’ll create (and play) games like Wizard Adventure, a text adventure with a whiskey-soaked twist, and Grand Theft Wumpus, the most violent version of Hunt the Wumpus the world has ever seen.

You'll learn to:

* Master the quirks of Lisp’s syntax and semantics
* Write concise and elegant functional programs
* Use macros, create domain-specific languages, and learn other advanced Lisp techniques
* Create your own web server, and use it to play browser-based games
* Put your Lisp skills to the test by writing brain-melting games like Dice of Doom and Orc Battle

With Land of Lisp, the power of functional programming is yours to wield.

Erasure and Polymorphism in Pure Type Systems by Nathan Mishra-Linger and Tim Sheard

Abstract

We introduce Erasure Pure Type Systems, an extension to Pure Type Systems with an erasure semantics centered around a type constructor ∀ indicating parametric polymorphism. The erasure phase is guided by lightweight program annotations. The typing rules guarantee that well-typed programs obey a phase distinction between erasable (compile-time) and non-erasable (run-time) terms.

The erasability of an expression depends only on how its value is used in the rest of the program. Despite this simple observation, most languages treat erasability as an intrinsic property of expressions, leading to code duplication problems. Our approach overcomes this deficiency by treating erasability extrinsically.

Because the execution model of EPTS generalizes the familiar notions of type erasure and parametric polymorphism, we believe functional programmers will find it quite natural to program in such a setting.

This paper is a shorter presentation of some of the ideas of Nathan Linger PhD thesis. The general idea is that, in a dependent type systems, erasable terms are not defined intrisically (by their type or another classification), but by how they are used in the program. Functions are classified by two type-level constructs, one meaning that the function argument is used during runtime computation, and the other meaning that the parameter is computationnaly irrelevant (it only appears in type annotations, proof term, etc.). A very nice idea is that parametric polymorphism and erasability (type erasure, proof irrelevance...) may actually be the same thing.

Being more familiar with non-dependent systems (ML, System F), I'm interested in "type erasure semantics", but find it very nice that insights can be gained by looking at dependent sytems.

.

Background

Pure type systems are a generalization of the Lambda Cube, parametrized by arbitrary dependency between sorts (type polymorphism, type-level computations, dependent types...). They have been mentioned on LtU before:

• Lambda Cube and programming languages
• Examples of encodings in Pure Type Systems

While PTS may also describe non-dependent type systems, the problematic handled in this paper are mostly familiar to dependent type systems. Those have been discussed numerous times on LtU, among them, in chronological order:

• Why Dependent Types Matter
• Dependent types: literature, implementations and limitations ? with a nice Curry-Howard-style introduction by neelk
• Simply Easy! (An Implementation of a Dependently Typed Lambda Calculus) with a discussion of the strong link between dependent types and total (non Turing-complete) functional languages
• Summary of Dependently Typed Systems? discusses the "practical" tools available today (Coq, Agda, Epigram, ATS...) for proving and programming in dependently-typed systems

Other approaches try to access to some of the power of dependent types without adding them in their full complexity. The programming language Ωmega, also by Tim Sheard, has been mentioned recently.

A nice thing about the erasure treatment in Nathan Linger's paper is that it avoids the duplication between different families of "erasable" (or type-level) and "non-erasable" (or value-level) terms, such as can be observed in Coq between Set and Prop, or between the different kind layers of Ωmega. I think this is a promising idea, both for programming-oriented and proof-oriented dependently-typed systems.

The idea of mining code repositories to tease out language design issues have been discussed before on LtU. In this paper, J. Garrett Morris looks at the usage of overlapping instances in the Haskell code repository site hackage on deciding whether to include the feature in a new language.

Using Hackage to Inform Language Design
Abstract

Hackage, an online repository of Haskell applications and libraries, provides a hub for programmers to both release code to and use code from the larger Haskell community. We suggest that Hackage can also serve as a valuable resource for language designers: by providing a large collection of code written by different program- mers and in different styles, it allows language designers to see not just how features could be used theoretically, but how they are (and are not) used in practice.We were able to make such a use of Hackage during the design of the class system for a new Haskell-like programming language. In this paper, we sketch our language design problem, and how we used Hackage to help answer it. We describe our methodology in some detail, including both ways that it was and was not effective, and summarize our results.

Oleg just posted a new page, First-class modules: hidden power and tantalizing promises, related to new features in OCaml 3.12 (on LtU).

First-class modules introduced in OCaml 3.12 make type constructors first-class, permitting type constructor abstraction and polymorphism. It becomes possible to manipulate and quantify over types of higher kind. We demonstrate that as a consequence, full-scale, efficient generalized algebraic data types (GADTs) become expressible in OCaml 3.12 as it is, without any further extensions. Value-independent generic programming along the lines of Haskell's popular ``Generics for the masses'' become possible in OCaml for the first time. We discuss extensions such as a better implementation of polymorphic equality on modules, which can give us intensional type analysis (aka, type-case), permitting generic programming frameworks like SYB.

It includes a nice intro to first-class modules by Frisch and Garrigue: First-class modules and composable signatures in Objective Caml 3.12.

OCaml definitely just got even more interesting.

Now that's a really cool effort, I'm just saying : A haskell interpreter in Javascript.

Well, yes : if only for possibly inspiring other folks (and... forks ;) from there.

Bravo, Mattis and the team. :)

Several years ago, a reading group I was in read about the Flux OSKit Project, which aimed to provide a modular basis for operating systems. One of the topics of discussion was the possibility of, and possible benefits of, an application-specific OS. (For example, the fearful spectre of EmacsOS was raised.)

Today, I ran across "Turning down the LAMP: Software specialization for the cloud", which actually makes a pretty strong case for the idea on a virtual machine infrastructure,

...We instead view the cloud as a stable hardware platform, and present a programming framework which permits applications to be constructed to run directly on top of it without intervening software layers. Our prototype (dubbed Mirage) is unashamedly academic; it extends the Objective Caml language with storage extensions and a custom run-time to emit binaries that execute as a guest operating system under Xen. Mirage applications exhibit significant performance speedups for I/O and memory handling versus the same code running under Linux/Xen.

As one example,

Frameworks which currently use (for example) fork(2) on a host to spawn processes would benefit from using cloud management APIs to request resources and eliminate the distinction between cores and hosts.

On the other hand, I suspect that this "unashamedly academic" idea may already be advancing into the commercial arena, if I am correctly reading between the lines of the VMware vFabric tc Server^TM marketing material.

With LtU being 10 years old, it seems appropriate to start recycling ancient underappreciated posts — especially those in the static HTML archive where commenting is no longer possible.

With Smalltalk-80 nominally turning 30 and PARC turning 40, 2010 is a fitting year to revisit Design Principles Behind Smalltalk by Daniel H. H. Ingalls, known to his German admirers as Daniel Ha-ha Ingalls.

Mentioned twice by Ehud in 2001 (here and here), Ingalls's piece should be filed under Visionary Languages. Alas, no such category exists on LtU.

John N. Shutt's PhD Thesis is posted.
Abstract

Abstraction creates custom programming languages that facilitate programming for specific problem domains. It is traditionally partitioned according to a two-phase model of program evaluation, into syntactic abstraction enacted at translation time, and semantic abstraction enacted at run time. Abstractions pigeon-holed into one phase cannot interact freely with those in the other, since they are required to occur at logically distinct times.

Fexprs are a Lisp device that subsumes the capabilities of syntactic abstraction, but is enacted at run-time, thus eliminating the phase barrier between abstractions. Lisps of recent decades have avoided fexprs because of semantic ill-behavedness that accompanied fexprs in the dynamically scoped Lisps of the 1960s and 70s.

This dissertation contends that the severe difficulties attendant on fexprs in the past are not essential, and can be overcome by judicious coordination with other elements of language design. In particular, fexprs can form the basis for a simple, well-behaved Scheme-like language, subsuming traditional abstractions without a multi-phase model of evaluation.

The thesis is supported by a new Scheme-like language called Kernel, created for this work, in which each Scheme-style procedure consists of a wrapper that induces evaluation of operands, around a fexpr that acts on the resulting arguments. This arrangement enables Kernel to use a simple direct style of selectively evaluating subexpressions, in place of most Lisps' indirect quasiquotation style of selectively suppressing subexpression evaluation. The semantics of Kernel are treated through a new family of formal calculi, introduced here, called vau calculi. Vau calculi use direct subexpression-evaluation style to extend lambda calculus, eliminating a long-standing incompatibility between lambda calculus and fexprs that would otherwise trivialize their equational theories.

The impure vau calculi introduce non-functional binding constructs and unconventional forms of substitution. This strategy avoids a difficulty of Felleisen's lambda-v-CS calculus, which modeled impure control and state using a partially non-compatible reduction relation, and therefore only approximated the Church-Rosser and Plotkin's Correspondence Theorems. The strategy here is supported by an abstract class of Regular Substitutive Reduction Systems, generalizing Klop's Regular Combinatory Reduction Systems.

Related discussions

• Decomposing lambda - the Kernel language
• First-class environments. Discuss. ;)
• Lisps, First-Class Special Forms, Fexprs, The Kernel Programming Language
• The Kernel Programming Language