Lambda the Ultimate

The machine learning community has started to realize the importance of expressive languages for specifying probabilistic models and also executing those models (i.e., performing "inference" by computing conditional distributions). A number of "probabilistic programming languages" have been proposed by machine learning/AI researches recently--Pfeffer's IBAL, and Goodman, Mansinghka, my, and Tenenbaum's CHURCH, and Winn's CSOFT.

Outside of the ML community, I know of a few languages, including Park, Pfenning, and Thrun's PTP, and Erwig and Kollmansberger's PFP/Haskell. In general, the work by ML researchers places more emphasis on the conditional execution of probabilistic programs (e.g., asking about the value of some variable given that the entire program takes on a particular value).

Of possible interest to the PL community are a number of interesting relationships between ideas in probability theory and programming languages (when used to specify so-called generative models). One of these is that purity/referential-transparency relaxes in the probabilistic setting to exchangeability (a property of a probability distribution being invariant to reordering). Other interesting theoretical connections relate to relaxed notions of halting (e.g., halting with probability one) and their effects on statistical inference (this is particularly relevant for so-called nonparametric distributions; e.g., see a recent workshop abstract of mine).

Along with my colleagues (Vikash Mansinghka (MIT), John Winn (MSR Cambridge), David McAllester (TTI-Chicago) and Joshua Tenenbaum (MIT)), we are organizing a workshop at the NIPS*2008 conference. While I've been reading LtU for some time, I've joined now to announce this workshop to the PL community because we definitely need the PL communities help in solving some open problems.

Probabilistic inference algorithms are very complicated beasts and writing universal inference algorithms that take as specifications "probabilistic programs" seems, at first blush, to implicate program analysis, compilation, partial evaluation and a host of other ideas from programming languages.

If these questions pique your interest, visit the workshop website:

http://probabilistic-programming.org

and also drop me an email (droy at mit edu). I hope to see some of you in Whistler this December.

I've just finished my master's thesis on the parallel shift. It covers why threading, in most cases, isn't a suitable programming model for extracting parallel performance, how we still can extract performance out it and what desired parallel programming models need to consider.

I expect a lot of people in this forum are more knowledgeable in computer languages than I am. Therefore, I would very much like some comments on what I've written, especially the first part. Or better yet - a discussion :)

You can find the thesis at www.johantorp.com

Best Regards, Johan Torp

ABSTRACT
Part 1 - A bird's eye view of desktop parallelism,
Part 2 - Zooming in on C++0x's memory model

The first part of the thesis is an overview of the paradigmatic shift to parallelism that is currently taking place. It explains why processors need to become parallel, how they might function and which types of parallelism there are. Given that information, it explains why threads and locks is not a suitable programming model and how threading is being improved and used to extract parallel performance. It also covers the problems that await new parallel programming models and how they might work. The final chapter surveys the landscape of existing parallel software and hardware projects and relates them to the overview. The overview is intended for programmers and architects of desktop and embedded systems.

The second part explains how to use C++'s upcoming memory model and atomic API. It also relates the memory model to classical definitions of distributed computing in an attempt to bridge the gap in terminology between the research literature and C++. An implementation of hazard pointers and a lock-free stack and queue are given as example C++0x code. This part is aimed at expert C++ developers and the research community.

I feel incredibly silly posting this, but I could use some pointers.

There seem to be two schools of function specification: one in which all function types are expressed as T1 -> T2, and the other in which function types are expressed as T1 x T2 x ... Tn -> Tout. The difference here is that the second makes function arity part of the type.

In BitC, we initially chose the N-ary functions because I was slow figuring out how to make C's void type come out right. Later, we retained it because I thought that arity checking was important. That is, given a function:

(define (f x y) ...)

it seemed like a good thing to be able to notice that:

(f 1 2 3)

was a malformed call because the number of arguments do not agree. The alternative was to define application to occur by pair consing (similar to Scheme style, but with using an unboxed construction):

(f 1 2 3) =>
(f (1, 2, 3))

My concern about this is that type checking doesn't accomplish arity checking in the case where the type of the last parameter to the function is parametric. That is, if we get a function f whose type is something like:

(int32, float, 'a) -> bool

then you'll get to pass as many arguments as you want.

The N-ary function thing is now getting in our way, and I would like to switch to something like the pair-consed view. There seem to be three resolutions:

• Conclude that losing the arity check when the last parameter is polymorphic is survivable.
• Check arity as a separate syntactic matter that is independent from type.
• Ask how other people have dealt with this.

So: how do other polymorphic languages handle this?