Lambda the Ultimate

Viewpoints Research have published the first year's status report on their previously discussed project.

Eriskay: a Programming Language Based on Game Semantics. John Longley and Nicholas Wolverson. GaLoP 2008.

We report on an ongoing project to design a strongly typed, class-based object-oriented language based around ideas from game semantics. Part of our goal is to create a powerful modern programming language whose clean semantic basis renders it amenable to work in program verification; however, we argue that our semantically inspired approach also yields benefits of more immediate relevance to programmers, such as expressive new language constructs and novel type systems for enforcing security properties of the language. We describe a simple-minded game model with a rich mathematical structure, and explain how this model may be used to guide the design of our language. We then focus on three specific areas where our approach appears to offer something new: linear types and continuations; observational equivalence for class types; and static control of the use of higher-order store.

In a substantial appendix, we present the formal definition of a fragment of our language which embodies many of the innovative features of the full language.

It's always interesting to see a new programming language strongly based on some mathematical formalism, because a language gives you a concrete example to match the abstract semantic definitions to, and game semantics is something that I've been curious about for a while.

One particularly interesting feature is that the core language has a restricted model of the heap, which controls the use of higher-order store in such a way that cycles are prohibited. This is enforced with a notion called "argument safety", which essentially prohibits storing values of higher type into fields which come from "outside" the object. This is somewhat reminiscent of the ownership disciplines found in OO verification systems like Boogie, which enforce a tree structure on the ownership hierarchy. It would be very interesting to find out whether this resemblance is a coincidence or not.

(Samson Abramsky has some lecture notes on game semantics for the very curious.)

Applied Metamodelling: A Foundation for Language Driven Development (2004)
by Tony Clark, Paul Sammut, James Willans

An excerpt:

Language-driven development is fundamentally based on the ability to rapidly design new languages and tools in a unified and interoperable manner. We argue that existing technologies do not provide this capability, but a language engineering approach based on metamodelling can. The detailed study of metamodelling and how it can realise the Language-Driven Development vision will form the focus for the remainder of this book.

In software engineering circles the term "language driven development" is synonymous with "language oriented programming", a term which LtU members are more familiar with (thanks to Martin Ward's article Language Oriented Programming which first appeared in 1994, and then Martin Fowler's essays on the topic). The book hasn't appeared on the radar here on LtU, despite 41 citations. I suspect this is due in part to only one citation at Citeseer, and the lack of cross-talk between computer scientists and software engineers.

There are a lot of similarities between the XMF language (discussion at LtU) and that of the Katahdin language (discussion at LtU). Other related discussions here at LtU, include Language Workbenches: The Killer App for DSLs - about the essay by Martin Fowler, Ralph Johnson: Language workbenches - a response to Fowler's essay, XActium - Lightweight Language Engineering? - which discusses an essay about a previous version of XMF, Generating Interpreters? , Language Oriented Programming - discusses an essay by Jetbrain's Sergey Dmitriev, "Language Oriented Programming" Meta Programming System - discussion of the Jetbrain MPS system, The DSL, MDA, UML thing again... - an older discussion on the relationship between DSLs and MDA.

(Disclaimer: Some may notice that I am mentioned on the XMF web site, but this is just because I subjected their XMF language to a number of grueling challenges which they passed with flying colors: see the language snippets in the documentation. I have no affiliation with their company.)

Sliced bananas on opaque data (The expression lemma). Ralf Lämmel and Ondrej Rypacek.

Algebraic data types and catamorphisms (folds) play a central role in functional programming as they allow programmers to define recursive data structures and operations on them uniformly by structural recursion. Likewise, in object-oriented (OO) programming, recursive hierarchies of object types with virtual methods play a central role for the same reason. There is a semantical correspondence between these two situations which we reveal and formalize categorically. To this end, we assume a coalgebraic model of OO programming with functional objects. In practical terms, the development prepares for refactorings that turn sufficiently disciplined functional folds into OO programs of a designated shape (and v.v.).

