Functional Nets
by Martin Odersky


  First Example




This is an excerpt from a paper to appear in Proceedings of the European Symposium on Programming 2000, Lecture Notes in Computer Science, (c) Springer Verlag. The full paper can be downloaded as a postscript file.


Functional nets are a way to think about programs and computation which is born from a fusion of the essential ideas of functional programming and Petri nets. As in functional programming, the basic computation step in a functional net rewrites function applications to function bodies. As in Petri-Nets, a rewrite step can require the combined presence of several inputs (where in this case inputs are function applications). This fusion of ideas from two different areas results in a style of programming which is at the same time very simple and very expressive.

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

Consider the task of implementing a one-place buffer, which connects producers and consumers of data. Producers call a function put to deposit data into the buffer while consumers call a function get to retrieve data from the buffer. There can be at most one datum in the buffer at any one time. A put operation on a buffer which is already full blocks until the buffer is empty. Likewise, a get on an empty buffer blocks until the buffer is full. This specification is realized by the following simple functional net:
def get & full x     =  x & empty,
    put x & empty    =  () & full x
The net contains two definitions which together define four functions. Two of the functions, put and get, are meant to be called from the producer and consumer clients of the buffer. The other two, full and empty, reflect the buffer's internal state, and should be called only from within the buffer. Function put takes a single argument, x. We often write a function argument without surrounding parentheses, e.g. put x instead of put(x). We also admit functions like get that do not take any argument; one can imagine that every occurrence of such a function is augmented by an implicit empty tuple as argument, e.g. get becomes get(). The two equations define rewrite rules. A set of function calls that matches the left-hand side of an equation may be rewritten to the equation's right-hand side. The & symbol denotes parallel composition. We sometimes call & a fork if it appears on an equation's right-hand side, and a {\em join} if it appears on the left. Consequently, the left-hand sides of equations are also called join patterns. For instance, the equation
get & full x  =  x & empty
states that if there are two concurrent calls, one to get and the other to full x for some value x, then those calls may be rewritten to the expression x & empty. That expression returns x as get's result and in parallel calls function empty. Unlike get, empty does not return a result; it's sole purpose is to enable via the second rewrite rule calls to put to proceed. We call result-returning functions like get synchronous, whereas functions like empty are called asynchronous. In general, only the leftmost operand of a fork or a join can return a result. All function symbols of a left-hand side but the first one are asynchronous. Likewise, all operands of a fork except the first one are asynchronous or their result is discarded. It's now easy to interpret the second rewrite rule,
put x & empty   =  () & full x
This rule states that two concurrent calls to put x & empty and may be rewritten to () & full x. The result part of that expression is the unit value (); it signals termination and otherwise carries no interesting information. Clients of the buffer still need to initialize it by calling empty. A simple usage of the one-place buffer is illustrated in the following example.
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 ) &
Besides the initializer empty there are three client processes composed in parallel. One process puts the number 1 into the buffer. The other two processes both try to get the buffer's contents and put back a modified value. The construct
val y = get ; ...
evaluates the right-hand side expression get and defines y as a name for the resulting value. The defined name y remains visible in the expression following the semicolon. By contrast, if we had written def y = get; ... we would have defined a function y, which each time it was called would call in turn get. The definition itself would not evaluate anything.

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.


The previous example mixed the definition of a one-place buffer and the client program using it. A better de-coupling is obtained by defining a constructor function for one-place buffers. The constructor, together with a program using it can be written as follows.
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 )
The defining equations of a one-place buffer are now local to a block, from which the pair of locally defined functions get and put is returned. Parallel to returning the result the buffer is initialized by calling empty. The initializer empty is now part of the constructor function; clients no longer can call it explicitly, since empty is defined in a local block and not returned as result of that block. Hence, newBuffer defines an object with externally visible methods get and put and private methods empty and full. The object is represented by a tuple which contains all externally visible methods.

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 )
Note the occurrence of the qualified names this.get and this.put on the left-hand side of the local definitions. These definitions introduce three local names:
  • the local name this, which denotes a record with two fields, get and put, and
  • local names empty and full, which denote functions.
