Lambda the Ultimate

Application-specific foreign-interface generation, John Reppy and Chunyan Song, October 2006.

A foreign interface (FI) mechanism to support interoperability with libraries written in other languages (especially C) is an important feature in most high-level language implementations. Such FI mechanisms provide a Foreign Function Interface (FFI) for the high-level language to call C functions and marshaling and unmarshaling mechanisms to support conversion between the high-level and C data representations. Often, systems provide tools to automate the generation of FIs, but these tools typically lock the user into a specific model of interoperability. It is our belief that the policy used to craft the mapping between the high-level language and C should be distinct from the underlying mechanism used to implement the mapping.

In this paper, we describe a FI generation tool, called FIG (for Foreign Interface Generator) that embodies a new approach to the problem of generating foreign interfaces for high-level languages. FIG takes as input raw C header files plus a declarative script that specifies the generation of the foreign interface from the header file. The script sets the policy for the translation, which allows the user to tailor the resulting FI to his or her application. We call this approach application-specific foreign-interface generation. The scripting language uses rewriting strategies as its execution model. The other major feature of the scripting language is a novel notion of composable typemaps that describe the mapping between high-level and low-level types.

FFIs are a perennial engineering problem, and it's very nice to see progress being made on automating what's automatable about building interfaces. Their interface specification language is built from two little DSLs. The first one is a language that for specifying how to map low level types to high level types, and the second one is a rewriting-based language for translating API functions, which makes use of the type mapping programs you defined earlier. The whole thing is quite pretty, and seems to read very well.

An interesting gimme for you stack-language fans: the DSL that Reppy and Song use to specify type mappings from low-level to high-level types is a combinator-based language that reads a bit like Forth or Postscript.

Pardus Linux is a case study of functional Python. It's a Linux distribution built from semi-scratch, the main focii being package management and init subsystems - places where C and shell script make poor sense. A funded group has finally tackled these issues.

A package management software deals a lot with sets, lists, and dependency graphs....We have extensively used functional operators (map, filter, reduce) and list comprehensions, even metaclasses are used in a few places.

Someone nudge Guido. Scheme or Oz might have been the better choice, but give them credit. They admit frankly to social acceptance issues.

Doing strange things with SQL is always fun...

This Sudoku solver makes use of Oracle 10g's MODEL clause, which seems quite hairy.

SQL isn't mentioned around here all that often, so I am glad we can at least remind ourselves from time to time of the most heavily used declarative language out there by posting SQL puzzles and hacks...

In recent years, there have been numerous proposals that introduce time into standard relational systems. Unfortunately, most of the attempts have been based on ad-hoc extensions of existing database systems and query languages, e.g., TQUEL and TSQL. Such extensions often create many problems, when precise semantics needs to be developed, if one exists at all. In a recent survey by J. Chomicki, a clean way of defining temporal databases based on logic was proposed. This methodology views temporal databases as multi-sorted, finitely representable first-order structures. Query languages then became formulas in suitable logics over the vocabulary of such structures.

The Design and Implementation of a Dataflow Language for Scriptable Debugging, Guillaume Marceau, Gregory H. Cooper, Jonathan P. Spiro, Shriram Krishnamurthi, and Steven P. Reiss.

Debugging is a laborious, manual activity that often involves the repetition of common operations. Ideally, users should be able to describe these repetitious operations as little programs. Debuggers should therefore be programmable, or scriptable. The operating environment of these scripts, however, imposes interesting design challenges on the programming language in which these scripts are written.

This paper presents our design of a language for scripting debuggers. The language offers powerful primitives that can precisely and concisely capture many important debugging and comprehension metaphors. The paper also describes a pair of debuggers, one for Java and the other for Scheme, built in accordance with these principles. The paper includes concrete examples of applying this debugger to programs.

We've seen a paper on compiling dataflow languages, so here's one on an interesting application.

Lowering: A Static Optimization Technique for Transparent Functional Reactivity, Kimberley Burchett, Gregory H. Cooper, and Shriram Krishnamurthi. PEPM 2007.

Functional Reactive Programming (FRP) extends traditional functional programming with dataflow evaluation, making it possible to write interactive programs in a declarative style. An FRP language creates a dynamic graph of data dependencies and reacts to changes by propagating updates through the graph. In a transparent FRP language, the primitive operators are implicitly lifted, so they construct graph nodes when they are applied to time-varying values. This model has some attractive properties, but it tends to produce a large graph that is costly to maintain. In this paper, we develop a transformation we call lowering, which improves performance by reducing the size of the graph. We present a static analysis that guides the sound application of this optimization, and we present benchmark results that demonstrate dramatic improvements in both speed and memory usage for real programs.

