Lambda the Ultimate

Causal Commutative Arrows and Their Optimization, Hai Liu. Eric Cheng. Paul Hudak. ICFP 2009.

Arrows are a popular form of abstract computation. Being more general than monads, they are more broadly applicable, and in particular are a good abstraction for signal processing and dataflow computations. Most notably, arrows form the basis for a domain specific language called Yampa, which has been used in a variety of concrete applications, including animation, robotics, sound synthesis, control systems, and graphical user interfaces.

Our primary interest is in better understanding the class of abstract computations captured by Yampa. Unfortunately, arrows are not concrete enough to do this with precision. To remedy this situation we introduce the concept of commutative arrows that capture a kind of non-interference property of concurrent computations. We also add an init operator, and identify a crucial law that captures the causal nature of arrow effects. We call the resulting computational model causal commutative arrows.

To study this class of computations in more detail, we define an extension to the simply typed lambda calculus called causal commutative arrows (CCA), and study its properties. Our key contribution is the identification of a normal form for CCA called causal commutative normal form (CCNF). By defining a normalization procedure we have developed an optimization strategy that yields dramatic improvements in performance over conventional implementations of arrows. We have implemented this technique in Haskell, and conducted benchmarks that validate the effectiveness of our approach. When combined with stream fusion, the overall methodology can result in speed-ups of greater than two orders of magnitude.

One way of understanding what is going on in this paper is that in terms of dataflow programming, FRP programs correspond to programs with single-entry, single-exit dataflow graphs. This means that none of the internal dataflow nodes in an FRP program are actually necessary -- you can coalesce all those nodes into a single node while preserving the observable behavior. (They briefly touch on this point when they mention that synchronous languages try to compile to "single loop code".) What's very slick is that they have a nice normal form procedure that (a) is defined entirely in terms of their high-level language, and (b) always yields code corresponding to the the coalesced dataflow graph. It's an elegant demonstration of the power of equational reasoning.

With its focus on sharing practical experiences, Code Generation 2010 is the ideal opportunity for software practitioners to understand how to benefit from emerging tools, technologies and approaches in the broad area of Model-Driven Software Development.

Accepted speakers have their conference fees waived.

For full details and instructions on how to submit a session please visit: http://www.codegeneration.net/cg2010/speak.php

Hear what participants thought about this year's conference in this short video clip:
http://www.youtube.com/watch?v=OsKQeuCCSvg

Call for Speakers:
Submission Deadline: Friday January 15th 2010

We are seeking high-quality session proposals covering topics in model-driven software development (including Domain-Specific Languages (DSLs), Model-Driven Architecture (MDA), Executable UML, Software Factories & Software Product Lines, Generative Programming and related areas). Sessions could cover topics such as:

- Tool and technology development and adoption
- Code Generation and Model Transformation tools and approaches
- Defining and implementing modelling languages
- Domain Analysis and Domain Engineering
- Language evolution and modularization
- Meta Modelling
- Runtime virtual machines versus direct code generation

Case studies and interactive sessions based on these and related approaches are particularly encouraged although more theoretical sessions are also welcome.

Take part in Code Generation 2010 and find out why it is Europe's leading event on Model-Driven Software Development.

What people said about our previous events:

"I've been working in domain-specific modelling for a dozen years … and in this time this has been the highest-quality conference on this topic that I've been to - and I've been to a few."

"The presentations were all top quality, making it often difficult to decide between the concurrently running sessions. The wealth of MDD knowledge present at the event was impressive, not only from the presenters, but from the other delegates as well."

Code Generation 2010 is organised by Software Acumen and supported by InfoQ.com, OMG, ACCU and SkillsMatter.

Suppose a small language with a few primitive types (number, boolean, string) and first-class procedures from and to these types with arbitrary but fixed arity, and the usual syntax (if, let, top-level definitions), but without type declarations. And suppose that the types of all primitive procedures (which are monomorphic) are given, and so is the type of the top-level procedure ("main", a procedure that is not invoked by any procedure, also monomorphic). The language is strict, if it matters.

What I'd like to have is an algorithm that can find the unique monomorphic type of all other procedures in a closed program, or prove that there is none. For example, in main = λ() f0; f = λ(x) gx; g = λ(x) fx, the procedures f and g have no unique monomorphic type, despite being Hindley-Milner typeable. So far I have figured out how to type a fair number of special cases, but I have no clue when to stop looking, or what to do when I run out of heuristics. It's definitely important that procedures can have procedure-valued arguments whose exact types (not merely the fact of being a procedure) must be reconstructed; without those, the problem is easily solved.

Can anyone help?

(Update: Actually, I'm wrong; that example is typeable. As I said, it's procedure-valued arguments that create problems.)