Implementing Declarative Parallel Bottom-Avoiding Choice

Implementing Declarative Parallel Bottom-Avoiding Choice. Andre Rauber Du Bois, Robert Pointon, Hans-Wolfgang Loidl, Phil Trinder. Symposium on Computer Architecture and High Performance Computing (SBAC-PAD) 2002.

Non-deterministic choice supports efficient parallel speculation, but unrestricted non-determinism destroys the referential transparency of purely-declarative languages by removing unfoldability and it bears the danger of wasting resources on unncessary computations. While numerous choice mechanisms have been proposed that preserve unfoldability, and some concurrent implementations exist, we believe that no compiled parallel implementation has previously been constructed. This paper presents the design, smantics, implementation and use of a family of bottom-avoiding choice operators for Glasgow parallel Haskell. The subtle semantic properties of our choice operations are described, including a careful classification using an existing framework, together with a discussion of operational semantics issues and the pragmatics of distributed memory implementation.

amb breaks referential transparency (e.g., think about (\x.x+x)(3 amb 5) - how many choice points are there?)

This paper presents the problems, and shows how to implementat bottom-avoiding choice operators in Galsgow parallel Haskell (GPH).

The paper is worth checking out for the references alone, which can server as a useful guide to the subject of non-determinism in functional languages. Section 3 of the paper summarizes the semantic properties of the choice operators, and can be a good place to start reading if you are familiar with the subject.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Thoughts

In this area, I think the research community is missing the boat in some important ways.

First of all, with "amb", there are really two kinds of bottom that really ought to be distinct: the notion of "no values", and the notion of divergence due to a never-ending computation. Call the former "nothing" and the later "bot" (Haskell folks write _|_ for bot.)

Computing with "nothing" is very simple and well-founded. "nothing amb x" and "x amb nothing" are equivalant to "x". McAllester's Ontic language takes the amb operator a lot further than McCarthy had original envisioned, and enables one to bundle up collections of amb values into set-like types. Ontic's syntax for this is "the-set-of-all x".

This "the-set-of-all x" construct is the microscope under which "nothing" and "bot" are revealed to be distinct concepts. In a type containing a bunch of amb values, some of which may be divergent, it's impossible to perform any useful operations except for positively verifying that an element is a member. Membership can't be refuted, because that requires executing a divergent computation. The only way bottom-avoiding choice can be made usable is with a Prolog-style Cut operator, whose results are nondeterministic and likely to be unpredictable and weird in practice.

Thus I'm a big believer in amb as a fundamental programming construct, and "nothing"-avoiding choice is trivial in this system, but "bot"-avoiding choice seems an impractical and unhelpful tool in language design.

Note on the poster's comment on amb breaking referential transparency: When amb is implemented correctly (with proper sharing of choice points), it's referentially transparent.

For example, (\x.x+x)(3 amb 5) beta-converts to let x=(3 amb 5) in x+x, which reduces to (let x=3 in x+x) amb (let x=5 in x+x), which reduces to 6 amb 10.

This can be summarized as "only single-valued terms evaluate to values; zero-valued or multi-valued terms must be treated as references to a single, shared choice point".

Another way of visualizing terms like (\x.x+x)(3 amb 5) is to translate them to Haskell comprehensions: [x+x | x <- [3,5]].

Another example is "let x=nothing in 7" must evaluate to nothing, not 7. This is obvious from the comprehension [7 | x<-[]]. At first, this seems counterintuitive because we tend to think of any expression you can write as evaluating to a value, whereas with "amb", only single-valued terms evaluate to values; the ordinary substitution rules don't apply where multiple values are present.

Jan Kuper's thesis

there are really two kinds of bottom that really ought to be distinct: the notion of "no values", and the notion of divergence due to a never-ending computation.

Jan Kuper's PhD thesis "Partiality in Logic and Computation - Aspects of Undefinedness" might interest you.

Don't Know vs. Don't Care Nondeterminism

These concepts are explained nicely in Ehud Shapiro, The family of concurrent logic programming languages (alas, this requires ACM DL subscription).

The list monad

I was already thinking that the list monad works a bit like ambivalence. Now that I see you converting the amb operator to list comprehensions, I'm wondering: what are the differences?

List Monad vs Amb

The only differences between a list comprehension and a similar computation involving amb are that list comprehensions are explicitly ordered, and duplicate items remain distinct. Amb values are set-like and don't have any inherent order or multiplicity to them; (2 amb 3) is equivalant to (3 anb 2) and (2 amb 2) is equivalant to 2.

If you ignore the underlying order and multiplicity of lists, you can use the list monad to precisely model the behaviour of amb. You can actually define a "set monad" this way. For example, the set monad's join is the union (of a set of sets); its zero is the empty set; its unit forms singleton sets; its plus takes the union of a pair of sets; it's map takes the image of a given function under a given set...each of the monad laws in the set monad happens to be a ZFC axiom.