Fundamental Constructs in Programming Languages

When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves.

The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them.

This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics.

1. 1.

   https://plancomps.github.io.

2. 2.

   At the time of writing, the collection has not yet been released, and could change.

3. 3.

   Nowadays, a Unix command often has a multitude of obscure options, documented in a manual ‘page’ that fills many screens.

4. 4.

   Singular forms of type names are used as value constructors.

5. 5.

   Currently, Funcons-beta does not support namespaces in collections of funcons.

6. 6.

   Funcons have not yet been developed for ‘relaxed’ memory models or data marshalling.

7. 7.

   ‘L’ and ‘R’ refer to the left and right sides of typical assignment commands [32].

8. 8.

   Funcons for using un-typed locations as variables would be slightly simpler.

9. 9.

   https://pdmosses.github.io/prolog-msos-tool.

10. 10.

    https://pdmosses.github.io/msos-in-prolog.

11. 11.

    https://github.com/fcbr/mmt.

12. 12.

    See [20] for discussion of earlier uses of similar operations in denotational semantics.

Helpful comments on a previous version were provided by Thomas van Binsbergen, Cliff Jones, Neil Sculthorpe, members of the PL Group at Delft, and the anonymous reviewers. Thanks to the track organisers Klaus Havelund and Bernhard Steffen for extra space for the appendices.

The initial development of funcons was supported by an EPSRC grant to Swansea University for the PLanCompS project (EP/I032495/1). The author is now an emeritus at Swansea, and a visitor at Delft University of Technology.

Authors and Affiliations

1. Delft University of Technology, Delft, The Netherlands

   Peter D. Mosses

2. Swansea University, Swansea, UK

   Peter D. Mosses

Corresponding author

Correspondence to Peter D. Mosses .

Editors and Affiliations

1. University of Limerick, Limerick, Ireland

   Tiziana Margaria

2. TU Dortmund, Dortmund, Germany

   Bernhard Steffen

A Data

1.1 A.1 Datatypes

Primitive values. Conceptually, primitive values are atomic, and not formed from other values. For large (or infinite) types of primitive values, however, it is infeasible to declare a separate constant for each value. So in practice, funcons used to construct primitive values usually take other values as arguments.

• \({{\textsf {booleans}}}\) are the values \({{\textsf {true}}}\), \({{\textsf {false}}}\); funcons corresponding to the usual Boolean operations are defined.

• \({{\textsf {integers}}}\) is the built-in type of unbounded integers, with funcons for the usual mathematical operations. Funcons corresponding to associative binary operations are extended to arbitrary numbers of arguments. Subtypes include \({{\textsf {naturals}}}\) and \({{\textsf {bounded}}(M, N)}\); compositions with casts to such subtypes correspond to partial operations representing computer arithmetic.

• \({{\textsf {floats}}}\) is the built-in type of IEEE floating point numbers, with funcons for the required operations.

• \({{\textsf {characters}}}\) is the built-in type of all Unicode characters. Its subtypes include \({{\textsf {ascii}}\text {-}{\textsf {characters}}}\) and \({{\textsf {iso}}\text {-}{\textsf {latin}}\text {-}{\textsf {1}}\text {-}{\textsf {characters}}}\). Its funcons incude the UTF-8, UTF-16, and UTF-32 encodings of characters as byte sequences.

• \({{\textsf {null}}\text {-}{\textsf {type}}}\) has the single value \({{\textsf {null}}\text {-}{\textsf {value}}}\), alias \({{\textsf {null}}}\).

Composite values. Conceptually, composite values are constructed from finite sequences of argument values. The types of composite values include parametrised algebraic data types, with a generic representation. Various algebraic datatypes are defined, and new ones can be introduced. Composite values include also built-in parametrised types of sets, maps, multi-sets, and graphs.

Algebraic datatypes

• \({{\textsf {datatype}}\text {-}{\textsf {values}}}\) are generic representations for all algebraic datatype values.

• \({{\textsf {tuples}}( T_1, \cdots , T_n )}\) are grouped sequences of values of the specified types.

