Introduction

Functional nets have a theoretical foundation in join calculus [9, 10]. They have the same relation to join calculus as classical functional programming has to lambda calculus. That is, functional nets constitute a programming method which derives much of its simplicity and elegance from close connections to a fundamental underlying calculus. lambda calculus [6, 3] is ideally suited as a basis for functional programs, but it can support mutable state only indirectly, and nondeterminism and concurrency not at all. The pair of join calculus and functional nets has much broader applicability -- functional, imperative and concurrent program constructions are supported with equal ease.

The purpose of this paper is two-fold. First, it aims to promote functional nets as an interesting programming method of wide applicability. We present a sequence of examples which show how functional nets can concisely model key constructs of functional, imperative, and concurrent programming, and how they often lead to better solutions to programming problems than conventional methods.

Second, the paper develops concepts to link our programming notation of functional nets with the underlying calculus. To scale up from a calculus to a programming language, it is essential to have a means of aggregating functions and data. We introduce qualified definitions as a new syntactic construct for aggregation. In the context of functional nets, qualified definitions provide more flexible control over visibility and initialization than the more conventional record- or object-constructors. They are also an excellent fit to the underlying join calculus, since they maintain the convention that every value has a name. We will present object-based join calculus, an extension of join calculus with qualified definitions. This extension comes at surprisingly low cost, in the sense that the calculus needs to be changed only minimally and all concepts carry over unchanged. By contrast, conventional record constructors would create anonymous values, which would be at odds with the name-passing nature of join.

The notation for writing examples of functional nets is derived from Funnel, a small language which maps directly into our object-based extension of join. An implementation of Funnel is publicly available. There are also other languages which are based in some form on join calculus, and which express the constructs of functional nets in a different way, e.g. Join [11] or JoCaml [8]. We have chosen to develop and present a new notation since we wanted to support both functions and objects in a way which was as simple as possible.

As every program notation should be, functional nets are intended to be strongly typed, in the sense that all type errors should be detected rather than leading to unspecified behavior. We leave open whether type checking is done statically at compile time or dynamically at run time. Our examples do not mention types, but they are all of a form that would be checkable using a standard type system with recursive records, subtyping and polymorphism.

The rest of this paper is structured as follows. Section 2 introduces functional nets and qualified definitions. Sections 3 and 4 show how common functional and imperative programming patterns can be modeled as functional nets. Section 5 discusses concurrency and shows how functional nets model a wide spectrum of process synchronization techniques. Section 6 introduces object-based join calculus as the formal foundation of functional nets. Section 7 discusses how the programming notation used in previous sections can be encoded in this calculus. Section 9 discusses related work and concludes.

A First Example

def get & full x     =  x & empty,
    put x & empty    =  () & full x

get & full x  =  x & empty

put x & empty   =  () & full x

def get & full x     =  x  & empty,
    put x & empty    =  () & full x;

put 1 &
 ( val y = get ; val r = y + y ; print r ; put r ) &
 ( val z = get ; val r = y * y ; print r; put r ) &
 empty

val y = get ; ...

As usual, a semicolon between expressions stands for sequencing. The combined expression print r; put r first prints its argument r and then puts it into the buffer. The sequence in which the client processes in the above example execute is arbitrary, controlled only by the buffer's rewrite rules. The effect of running the example program is hence the output of two numbers, either (2, 4) or (1, 2), depending which client process came first.

Objects

def newBuffer = {
  def get & full x     =  x  & empty,
      put x & empty    =  () & full x;
  (get, put) & empty
};
val (get', put') = newBuffer;
put' 1 &
 ( val y = get' ; val r = y + y ; print r ; put' r ) &
 ( val z = get' ; val r = y * y ; print r ; put' r )

This representation is feasible as long as objects have only a few externally visible methods, but for objects with many methods the resulting long tuples quickly become unmanageable. Furthermore, tuples do not support a notion of subtyping, where an object can be substituted for another one with fewer methods. We therefore introduce records as a more suitable means of aggregation where individual methods can be accessed by their names, and subtyping is possible.

The idiom for record access is standard. If r denotes a record, then r.f denotes the field of r named f. We also call references of the form r.f qualified names. The idiom for record creation is less conventional. In most programming languages, records are defined by enumerating all field names with their values. This notion interacts poorly with the forms of definitions employed in functional nets. In a functional net, one often wants to export only some of the functions defined in a join pattern whereas other functions should remain hidden. Moreover, it is often necessary to call some of the hidden functions as part of the object's initialization.

To streamline the construction of objects, we introduce qualified names not only for record accesses, but also for record definitions. For instance, here is a re-formulation of the newBuffer function using qualified definitions.

def newBuffer = {
  def this.get & full x      =  x  & empty,
      this.put x & empty     =  () & full x;
  this & empty
};
val buf = newBuffer;
buf.put 1 &
 ( val y = buf.get ; val r = y + y ; print r ; buf.put r ) &
 ( val z = buf.get ; val r = y * y ; print r ; buf.put r )

• the local name this, which denotes a record with two fields, get and put, and
• local names empty and full, which denote functions.

