Lambda the Ultimate

Steven Kieffer, Jeremy Avigad, Harvey Friedman (2008). A language for mathematical knowledge management. Carnegie-Mellon tech. report CMU-PHIL-181.

The authors present a compact language for articulating mathematics, PST, which is syntactic sugar for an extension of Zermelo-Frankel set theory, DZFC, previously proposed by Harvey Friedman, which allows the naming of partially defined functions. The article gives some examples which show how for some mathematics, PST allows rather straightfoward expression. The article also gives some statistics gathered from an encoding of Suppes' Set Theory and Munkres' Topology, showing how PST allows a drastic compression compared to plain first-order ZFC.

An ancient paper (July 1978: 30 years ago) from the long gone Lisp Bulletin by Harald Wertz.

The system describes attempts to improve incompletely specified Lisp programs, without however resorting to more information, in the form of specifications, test cases or the like.

A second paper on the system is Stereotyped Program Debugging: an Aid for Novice Programmers.

Partial vectorisation of Haskell programs. Manuel M. T. Chakravarty, Roman Leshchinskiy, Simon Peyton Jones, and Gabriele Keller, Proc ACM Workshop on Declarative Aspects of Multicore Programming, San Francisco, Jan 2008.

Vectorisation for functional programs, also called the flattening transformation, relies on drastically reordering computations and restructuring the representation of data types. As a result, it only applies to the purely functional core of a fully-fledged functional language, such as Haskell or ML. A concrete implementation needs to apply vectorisation selectively and integrate vectorised with unvectorised code. This is challenging, as vectorisation alters the data representation, which must be suitably converted between vectorised and unvectorised code. In this paper, we present an approach to partial vectorisation that selectively vectorises sub-expressions and data types, and also, enables linking vectorised with unvectorised modules.

The idea is fairly simple, and utilizes conversion between vectorized and unvectorized representations of the datatypes. A formal translation scheme is provided.

Data Parallel Haskell papers are here.

Mark van Atten (2008). The Development of Intuitionistic Logic. Stanford Encyclopedia of Philosophy.

This article gives an excellent account of the development of intuitionistic logic, from its roots in Brouwer's theological metaphysics, through to its formal presentation by Heyting in 1956. The account is strong on the tensions between the subjectivist motif and the urge to formalise. Via Richard Zach.

Chris Oakasaki has a blog post about teaching functional programming using Ada. He says

Why, with excellent functional programming languages like Haskell or ML easily available, would I choose to do a functional programming project in Ada? (I CAN STILL HEAR YOU LAUGHING!) Partly because we use Ada in some courses at our institution, and I wanted a library that could help in teaching recursion to novices. But, honestly, mostly I just wanted to see if it could be done

The idea of crossing paradigms has been around awhile. SICP rather famously introduces object orientation by building it on top of Scheme.

What do you think about teaching or learning paradigm A in a language strongly oriented towards paradigm B? What's gained? What's lost?

Catch me if you can: Towards type-safe, hierarchical, lightweight, polymorphic and efficient error management in OCaml, by David Teller, Arnaud Spiwack, Till Varoquaux:

This is the year 2008 and ML-style exceptions are everywhere. Most modern languages, whether academic or industrial, feature some variant of this mechanism. Languages such as Java even have a degree of out-of-the-box static coverage-checking for such exceptions, which is currently not available for ML languages, at least not without resorting to external tools.

In this document, we demonstrate a design principle and a tiny library for managing errors in a functional manner, with static coverage-checking, automatically-inferred, structurally typed and hierarchical exceptional cases, all of this for what we believe is a reasonable run-time cost. Our work is based on OCaml and features simple uses of higher-order programming, low-level exceptions, phantom types, polymorphic variants and compile-time code
rewriting.

Exhaustively checked, user-friendly exception handling was a bit of an open problem for awhile. As the paper details, languages supported either cumbersome, exhaustively checked polymorphic exceptions, as in Haskell, or we had unchecked easily extensible monomorphic exceptions, as in ML, or we had checked, extensible exceptions using a universal type as in Java.

Supporting exhaustively checked, easily extensible polymorphic exceptions seemed quite a challenge, which this paper solves using monadic error handling and nested polymorphic variants. The paper also gives a good overview of current techniques of exception checking in OCaml, ie. ocamlexc.

The performance of such exceptions is understandably lower than native exceptions, given all the thunking and indirection that monads entail. The authors attempt various implementations and test their performance against native exceptions. Ultimately, monadic error management seems acceptable for actual error handling, but not for control flow as native exceptions are sometimes used in OCaml.

One interesting extension is to consider how efficient the implementations would be given more sophisticated control flow operators, such as continuations, coroutines, or delimited continuations, or whether native exceptions can be salvaged using a type and effects system in place of monads.

Just a quick reminder -- the 2008 ICFP Programming Contest starts tomorrow.

Functional Netlists, Sungwoo Park, Jinha Kim, Hyeonseung Im. ICFP 2008.

In efforts to overcome the complexity of the syntax and the lack of formal semantics of conventional hardware description languages, a number of functional hardware description languages have been developed. Like conventional hardware description languages, however, functional hardware description languages eventually convert all source programs into netlists, which describe wire connections in hardware circuits at the lowest level and conceal all high-level descriptions written into source programs.

We develop a variant of the lambda calculus, called l-lambda (linear lambda), which may serve as a high-level substitute for netlists. In order to support higher-order functions, l-lambda uses a linear type system which enforces the linear use of variables of function type. The translation of l-lambda into structural descriptions of hardware circuits is sound and complete in the sense that it maps expressions only to realizable hardware circuits and that every realizable hardware circuit has a corresponding expression in l-lambda. To illustrate the use of l-lambda as a high-level substitute for netlists, we design a simple hardware description language that extends l with polymorphism, and use it to implement a Fast Fourier Transform circuit.

Given the recent discussion about hardware synthesis languages, the appearance of this paper seems timely. The use of linear types is perhaps unsurprising from a technical point of view, but it's surprising when you consider how frequently and in how many different contexts they appear.

Also, one thing I don't understand: there's apparently a difference between a "hardware description language" and a "hardware synthesis language". If anyone could explain what the difference means, I'd appreciate it. :)

See the Dusty Decks announcement.

Non-Deterministic Recursive Ascent Parsing, Renee Leermakers. 1991 conference on European chapter of the Association for Computational Linguistics.

A purely functional implementation of LR-parsers is given, together with a simple correctness proof. It is presented as a generalization of the recursive descent parser. For non-LR grammars the time-complexity of our parser is cubic if the functions that constitute the parser are implemented as memo-functions, i.e. functions that memorize the results of previous invocations. Memo-functions also facilitate a simple way to construct a very compact representation of the parse forest. For LR(0) grammars, our algorithm is closely related to the recursive ascent parsers recently discovered by Kruseman Aretz [1] and Roberts [2]. Extended CF grammars (grammars with regular expressions at the right hand side) can be parsed with a simple modification of the LR-parser for normal CF grammars.

How LR parsers worked always confused me until I learned about their presentation in terms of recursive ascent.