• \({{\textsf {lists}}(T)}\) are grouped sequences of values of type T, with the usual operations; \({{\textsf {strings}}}\) are lists of characters.

• \({{\textsf {vectors}}(T)}\) are grouped sequences of values of type T, accessed by index.

• \({{\textsf {trees}}(T)}\) are finite, with values of type T at nodes and leaves.

• \({{\textsf {references}}(T)}\) are values that refer to values of type T.

• \({{\textsf {pointers}}(T)}\) are references to values of type T or \({{\textsf {pointer}}\text {-}{\textsf {null}}}\).

• \({{\textsf {records}}(T)}\) are unordered aggregate values, indexed by identifiers.

• \({{\textsf {variants}}(T)}\) are pairs of identifiers and values of type T.

• \({{\textsf {classes}}}\) are collections of features, allowing multiple superclasses, used to classify objects.

• \({{\textsf {objects}}}\) are classified collections of features.

• \({{\textsf {bit}}\text {-}{\textsf {vectors}} ( N )}\) has instantiations for \({{\textsf {bits}}}\) and \({{\textsf {bytes}}}\).

Built-in datatypes

• \({{\textsf {sets}}(\textit{GT})}\) are finite sets of ground values of type \({\textit{GT}}\).

• \({{\textsf {maps}}(\textit{GT}, T^?)}\) are finite maps from type \({\textit{GT}}\) to type \(T^?\).

• \({{\textsf {multisets}}(\textit{GT})}\) are finite multisets of ground values of type \({\textit{GT}}\).

• \({{\textsf {directed}}\text {-}{\textsf {graphs}}(\textit{GT})}\) have values of type \({\textit{GT}}\) as vertices.

See [26] for funcons that operate on the above types of values.

1.2 A.2 Abstractions

Generic Abstractions. These non-ground values are used for constructing thunks, functions, and patterns. An abstraction body of computation type \(T \mathop {\Rightarrow }T'\) may refer to a given value of type T, and compute values of type \(T'\).

• \({{\textsf {abstractions}}(CT)}\) are procedural abstractions of computation type CT.

• \({{\textsf {abstraction}}(X)}\) constructs an abstraction with dynamic bindings.

• \({{\textsf {closure}} ( X )}\) computes an abstraction with static bindings.

• \({{\textsf {enact}} ( A )}\) evaluates the body of the abstraction A.

Thunks. The abstraction body of a thunk does not reference a given value.