The identifiers which occur before a period in a join pattern always define new record names, which are defined only in the enclosing definition. It is not possible to use this form of qualified definition to add new fields to a record defined elsewhere.

Some Notes on Syntax. We assume the following order of precedence, from strong to weak:

( ) and (.)   ,    (&)   ,   (=)   ,   (,)   ,   (;)   .

As a syntactic convenience, we allow indentation instead of ;-separators inside blocks delimited with braces { and }. Except for the significance of indentation, braces are equivalent to parentheses. The rules are as follows: (1) in a block delimited with braces, a semicolon is inserted in front of any non-empty line which starts at the same indentation level as the first symbol following the opening brace, provided the symbol after the insertion point can start an expression or definition. The only modification to this rule is: (2) if inserted semicolons would separate two def blocks, yielding def D1 ; def D2 say, then the two def blocks are instead merged into a single block, i.e. def D1, D2. (3) The top level program is treated like a block delimited with braces, i.e. indentation is significant.

With these rules, the newBuffer example can alternatively be written as follows.

def newBuffer = {
  def this.get & full x      =  x  & empty
  def this.put x & empty     =  () & full x
  this & empty
}
val buf = newBuffer
buf.put 1 &
 { val y = buf.get ; val r = y + y ; print r ; buf.put r } &
 { val z = buf.get ; val r = y * y ; print r ; buf.put r }

( def this.f = ... , this.g = ... ; this )

( def f = ... , g = ... )

Functional Programming

def factorial n  =  if (n == 0) 1
                    else n * factorial (n-1)

Functional programs often work with recursive data structures such as trees and lists. In Lisp or Scheme such data structures are primitive S-expressions, whereas in ML or Haskell they are definable as algebraic data types. Our functional net notation does not have a primitive tree type, nor has it constructs for defining algebraic data types and for pattern matching their values. It does not need to, since these constructs can be represented with records, using the Visitor pattern [12].

The visitor pattern is the object-oriented version of the standard Church encoding of algebraic data types. A visitor encodes the branches of a pattern matching case expression. It is represented as a record with one method for each branch. For instance, a visitor for lists would always have two methods:

def Nil = ...
def Cons (x, xs) = ...

Assume we have already defined a method match for lists that takes a list visitor as argument and has the behavior just described. Then one could write an isEmpty test function over lists as follows:

def isEmpty xs = xs.match {
  def Nil = true
  def Cons (x, xs1) = false
}

val List = {
  def Nil          =  { def match v = v.Nil }
  def Cons (x, xs) =  { def match v = v.Cons (x, xs) }
}

def concat (xs, ys) = xs.match {
  def Nil = ys
  def Cons (x, xs) = List.Cons (x, concat (xs1, ys))
}

Imperative Programming

def newRef initial  =  {
  def this.value      & state x  =  x  & state x,
      this.update y   & state x  =  () & state y
  this & state initial
}

val count = newRef 0
def increment  =  count.update (count.value + 1)
increment

    var x := E    expands to    val _x = newRef E ; def x = _x.value
    x := E        expands to    _x.update E

var count := 0
def increment  =  count := count + 1

Functional nets have no predefined operation which tests whether two names or references are the same. However, it is still possible to implement an eq method. Here's our first attempt, which still needs to be refined later.

def newObjectWithIdentity  =  {
  def this.eq other    & flag x  =  resetFlag (other.testFlag & flag true)
      this.testFlag    & flag x  =  x & flag x
      resetFlag result & flag x  =  x & flag false
  this & flag false
}

Concurrency

Functional nets support an resource-based view of concurrency, where calls model resources, & expresses conjunction of resources, and a definition acts as a rewrite rule which maps input sets of resources into output sets of resources. This view is very similar to the one of Petri nets [18, 21]. In fact, there are direct analogies between the elements of Petri nets and functional nets.

A transition in a Petri net corresponds to a rewrite rule in a functional net. A place in a Petri net corresponds to a function symbol applied to some (formal or actual) arguments. A token in a Petri net corresponds to some actual call during the execution of a functional net (in analogy to Petri nets, we will also call applications of asynchronous functions tokens). The basic execution step of a Petri net is the firing of a transition which has as a precondition that all in-going places have tokens in them. Quite similarly, the basic execution step of a functional net is a rewriting according to some rewrite rule, which has as a precondition that all function symbols of the rule's left-hand side have matching calls.

Functional nets are considerably more powerful than conventional Petri nets, however. First, function applications in a functional net can have arguments, whereas tokens in a Petri net are unstructured. Second, functions in a functional net can be higher-order, in that they can have functions as their arguments. In Petri nets, such self-referentiality is not possible. Third, definitions in a functional net can be nested inside rewrite rules, such that evolving net topologies are possible. A Petri-net, on the other hand, has a fixed connection structure.