I haven't even glanced at the paper yet, but it looks extremely interesting, and it's directly related to some recent discussion. This blog post from Ondrej is also relevant.

Uniqueness Typing Simplified, by Edsko de Vries, Rinus Plasmeijer, and David M. Abrahamson.

We present a uniqueness type system that is simpler than both Clean’s uniqueness system and a system we proposed previously. The new type system is straightforward to implement and add to existing compilers, and can easily be extended with advanced features such as higher rank types and impredicativity. We describe our implementation in Morrow, an experimental functional language with both these features. Finally, we prove soundness of the core type system with respect to the call-by-need lambda calculus.

Uniqueness typing is related to linear typing, and their differences have been discussed here before. Linear types have many applications. This paper describes the difference between linear and unique types:

In linear logic, variables of a non-linear type can be coerced to a linear type (dereliction). Harrington phrases it well: in linear logic, "linear" means "will not be duplicated" whereas in uniqueness typing, "unique" means "has not been duplicated".

In contrast to other papers on substructural typing, such as Fluet's thesis Monadic and Substructural Type Systems for Region-Based Memory Management, this paper classifies uniqueness attributes by a kind system. This possibility was mentioned in Fluet's thesis as well, Section 4.2, footnote 8, though the technique used here seems somewhat different.

Uniqueness typing is generally used to tame side-effects in purely functional languages. Uniqueness types have also been contrasted with monads on LTU, which are also used to tame effects, among other things. One point not discussed in that thread, is how straightforward it is to compile each approach into efficient code. It seems clear that uniqueness types have a straightforward, efficient compilation, but it's not clear to me how efficient monads can be, and how much work is required to make them efficient. This may make uniqueness or substructural types more suitable for just-in-time compilers than monads.

John Baez and Mike Stay are working on a book chapter titled "Categories in Physics, Topology, Logic and Computation: a Rosetta Stone." They previously asked for some help with the logic section, and now they're looking for help with the computation section:

But now I really need comments from anyone who likes categories and theoretical computer science!

In fact, the final 'computation' section of the paper is still very rough. It introduces combinators but doesn’t really explain them well yet... and perhaps worse, it doesn’t say anything about the lambda calculus!

I plan to fix some of these deficiencies in the next week. But, I figure it’s best to get comments and criticism now, while there’s still time to take it into account.

This is already a great introductory paper, but the computation section is indeed quite rough. Obviously comments are welcome, but even if you don't have anything to add, the first sections are sure to be enjoyable for many LtU readers. The paper does not assume any background in category theory, logic or physics and manages to be an excellent introduction to the surprising connections between these fields. If you have some background, it's a very quick and fun read, and if you can offer feedback, so much the better!

Via Scott Rosenberg (whose book Dreaming in Code I think we mentioned here before), I learn than Susan Lammers is making the interviews from her 1984 book Programmers At Work available on the Web.

Here is how she describes the goals of her new site:

Many people have urged me over the years to do a second Programmers At Work (PAW) with a new generation of programmers and I’ve sketched out the project, made lists of new folks to feature, done inquiries, thought about going back to talk to the guys in the original edition, and other variations . Now with this web site, I will make the original interviews available online, and perhaps it will become the seed for a more “thoroughly modern” approach to the PAW series. What I’m hoping we can kindle on this site is an ongoing exploration and dynamic conversation with the "connected" community of programmers on the web about the creative process in programming.

Who better than the LtU community to contribute to such a conversation?

The first PAW interview posted to the site is the interview with Charles Simonyi, a man whose views of the future of programming, and programming languages, are mentioned here often (though not always with great enthusiasm).

Data Types a la Carte. Wouter Swierstra.

This paper describes a technique for assembling both data types and functions from isolated individual components. We also explore how the same technology can be used to combine free monads and, as a result, structure Haskell’s monolithic IO monad.