• \({{\textsf {thunks}} ( T )}\) are constructed from abstractions with bodies of type \(( \ ) \mathop {\Rightarrow }T'\).

• \({{\textsf {thunk}}( A )}\) constructs a thunk from the abstraction A.

• \({{\textsf {force}}( V )}\) enacts the abstraction of the thunk V.

Functions. The abstraction body of a function may reference a given value.

• \({{\textsf {functions}}( T, T' )}\) are constructed from abstractions with bodies of type \(T \mathop {\Rightarrow }T'\).

• \({{\textsf {function}} ( {\textsf {abstraction}} ( X ) )}\) constructs a function with dynamic bindings.

• \({{\textsf {function}} ( {\textsf {closure}}( X ) )}\) computes a function with static bindings.

• \({{\textsf {apply}} ( F, V )}\) gives the value V to the body of the abstraction of function F.

• \({{\textsf {supply}}( F, V )}\) determines the argument value of a function application, but returns a thunk that defers evaluating the body of the function.

• \({{\textsf {compose}}( F_2, F_1 )}\) returns the function that first applies \(F_1\) then \(F_2\).

• \({{\textsf {curry}} ( F )}\) takes a function F that takes a pair of arguments, and returns the corresponding ‘curried’ function.

• \({{\textsf {uncurry}}( F )}\) takes a curried function F and returns a function that takes a pair of arguments.

• \({{\textsf {partial}}\text {-}{\textsf {apply}} ( F, V )}\) takes a function F that takes a pair of arguments, and determines the first argument, returning a function of the second argument.

Patterns. The abstractions of patterns match a given value.

• \({{\textsf {patterns}}}\) are constructed from abstractions with bodies of computation type \({{\textsf {values}} \mathop {\Rightarrow }{\textsf {environments}}}\).

• \({{\textsf {pattern}}(A)}\) constructs patterns from abstractions A.

• \({{\textsf {match}}(X, {\textsf {pattern}}(A))}\) enacts the abstraction A, giving it the value of X.

B Flow of Control

• \({{\textsf {left}}\text {-}{\textsf {to}}\text {-}{\textsf {right}} ( \cdots )}\) evaluates its arguments sequentially, and concatenates the computed value sequences. Composing it with a funcon having pre-computed arguments prevents interleaving; e.g., \({{\textsf {integer}}\text {-}{\textsf {add}} ( {\textsf {left}}\text {-}{\textsf {to}}\text {-}{\textsf {right}} ( X, Y ) )}\) always executes X before Y.

  \({{\textsf {right}}\text {-}{\textsf {to}}\text {-}{\textsf {left}} ( \cdots )}\) is analogous.

  \({{\textsf {interleave}} ( \cdots )}\) evaluates its arguments in any order, possibly with interleaving, and concatenates the computed value sequences.

• \({{\textsf {sequential}} ( X, \cdots )}\) executes the command X, then any remaining arguments, evaluating to the same value(s) as the last argument.

• \({{\textsf {effect}} ( \cdots )}\) interleaves the evaluations of its arguments, discarding their computed values, and gives \({{\textsf {null}}\text {-}{\textsf {value}}}\).

• \({{\textsf {choice}} ( Y, \cdots )}\) selects one of its arguments, then evaluates it.

• \({{\textsf {if}}\text {-}{\textsf {true}}\text {-}{\textsf {else}} ( B, X, Y )}\) evaluates B to a Boolean value, then evaluates either X or Y (which have to compute values of the same type).

• \({{\textsf {while}}\text {-}{\textsf {true}} ( B, X )}\) evaluates B to a Boolean value, then either executes X (which has to correspond to a command) and iterates, or terminates.

C Flow of Data

• \({{\textsf {given}}}\) evaluates to the current value of the auxiliary entity \({{\textsf {given}}\text {-}{\textsf {value}}}\).

• \({{\textsf {give}}( X, Y )}\) evaluates X. It then executes Y with the value of X as the value of the auxiliary entity \({{\textsf {given}}\text {-}{\textsf {value}}}\).

• \({{\textsf {left}}\text {-}{\textsf {to}}\text {-}{\textsf {right}}\text {-}{\textsf {map}} ( F, V^* )}\) evaluates F for each value in the sequence \(V^*\) in the same order, computing the sequence of resulting values.

  \({{\textsf {interleave}}\text {-}{\textsf {map}} ( F, V^* )}\) allows interleaving of the evaluations.

• \({{\textsf {left}}\text {-}{\textsf {to}}\text {-}{\textsf {right}}\text {-}{\textsf {repeat}}( F, M, N )}\) evaluates F for each integer from M up to N sequentially, computing the sequence of resulting values.

  \({{\textsf {interleave}}\text {-}{\textsf {repeat}} ( F, M, N )}\) allows interleaving of the evaluations.

• \({{\textsf {left}}\text {-}{\textsf {to}}\text {-}{\textsf {right}}\text {-}{\textsf {filter}} ( P, V^* )}\) evaluates P for each value in \(V^*\), computing the sequence of argument values for which the value of P is true.

  \({{\textsf {interleave}}\text {-}{\textsf {filter}} ( P, V^* )}\) allows interleaving of the evaluations.

• \({{\textsf {fold}}\text {-}{\textsf {left}} ( F, A, V^* )}\) reduces a sequence \(V^*\) to a single value by folding it from the left, using A as the initial accumulator value.

  \({{\textsf {fold}}\text {-}{\textsf {right}} ( F, A, V^* )}\) is analogous.

For any list L, the funcon term \({{\textsf {list}}\text {-}{\textsf {elements}}(L)}\) evaluates to the sequence \(V^*\) of elements in L, and \({{\textsf {list}}(V^*)}\) reconstructs L. Composition with these funcons allows the above funcons on sequences to be used with lists; similarly for vectors, sets, multisets, and the datatype of maps.

D Name Binding

• \({{\textsf {bind}}\text {-}{\textsf {value}} ( I, X )}\) computes the singleton environment mapping I to the value computed by X.

• \({{\textsf {unbind}} ( I )}\) computes an environment that hides the binding of I.

• \({{\textsf {bound}}\text {-}{\textsf {value}} ( I )}\) computes the value to which I is currently bound (possibly recursively, via a link), if any, and otherwise fails.

• \({{\textsf {scope}} ( D, X )}\) first evaluates D to compute an environment \(\rho \). It then extends the auxiliary environment entity with \(\rho \) for the execution of X.

• \({{\textsf {closed}} ( X )}\) prevents references to non-local bindings while evaluating X.

• \({{\textsf {accumulate}} ( D_1, D_2 )}\) first evaluates \(D_1\), to compute an environment \(\rho _1\). It then extends the auxiliary environment entity by \(\rho _1\) for the evaluation of \(D_2\), to compute an environment \(\rho _2\). The result is \(\rho _1\) extended by \(\rho _2\).

• \({{\textsf {collateral}} ( D_1, \cdots )}\) evaluates its arguments to compute environments. It returns their union as result, failing if their domains are not pairwise disjoint.

• \({{\textsf {bind}}\text {-}{\textsf {recursively}} ( I, X )}\) makes \({{\textsf {bind}}\text {-}{\textsf {value}} ( I, X )}\) recursive. It first computes a singleton environment \(\rho \) mapping I to a fresh link L. It then extends the auxiliary environment entity by \(\rho \) for the execution of X, to compute a value V. Finally, it sets L to refer to V, and gives \(\rho \) as the computed result.

• \({{\textsf {recursive}}( \textit{SI}, D )}\) makes D recursive on the identifiers in the set \({\textit{SI}}\). It first computes an environment \(\rho \) mapping all I in \({\textit{SI}}\) to fresh links. It then extends the auxiliary environment entity by \(\rho \) for the execution of D, to compute an environment \(\rho '\). Finally, it sets the link for each I to refer to the value of I in \(\rho '\), and gives \(\rho '\) as the computed result.

E Imperative Variables

• \({{\textsf {variables}}}\) is the type of all simple variables.

• \({{\textsf {allocate}}\text {-}{\textsf {variable}} ( T )}\) constructs a simple variable for storing values of type T in a location not in the current store.

• \({{\textsf {recycle}}\text {-}{\textsf {variables}}( \textit{Var}, \cdots )}\) removes locations allocated to variables from the current store.

• \({{\textsf {initialise}}\text {-}{\textsf {variable}}( \textit{Var}, V )}\) assigns V as the initial value of \({\textit{Var}}\).

• \({{\textsf {allocate}}\text {-}{\textsf {initialised}}\text {-}{\textsf {variable}}( T, V )}\) is a composition of \({{\textsf {allocate}}\text {-}{\textsf {variable}} ( T )}\) and \({{\textsf {initialise}}\text {-}{\textsf {variable}}( \_\,, V )}\).

• \({{\textsf {assign}}( \textit{Var}, V )}\) stores V at the location of \({\textit{Var}}\) when the type contains V.

• \({{\textsf {assigned}} ( \textit{Var} )}\) gives the value last assigned to \({\textit{Var}}\).

• \({{\textsf {current}}\text {-}{\textsf {value}} ( V )}\) gives the same result as \({{\textsf {assigned}} ( V )}\) when V is a simple variable, otherwise V.

• \({{\textsf {un}}\text {-}{\textsf {assign}} ( \textit{Var} )}\) makes \({\textit{Var}}\) uninitialised.

• \({{\textsf {structural}}\text {-}{\textsf {assign}} ( V_1, V_2 )}\) assigns to all the simple variables in \(V_1\) the corresponding values in \(V_2\), provided that the structure and all non-variable values in \(V_1\) match the structure and corresponding values of \(V_2\).

• \({{\textsf {structural}}\text {-}{\textsf {assigned}} ( V )}\) computes V with all simple variables replaced by their assigned values. When V is a simple variable or a value with no component variables, \({{\textsf {structural}}\text {-}{\textsf {assigned}} ( V )}\) gives the same result as \({{\textsf {current}}\text {-}{\textsf {value}} ( V )}\).

F Abrupt Termination

• \({{\textsf {abrupt}} ( V )}\) terminates abruptly for reason V.

• \({{\textsf {handle}}\text {-}{\textsf {abrupt}}( X, Y )}\) first executes X. If X terminates normally, Y is ignored. If X terminates abruptly for any reason, Y is executed, with the reason as the given value.

• \({{\textsf {finally}} ( X, Y )}\) first executes X. On normal or abrupt termination of X, it executes Y. If Y terminates normally, its computed value is ignored, and the funcon terminates in the same way as X; otherwise it terminates in the same way as Y.

• \({{\textsf {fail}}}\) abruptly terminates for reason \({{\textsf {failed}}}\).

• \({{\textsf {else}} ( X_1, X_2, \cdots )}\) executes the arguments in turn until either some \(X_i\) does not fail, or all arguments \(X_i\) have been executed. The last argument executed determines the result.

  \({{\textsf {else}}\text {-}{\textsf {choice}} ( X_1, X_2, \cdots )}\) is similar, but executes the arguments sequentially in any order.

• \({{\textsf {check}}\text {-}{\textsf {true}} ( X )}\) terminates normally if the value computed by X is \({{\textsf {true}}}\), and fails if it is \({{\textsf {false}}}\).

• \({{\textsf {checked}} ( X )}\) fails when X computes the empty sequence of values \(( \ )\), representing that a value has not been computed. It otherwise computes the same as X.

• \({{\textsf {throw}} ( V )}\) abruptly terminates for reason \({{\textsf {thrown}} ( V )}\).

  \({{\textsf {handle}}\text {-}{\textsf {thrown}}( X, Y )}\) handles abrupt termination of X for reason \({{\textsf {thrown}} ( V )}\) with Y.

  \({{\textsf {handle}}\text {-}{\textsf {recursively}}( X, Y )}\) is similar to \({{\textsf {handle}}\text {-}{\textsf {thrown}} ( X, Y )}\), except that another copy of the handler attempts to handle any values thrown by Y.

• \({{\textsf {return}} ( V )}\) abruptly terminates for reason \({{\textsf {returned}} ( V )}\).

  \({{\textsf {handle}}\text {-}{\textsf {return}} ( X )}\) evaluates X. If X either terminates abruptly for reason \({{\textsf {returned}} ( V )}\), or terminates normally with value V, it terminates normally giving V.

• \({{\textsf {break}}}\) abruptly terminates for reason \({{\textsf {broken}}}\).

  \({{\textsf {handle}}\text {-}{\textsf {break}} ( X )}\) terminates normally when X terminates abruptly for reason \({{\textsf {broken}}}\).

• \({{\textsf {continue}}}\) abruptly terminates for reason \({{\textsf {continued}}}\).

  \({{\textsf {handle}}\text {-}{\textsf {continue}} ( X )}\) terminates normally when X terminates abruptly for reason \({{\textsf {continued}}}\).

Further funcons are provided for expressing delimited continuations [26, 30].

G Communication

• \({{\textsf {read}}}\) inputs a single non-null value from the \({{\textsf {standard}}\text {-}{\textsf {in}}}\) entity, and gives it as the result.

• \({{\textsf {print}} ( V^* )}\) outputs the sequence of values \(V^*\) to the \({{\textsf {standard}}\text {-}{\textsf {out}}}\) entity.

Reprints and permissions

© 2021 Springer Nature Switzerland AG

Policies and ethics