Colored Petri nets [16] let one pass parameters along the arrows connecting places with transitions. These nets are equivalent to first-order functional nets with only global definitions. They still cannot express the higher-order and evolution aspects of functional nets. Bussi and Asperti have translated join calculus ideas into standard Petri net formalisms. Their mobile Petri nets \cite{bussi-asperti:mobile-petri-nets} support first-class functions and evolution, and drop at the same time the locality restrictions of join calculus and functional nets. That is, their notation separates function name introduction from rewrite rule definition, and allows a function to be defined collectively by several unrelated definitions.

In the following, we will present several well-known schemes for process synchronization and how they each can be expressed as functional nets.

Semaphores. A common mechanism for process synchronization is a lock (or: semaphore). A lock offers two atomic actions: getLock and releaseLock. Here's the implementation of a lock as a functional net:

def newLock = {
  def this.getLock & this.releaseLock  =  ()
  this & this.releaseLock
}

val s = newLock ; ...
s.getLock ; ``< critical region >'' ; s.releaseLock

val global = newLock
def newObjectWithIdentity  =  {
  def this.eq other = global.getLock ; this.testEq other ; global.releaseLock
      this.testEq other & flag x  =  resetFlag (other.testFlag & flag true)
      this.testFlag & flag x  =  x & flag x
      resetFlag result & flag x  =  x & flag false
  this & flag false
}

Asynchronous Channels. Quite similar to a semaphore is the definition of an asynchronous channel with two operations, read and write:

def newAsyncChannel = {
  def this.read & this.write x  =  x
  this
}

val c = newAsyncChannel
def producer = {
  var x := 1
  while (true) { val y := x ; x := x + 1 & c.write y }
}
def consumer = {
  while (true) { val y = c.read ; print y }
}
producer & consumer

Synchronous Channels. A potential problem with the previous example is that the producer might produce data much more rapidly than the consumer consumes them. In this case, the number of pending write operations might increase indefinitely, or until memory was exhausted. The problem can be avoided by connecting producer and consumer with a synchronous channel.

In a synchronous channel, both reads and writes return and each operation blocks until the other operation is called. Synchronous channels are the fundamental communication primitive of classical pi calculus [17]. They can be represented as functional nets as follows.

def newSyncChannel = {
  def this.read & noReads     =  read1 & read2,
      this.write x & noWrites =  write1 & write2 x,
      read1 & write2 x        =  x & noWrites,
      write1 & read2          =  () & noReads
  this
}

val c = newSyncChannel
def producer = {
  var x := 1
  while (true) { c.write x  ;  x := x + 1 }
}
def consumer = {
  while (true) { val y = c.read  ;  print y }
}
producer & consumer

Monitors. Another scheme for process communication is to use a common store made up of mutable variables, and to use mutual exclusion mechanisms to prevent multiple processes from updating the same variable at the same time. A simple mutual exclusion mechanism is the monitor [13, 14] which ensures that only one of a set of functions f1, ..., fk can be active at any one time. A monitor is easily represented using an additional asynchronous function, turn. The turn token acts as a resource which is consumed at the start of each function fi and which is reproduced at the end:

def f1 & turn  =    ... ; turn,
         ...
    fk & turn  =    ... ; turn

def newBiCounter  =  {
  var count := 0
  def this.increment & turn  \==  count := count + 1 ; turn
  def this.decrement & turn \>=  count := count - 1 ; turn
  this
}  

• there can be multiple concurrent readers,
• there can only be one writer at one time,
• pending write requests have priority over pending read requests, but don't preempt ongoing read operations.

Initial solution:

  def this.startRead  & writers 0  =  startRead1,
          startRead1  & readers n  =  () & writers 0 & readers (n+1),
      this.startWrite & writers n  =  startWrite1 & writers (n+1),
          startWrite1 & readers 0  =  (),
      this.endRead    & readers n  =  readers (n-1),
      this.endWrite   & writers n  =  writers (n-1) & readers 0
  this & readers 0 & writers 0
}

This solution is simple enough to trust its correctness. But the present formulation is not yet valid Funnel because we have made use of numeric arguments in join patterns. For instance readers 0 expresses the condition that the number of readers is zero. We arrive at an equivalent formulation in Funnel through factorization. A function such as readers which represents a condition is split into several sub-functions which together partition the condition into its cases of interest. In our case we should have a token noReaders which expresses the fact that there are no ongoing reads as well as a token readers n, where n is now required to be positive. Similarly, writers n is now augmented by a case noWriters. After splitting and introducing the necessary case distinctions, one obtains the following functional net:

After factorization:

def newReadersWriters = {
  def this.startRead  & noWriters  =  startRead1,
          startRead1  & noReaders  =  () & noWriters & readers 1,
          startRead1  & readers n  =  () & noWriters & readers (n+1),
      this.startWrite & noWriters  =  startWrite1 & writers 1,
      this.startWrite & writers n  =  startWrite1 & writers (n+1),
          startWrite1 & noReaders  =  (),
      this.endRead    & readers n  =  if (n == 1) noReaders 
                                      else readers (n-1),
      this.endWrite   & writers n  =  noReaders &
                                      if (n == 1) noWriters 
                                      else writers (n-1)
  this & noReaders & noWriters
}