This new Functional Pearl has been mentioned twice in comments (1, 2), and has now also appeared with comments on Phil Wadler's blog. Obviously it's time to put it on the front page.

We present decidable logic programs for addition, multiplication, division with remainder, exponentiation, and logarithm with remainder over the unbounded domain of natural numbers. Our predicates represent relations without mode restrictions or annotations. They are fully decidable under the common, DFS-like, SLD resolution strategy of Prolog or under an interleaving refinement of DFS...

[The] attempts to define decidable multiplication even for the seemingly trivial unary case show the difficulties that become more pronounced as we move to binary arithmetic. We rely on a finite representation of infinite domains, precise instantiatedness analysis, and reasoning about SLD using search trees.

So you've read The Reasoned Schemer and were excited about the fact that unlike the built-in operations in Prolog, arithmetic relations (over binary numbers) were fully implemented. For example, addition could also be used for subtraction and multiplication for factoring numbers and for generating all triples of numbers related by multiplication. Now comes this paper to explain the motivation behind some of the more arcane definitions needed to implement arithmetic in a fully relational style, and to prove their properties formally. The paper develops unary and binary arithmetic relations in pure Prolog (with no cuts, negation or introspection).

LtU readers will also be interested in yet another embedding of pure Prolog into Haskell, that the authors offer. It is not meant to be the most optimal or convenient Prolog implementation (it wasn't even intended to be an implementation of a logic system). It was explicitly designed to be easier to reason about and so help prove certain properties of SLD or similar evaluation strategies. The main difference of DefinitionTree from other embeddings of Prolog in Haskell has to do with the generation of fresh names for logic variables. In DefinitionTree, name generation is not an effect, and the naming is fully decoupled from the evaluation. The evaluation no longer needs to carry a state for the generation of fresh names, hence the evaluator is easier to reason about equationally.

Foundations for Structured Programming with GADTs, Patricia Johann and Neil Ghani. POPL 2008.

GADTs are at the cutting edge of functional programming and become more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory of datatypes as carriers of initial algebras of functors can be extended from algebraic and nested data types to GADTs. We then use this observation to derive an initial algebra semantics for GADTs, thus ensuring that all of the accumulated knowledge about initial algebras can be brought to bear on them. Next, we use our initial algebra semantics for GADTs to derive expressive and principled tools -- analogous to the well-known and widely-used ones for algebraic and nested data types -- for reasoning about, programming with, and improving the performance of programs involving, GADTs; we christen such a collection of tools for a GADT an initial algebra package. Along the way, we give a constructive demonstration that every GADT can be reduced to one which uses only the equality GADT and existential quantification. Although other such reductions exist in the literature, ours is entirely local, is independent of any particular syntactic presentation of GADTs, and can be implemented in the host language, rather than existing solely as a metatheoretical artifact. The main technical ideas underlying our approach are (i) to modify the notion of a higher-order functor so that GADTs can be seen as carriers of initial algebras of higher-order functors, and (ii) to use left Kan extensions to trade arbitrary GADTs for simpler-but-equivalent ones for which initial algebra semantics can be derived.

I found this to be a really interesting paper, because the work had an opposite effect on my opinions from what I expected. Usually, when I see a paper give a really clean semantics to an idea, I end up convinced that this is actually a good idea. However, Johann and Ghani gave a really elegant treatment of GADTs, which had the effect of making me think that perhaps Haskell-style GADTs should not be added as is to new programming languages!

This is because of the way they give semantics to GADTs as functors |C| -> C, where C is the usual semantic category (eg, CPPO) and |C| is the discrete category formed from C that retains the objects and only the identity morphisms. If I understand rightly, this illustrates that the indices in a GADT are only being used as index terms, and their structure as types is going unused. So it's really kind of a pun, arising from the accident that Haskell has * as its only base kind. This makes me think that future languages should include indices, but that these index domains should not coincide with kind type. That is, users should be able to define new kinds distinct from *, and use those as indexes to types, and these are the datatypes which should get a semantics in the style of this paper.