Goffin: Higher-Order Functions Meet Concurrent Constraints

Manuel M. T. Chakravarty, Yike Guo, Martin Köhler, and Hendrik C. R. Lock

Science of Computer Programming 30(1-2), pp 157-199, 1998. (Revised version of a paper presented at the First International Workshop on Concurrent Constraint Programming, 1995.)

We introduce a higher-order constraint-based language for structured and declarative parallel programming. The language, called Goffin, systematically integrates constraints and functions within a uniform setting of concurrent programming.

From the point of parallel programming methodology, the constraint part of Goffin provides a co-ordination language for the functional part, which takes on the role of the computation language. This conceptual distinction allows the structured formulation of parallel algorithms.

Goffin is an extension of the purely functional language Haskell. The functional kernel is embedded in a layer based on concurrent constraints. Logical variables are bound by constraints which impose relations over expressions that may contain user-defined functions. Referential transparency is preserved by restricting the creation of logical variables to the constraint part and by suspending the reduction of functional expressions that depend on the value of an unbound logical variable. Hence, constraints are the means to organize the concurrent reduction of functional expressions. Moreover, constraint abstractions, i.e., functions over constraints, allow the definition of parameterized co-ordination forms. In correspondence with the higher-order nature of the functional part, abstractions in the constraint logic part are based on higher-order logic, leading to concise and modular specifications of behaviour.

We introduce and explain Goffin together with its underlying programming methodology, and present a declarative as well as an operational semantics for the language. In order to formalize the semantics, we identify the essential core constructs of the language and characterize their declarative meaning by associating them with formulae of Church's Simple Theory of Types. Afterwards, we present a reduction system that captures the concurrent operational semantics of the core constructs. Finally, the soundness of this reduction system with respect to the declarative semantics is established.

PostScript version (Preprint) (51 pages)

This page is part of Manuel Chakravarty's WWW-stuff.