Note that the naming of this is arbitrary, any other name would work equally well. Note also that empty and full are not part of the record returned from newRef, so that they can be accessed only internally.

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 (.)   ,    (&)   ,   (=)   ,   (,)   ,   (;)   .
That is, function application and selection bind strongest, followed by parallel composition, followed by the equal sign, followed by comma, and finally followed by semicolon. Function application and selection are left associative, & is associative, and ; is right associatve. Other standard operators such as +, *, == fall between function application and & in their usual order of precedence. When precedence risks being unclear, we'll use parentheses to disambiguate.

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 }
A common special case of a qualified definition is the definition of a record with only externally visible methods:
( def this.f = ... , this.g = ... ; this )
This idiom can be abbreviated by omitting the this qualifier and writing only the definitions.
( def f = ... , g = ... )

Functional Programming

A functional net that does not contain any occurrences of & is a purely functional program. For example, here's the factorial function written as a functional net.
def factorial n  =  if (n == 0) 1
                    else n * factorial (n-1)
Except for minor syntactical details, there's nothing which distinguishes this program from a program written in a functional language like Haskell or ML. We assume that evaluation of function arguments is strict: In the call f (g x), g x will be evaluated first and its value will be passed to f.

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) = ...
The intention is that our translation of pattern matching would call either the Nil method or the Cons method of a given visitor, depending what kind of list was encountered. If the encountered list resulted from a Cons we also need to pass the arguments of the original Cons to the visitor's Cons.

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
More generally, every function over lists can be defined in terms of match. So, in order to define a record which represents a list, all we need to do is to provide a match method. How should match be defined? Clearly, its behavior will depend on whether it is called on an empty or non-empty list. Therefore, we define two list constructors Nil and Cons, with two different different implementations for match. The implementations are straightforward:
val List = {
  def Nil          =  { def match v = v.Nil }
  def Cons (x, xs) =  { def match v = v.Cons (x, xs) }
In each case, match simply calls the appropriate method of its visitor argument v, passing any parameters along. We have chosen to wrap the Nil and Cons constructors in another record, named List. List acts as a module, which provides the constructors of the list data type. Clients of the List module then construct lists using qualified names List.Nil and List.Cons. Example:
def concat (xs, ys) = xs.match {
  def Nil = ys
  def Cons (x, xs) = List.Cons (x, concat (xs1, ys))
Note that the qualification with List lets us distinguish the constructor Cons, defined in List, from the visitor method Cons, which is defined locally.

Imperative Programming

Imperative programming extends purely functional programming with the addition of mutable variables. A mutable variable can be modeled as a reference cell object, which can be constructed as follows.
def newRef initial  =  {
  def this.value      & state x  =  x  & state x,
      this.update y   & state x  =  () & state y
  this & state initial
The structure of these definitions is similar to the one-place buffer in Section 2. The two synchronous functions value and update access and update the variable's current value. The asynchronous function state serves to remember the variable's current value. The reference cell is initialized by calling state with the initial value. Here is a simple example of how references are used:
val count = newRef 0
def increment  =  count.update (count.value + 1)
Building on reference cell objects, we can express the usual variable access notation of imperative languages by two simple syntactic expansions:
    var x := E    expands to    val _x = newRef E ; def x = _x.value
    x := E        expands to    _x.update E
The count example above could then be written more conventionally as follows.
var count := 0
def increment  =  count := count + 1
In the object-oriented design and programming area, an object is often characterized as having ``state, behavior, and identity''. Our encoding of objects expresses state as a collection of applications of private asynchronous functions, and behavior as a collection of externally visible functions. But what about identity? If functional net objects had an observable identity it should be possible to define a method eq which returns true if and only if its argument is the same object as the current object. Here ``sameness'' has to be interpreted as ``created by the same operation'', structural equality is not enough. E.g., assuming that the -- as yet hypothetical -- eq method was added to reference objects, it should be possible to write val (r1, r2) = (newRef 0, newRef 0) and to have r1.eq(r1) == true and r1.eq(r2) == false.

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
This defines a generator function for objects with an eq method that tests for identity. The implementation of eq relies on three helper functions, flag, testFlag, and resetFlag. Between calls to the eq method, flag false is always asserted. The trick is that the eq method asserts flag true and at the same time tests whether other.flag is true. If the current object and the other object are the same, that test will yield true. On the other hand, if the current object and the other object are different, the test will yield false, provided there is not at the same time another ongoing eq operation on object other. Hence, we have arrived at a solution of our problem, provided we can prevent overlapping eq operations on the same objects. In the next section, we will develop techniques to do so.


The previous sections have shown how functional nets can express sequential programs, both in functional and in imperative style. In this section, we will show their utility in expressing common patterns of concurrent program execution.

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
A typical usage of a semaphore would be:
val s = newLock ; ...
s.getLock ; ``< critical region >'' ; s.releaseLock
With semaphores, we can now complete our example to define objects with identity:
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
This code makes use of a global lock to serialize all calls of eq methods. This is admittedly a brute force approach to mutual exclusion, which also serializes calls to eq over disjoint pairs of objects. A more refined locking strategy is hard to come by, however. Conceptually, a critical region consists of a pair of objects which both have to be locked. A naive approach would lock first one object, then the other. But this would carry the risk of deadlocks, when two concurrent eq operations involve the same objects, but in different order.

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

def newAsyncChannel = {
  def & this.write x  =  x
Asynchronous channels are the fundamental communication primitive of asynchronous pi calculus [5, 15] and languages based on it, e.g. Pict [19] or Piccola [1]. A typical usage scenario of an asynchronous channel would be:
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 = ; print y }
producer & consumer
The producer in the above scenario writes consecutive integers to the channel c which are read and printed by the consumer. The writing is done asynchronously, in parallel to the rest of the body of the producer's while loop. Hence, there is no guarantee that numbers will be read and printed in the same order as they were written.

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 & noReads     =  read1 & read2,
      this.write x & noWrites =  write1 & write2 x,
      read1 & write2 x        =  x & noWrites,
      write1 & read2          =  () & noReads
This implementation is more involved than the one for asynchronous channels. The added complexity stems from the fact that a synchronous channel connects two synchronous operations, yet in each join pattern there can be only one function that returns. Our solution is similar to a double handshake protocol. It splits up read and write into two sub-operations each, read1, read2 and write1, write2. The sub-operations are then matched in two join patterns, in opposite senses. In one pattern it is the read sub-operation which returns whereas in the second one it is the write sub-operation. The noReads and noWrites tokens are necessary for serializing reads and writes, so that a second write operation can only start after the previous read operation is finished and vice versa. With synchronous channels, our producer/consumer example can be written as follows.
val c = newSyncChannel
def producer = {
  var x := 1
  while (true) { c.write x  ;  x := x + 1 }
def consumer = {
  while (true) { val y =  ;  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
For instance, here is an example of a counter which can be incremented and decremented:
def newBiCounter  =  {
  var count := 0
  def this.increment & turn  \==  count := count + 1 ; turn
  def this.decrement & turn \>=  count := count - 1 ; turn
Readers and Writers. A more complex form of synchronization distinguishes between readers which access a common resource without modifying it and writers which can both access and modify it. To synchronize readers and writers we need to implement operations startRead, startWrite, endRead, endWrite, such that:
  • 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.
This form of access control is common in databases. It can be implemented using traditional synchronization mechanisms such as semaphores, but this is far from trivial. We arrive at a functional net solution to the problem in two steps:

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
In the initial solution we make use of two auxiliary tokens. The token readers n keeps track in its argument n of the number of ongoing reads, while writers n keeps track in n of the number of {\em pending} writes. A startRead operation requires that there are no pending writes to proceed, i.e. writers 0 must be asserted. In that case, startRead continues with startRead1, which reasserts writers 0, increments the number of ongoing readers, and returns to its caller. By contrast, a startWrite operation immediately increments the number of pending writes. It then continues with startWrite1, which waits for the number of readers to be 0 and then returns. Note the almost-symmetry between startRead and startWrite, where the different order of actions reflects the different priorities of readers and writers.

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

         Funnel - Functional Nets - LAMP