Whenever I read about compiler optimizations, I try (with mixed success) to relate them to transformations in the lambda calculus. I haven't managed to figure out what's going on with the dip construct the authors propose, but I would guess that the place to look is the proof theory of the necessity operator in modal logic -- dataflow programming can be seen as a kind of stream programming, and streams form a comonad over the lambda calculus, and comonads give semantics to the modal necessity (box) operator.

Extending Prolog with Incomplete Fuzzy Information. Susana Munoz-Hernandez, Claudio Vaucheret. 2005.

Our first work (Fuzzy Prolog) was a language that models $\mathcal{B}([0,1])$-valued Fuzzy Logic. In the Borel algebra, $\mathcal{B}([0,1])$, truth value is represented using unions of intervals of real numbers. This work was more general in truth value representation and propagation than previous works.
An interpreter for this language using Constraint Logic Programming over Real numbers (CLP(${\cal R}$)) was implemented and is available in the Ciao system. Now, we enhance our former approach by using default knowledge to represent incomplete information in Logic Programming. We also provide the implementation of this new framework. This new release of Fuzzy Prolog handles incomplete information, it has a complete semantics (the previous one was incomplete as Prolog) and moreover it is able to combine crisp and fuzzy logic in Prolog programs.

A project of related interest is Fril which as far as I remember wasn't discussed here.

Reform Prolog is a recursion-parallel implementation of Prolog. By executing all invocations of a recursive predicate in parallel, data-parallelism can be exploited. In contrast to most other parallel Prolog systems, Reform Prolog thus exploits structured parallelism; in contrast to present-day parallel Fortran systems, Reform Prolog can parallelize programs with procedure calls, pointer datastructures and arbitrary data dependences into doacross-style loops.

The Reform Prolog project ended in 1996 and somehow morphed into the High Performance Erlang project (which should be no surprise, as Erlang has clear roots in the Prolog world, though the concurrency model is different).

Logfun is a library of logic functors. A logic functor is a function that can be applied to zero, one or several logics so as to produce a new logic as a combination of argument logics. Each argument logic can itself be built by combination of logic functors. The signature of a logic is made of a parser and a printer of formulas, logical operations such as a theorem prover for entailment between formulas, and more specific operations required by Logical Information Systems (LIS). Logic functors can be concrete domains like integers, strings, or algebraic combinators like product or sum of logics.

Logic functors are coded as Objective Caml modules. A logic semantics is associated to each of these logic functors. This enables to define properties of logics like the consistency and completeness of the entailment prover, and to prove under which conditions a generated entailement prover satisfies these properties given the properties of argument logics.

Logic Functors form a framework for specifying new logics, and deriving automatically theorem provers and consistency/completeness diagnoses. Atomic functors are logics for manipulating symbols and concrete domains, while other functors are logic transformers that may add connectives or recursive structures, or may alter the semantics of a logic. The semantic structure of the framework is model theoretic as opposed to the verifunctional style often used in classical logic. This comes close to the semantics of description logics, and we show indeed that the logic ALC can be rebuilt using logic functors. This offers the immediate advantage that variants of ALC can be explored and implemented almost for free.

The use of OCaml functors here may be interesting even for those who aren't into logic languages. The system allows new logics to be created in OCaml itself, by simply composing OCaml functors. This is covered further in Implementation as ML Functors. The quickest way to get a feel for what this system does is to look at the examples.

SecPAL: Design and Semantics of a Decentralized Authorization Language. Moritz Y. Becker; Andrew D. Gordon; Cédric Fournet. September 2006

We present a declarative authorization language. Policies and credentials are expressed using predicates defined by logical clauses, in the style of constraint logic programming. Access requests are mapped to logical authorization queries, consisting of predicates and constraints combined by conjunctions, disjunctions, and negations. Access is granted if the query succeeds against the current database of clauses. Predicates ascribe rights to particular principals, with flexible support for delegation and revocation. At the discretion of the delegator, delegated rights can be further delegated, either to a fixed depth, or arbitrarily deeply.

Our language strikes a fine balance between semantic simplicity, policy expressiveness, and execution efficiency. The semantics consists of just three deduction rules. The language can express many common policy idioms using constraints, controlled delegation, recursive predicates, and negated queries. We describe an execution strategy based on translation to Datalog with constraints and table-based resolution. We show that this execution strategy is sound, complete, and always terminates, despite recursion and negation, as long as simple syntactic conditions are met.

The SecPAL project lives here (MSR). The project aims are to develop a language for expressing decentralized authorization policies, and to investigate language design and semantics, as well as related algorithms and analysis techniques.