Chapter 1

Functional Concepts in C++

Rose H. Abdul Rauf^{1}, Ulrich Berger^{2}, Anton Setzer^{2} ^{3}

Abstract: We describe a parser-translator program that translates typed λ-terms into C++ classes so as to integrate functional concepts. We prove the correctness of the translation of λ-terms into C++ with respect to a denotational semantics using a Kripke-style logical relation. We also introduce a general technique for introducing lazy evaluation into C++ and illustrate it by carrying out in C++ the example of computing the Fibonacci numbers efficiently using infinite streams and lazy evaluation.

1.1 INTRODUCTION

C++ is a general purpose language that supports object oriented programming as well as procedural and generic programming, but unfortunately not directly functional programming. We have developed a parser-translator program that translates typed λ-terms into C++ statements so as to integrate functional concepts. The translated code uses the object oriented approach of programming that involves the creation of classes for the λ-term. By using inheritance, we achieve that the translation of a λ-abstraction is an element of a function type.

The paper is organised as follows: First, we introduce the translation and discuss how the translated code is executed including a description of the memory allocation (Sect. 1.2). The correctness of our implementation is proved with respect to the usual (set-theoretic) denotational semantics of the simply typed λ-calculus and a mathematical model of a sufficiently large fragment of C++. The proof is based on a Kripke-style logical relation between C++ values and denotational values (Sect. 1.3). In Sect. 1.4 we introduce a general technique for introducing lazy evaluation into C++ by introducing a data type of lazy elements of an arbitrary C++ type.

1Faculty of Information System and Quantitative Science, University of Technology MARA, 40450 Shah Alam, Selangor D.E., Malaysia; Email:

hafsah@tmsk.uitm.edu.my

2Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK; Email: {u.berger,a.g.setzer}@swansea.ac.uk

3Supported by EPSRC grant GR/S30450/01

Related work. Several researchers [7], [8] have discovered that C++ can be used for functional programming by representing higher order functions using classes. Our representation is based on similar ideas. There are other approaches that have made C++ a language that can be used for functional programming such as the FC++ library [9] (a very elaborate approach) as well as FACT! [19] (extensive use of templates and overloading) and [7] (creating macros that allow creation of single macro-closure in C++). The advantages of our solution are that it is very simple, it uses classes and inheritance in an essential way, it can be used for implementing λ-terms with side-effects, and, most importantly, we have a formal correctness proof.

The approach of using denotational semantics and logical relations for proving program correctness has been used before by Plotkin [12], Reynolds [14] and many others. The method of logical relations can be traced back at least to Tait [20] and has been used for various purposes, for example, for proving normalization (Tait [20]), computational adequacy (Plotkin [12]) and completeness (Jung and Tiuryn [5], Statman [18], Plotkin [13]). To our knowledge the verification of the implementation of the λ-calculus in C++ (and related object-oriented languages) using logical relations is new.

There are other fragments of object-oriented languages in the literature which are used to prove the correctness of programs. A well-known example is Featherweight Java ([4]). The model for this language avoids the use of a heap, since methods do not modify instance variables. In contrast, our model of C++ does make use of a heap and is therefore closer to the actual implementation of C++. Although our fragment of C++ does not allow for methods with side effects, it could easily be extended this way and then used to verify programs in C++ using side effects. This could be used, for instance, to prove the efficiency of the Lazy construct introduced in Sect. 1.4.

Lazy evaluation in C++ has been studied extensively in the literature (see e.g. [15], [9], [6]). To our knowledge, all implementations are restricted to lazy lists, whereas we introduce a general type of lazy elements of an arbitrary type, which not only corresponds to call-by-name (which is usually achieved by replacing a type A by () → A), but also guarantees that elements are only evaluated once, as required by true lazy evaluation. Note as well that there is no need to add a new delay construct to C++ since our implementation of laziness makes use of the existing language of C++ only.

1.2 TRANSLATION OF TYPED λ-TERMS INTO C++

In this section we describe how to translate simply typed λ-terms into C++ using the object-oriented concepts of classes and inheritance.

The simply typed λ-calculus, λ-calculus for short, is given as follows: We assume a set basetype of base types ρ,σ,..., and a set F of basic functions from base types to base types. Any native C++ type can be used as a base type, and any native C++ function without side effects can be used as a basic function. ^{4}

Types are elements of basetype, and function types A → B (if A,B are types). Terms are of the form x (variables), λx^{A}r (abstraction), r s (application), f[r_{1},...,r_{n}] (function application; f ∈ F),^{5} where r,s,r_{i} are terms. We treat constants, c, as basic functions with no arguments, and write in this case c instead of c[ ].

A context is a finite set of pairs Γ = x_{1} : A_{1},...,x_{n} : A_{n} (all x_{i} distinct) which is, as usual, identified with a finite map.

We let Type, Var, Term, Context denote the set of types, variables, terms and contexts, respectively. The typing rules are as usual:

Γ,x: A ⊢ x: A  \frac{Γ,x: A ⊢ r: B}{Γ ⊢ λx^{A}r: A → B}  \frac{Γ ⊢ r: A → B  Γ ⊢ s: A}{Γ ⊢ r s: B}
\frac{Γ ⊢ r_{1} : σ_{1}...Γ ⊢ r_{k}: σ_{k}}{Γ ⊢ f[r_{1},...,r_{k}] : ρ} (f a basic function of type σ_{1} → ···→ σ_{k} → ρ)

We now show how to translate λ-terms into C++. The translation is essentially the same as that given by the parsing function P introduced in Sect. 1.3 – the only difference is that P will be developed in an abstract setting, whereas the translation given in the following generates genuine C++ code.

Our translation generates new identifiers, which we need to disambiguate; in order for this to work, we restrict ourselves to the translation of finitely many λterms and types at a time. We first define an identifier name(a) : String for finitely many a: Type. Here String is the set of strings.

• If A is a native C++-type, name(A) is a C++ identifier obtained from A. This is A, if A is already an identifier, and the result of removing blanks and modifying symbols not allowed in identifiers (e.g. replacing ∗ by x), in case A is a compound type like longint or ∗ A.^{6}

• name(A → B) :=“C”∗name(A)∗“ ”∗name(B)∗“D”, where ∗ means concatenation. Here C stands for an open bracket, D for a closing bracket, and for the arrow in this identifier. By using these symbols we obtain valid C++- identifiers.^{7} For instance name(int → int) =“Cint intD”, name((int → int) → int) = “CCint intD intD”. In the following, we write CA BD instead of name(A → B) and CA BD aux instead of name(A → B)∗” aux” (this type will be introduced below), similarly for other types.

4The translation given below makes sense as well for functions with side effects, including those which affect instance variables of the classes used. However, in this case we would go beyond the simply typed λ-calculus, and could not use the simple denotational semantics of the λ-calculus in order to express the correctness of the translation.

5Note that we do not have any product types and that native C++-functions are not necessarily objects – they can even be constants such as integers – therefore f[r_{1},...,r_{k}] cannot be subsumed by the rule for r s.

6This modification might result in name clashes, in which case one adds some string like n for some integer n in order to disambiguate the names. Since we are translating only finitely many λ-types at any time, this way of avoiding name clashes is always possible.

7Again, we might need to disambiguate the identifiers as it was done for native C++ types.

For every A ∈ Type we introduce a series of class definitions, after which name(A) is a valid C++ type (assuming class definitions for any native C++ type used):

• For native C++-types the sequence of class definitions is empty.

• The sequence of class definitions for A → B consists of the class definitions of A, the class definitions of B not contained in the class definitions of A and additionally

class CA_BD_aux{
  public: virtual B operator () (A x)=0;};
typedef CA_BD_aux * CA_BD;

So, CA BD aux is a class with one virtual method used as application, which maps an element of type A to an element of type B. CA BD is a pointer to an element of this class.

Now we define for every λ-term t a sequence of C++-class definitions and a C++- term t^{C++} , s.t. if t : A, then t^{C++} is of type name(A). ^{8}

• If x is a variable, then the class definitions for introducing x are empty and x^{C++} := x.

• Assume A = E → F, t = λx^{A}.r. Assume the free variables of t are of type x_{1} : A_{1},...,x_{n} : A_{n} and that t is a new identifier. Assume name(A_{i}) = Ai, xi is the C++-representation for x_{i}, name(E) = E, name(F) = F, and r^{C++} = r. The class definition for t consists of the class definition for r together with

class t : CE_FD_aux{
  public:
     A1 x1;
     ...
     An xn;
     t(A1 x1,A2 x2, ... , An xn){
          this->x1 = x1;
          ...
          this->xn = xn;}
     virtual F operator () (E x){
           return r;};};

8Strictly speaking, t^{C++} depends on the choice of identifiers for λ-types and C++-classes representing λ-terms. When defining the parse function P in Sect. 1.3, this will be made explicit by having the dependency of this function on the context Γ and the class environment C. Since in our abstract setting λ-types are represented by themselves, P does not depend on the choice of identifiers for those types.

t^{C++} := newt(x1,...,xn).

• Assume t = r s. Then the class definitions of t consist of the class definitions for r, and the class definitions for s (where the class definitions corresponding to λ-abstractions occurring in both r and s need to be introduced only once).^{9} Furthermore t^{C++} := (∗(r^{C++} ))(s^{C++} ).

• Assume t = f[r_{1},...,r_{n}]. Then the class definitions for t are the class definitions for r_{i} (again class definitions for λ-terms occurring more than once need only to be introduced once). Furthermore, t^{C++} := f(r_{1}^{C++} ,...,r_{n}^{C++} ).

Note that a λ-abstraction is interpreted as a function of its free variables in the form (newt(x_{1},...,x_{n})). Hence, the evaluation of a λ-abstraction in an environment for the free variables is similar to a “closure” in implementations of functional programming languages.

We have developed a program which parses λ-terms and translates them into C++. Our intention is to upgrade this to an extension of the language of C++ by λ-types and -terms together with a parser program which translates this extended language into native C++. For this purpose we introduce a syntax for representing λ-types and -terms in C++. We use functional style notation rather than overloading existing C++-notation, since we belief that this will improve readability and acceptability of our approach by functional programmers. In our extended language, we write A –> B for the function type A → B, r^^s for the application of r to s,^{10}and \Ax.Bs for λx^{A}.s, if s: B. (If s is a term starting with λ, B will be omitted). For instance, the term

t = (λf^{int→int} λx^{int}.f (f x)) (λx^{int}.x + 2) 3

is written in our extended C++ syntax as

(\int->int f. \int x. int f^^(f^^x))^^(\int x. int x+2)^^3

We will use this extended syntax in our C++ implementation of lazy data structures (Sect. 1.4).

As an example, we show how the translation program transforms the term t above into native C++ code. We begin with the class definitions for the λ-types:

class Cint_intD_aux
{ public : virtual int operator() (int x) = 0; };
typedef Cint_intD_aux*  Cint_intD;

9A λ-abstraction is represented as a new instance of its corresponding class. Even if the classes for two occurrences of the same λ-abstraction coincide, for each occurrence a new instance is created. Therefore there is no problem, if a variable occurs as the same name, but with different referential meaning in two identical λ-expressions.

10Note that we cannot r(s) here, since this notation will not translate into application, but into (∗ r)(s).

class CCint_intD_Cint_intDD_aux
{  public : virtual Cint_intD operator()
                                 (Cint_intD x) = 0; };
typedef CCint_intD_Cint_intDD_aux*
         CCint_intD_Cint_intDD;

The class definition for t_{1} := λx^{int}.f (f x) is

class t1 : public Cint_intD_aux{
 public :Cint_intD f;
 t1( Cint_intD f)  {   this-> f = f;};
 virtual int operator () (int x)
 { return (*(f))((*(f))(x)); };
};

and t_{1}^{C++} = newt1(f). The class definitions for t_{0} := λf^{int→int} λx^{int}.f(fx) and t_{2} := λx^{int}.2 + x (using identifiers t0, t2) are as follows:

class t0 : public CCint_intD_Cint_intDD_aux{
 public :
 t0( ) { };
 virtual Cint_intD operator () (Cint_intD f)
 { return new  t1( f); }
};
 class t2 : public Cint_intD_aux{
 public :
 t2( ) { };
 virtual int operator () (int x)
 { return x + 2; };
};

Finally

t^{C++} := (∗((∗( newt0( )))( newt2( ))))(3);

When evaluating the expression t^{C++} , first the application of t0 to t2 is evaluated. To this end, instances l0, l2 of the classes t0 and t2 are created first. Then the operator() method of l0 is called. This call creates an instance l1 of t1, with the instance variable f set to l2. The result of applying t0 to t2 is l1.

The next step in the evaluation of t^{C++} is to evaluate 3, and then to call the operator() method of l1. This will first make a call to the operator method of f, which is bound to l2, and apply it to 3. This will evaluate to 5. Then it will call the operator method of f again, which is still bound to l2, and apply it to the result 5. The result returned is 7.

We see that the evaluation of the expression above follows the call-by-value evaluation strategy.^{11} Note that l0, l1, l2 were created on the heap, but have not been deleted afterwards. The deletion of l0, l1 and l2 relies on the use of a garbage collected version of C++, alternatively we could use smart pointers in order to enforce their deletion.

11Note that this computation causes some overhead, since for every subterm of the form λx.r a new object is created, which is in many cases used once, and can be thrown away

1.3 PROOF OF CORRECTNESS

We now prove the correctness of our C++ implementation of the λ-calculus. For notational simplicity we restrict ourselves to the base type int of integers. By “correctness” we mean that every closed term r of type int is evaluated by our implementation to a numeral which coincides with the value of r. The value of a term can be defined either operationally as the normal form w.r.t. β-reduction, (λx^{A}r)s →_{β} r[s/x], and function reduction, f[n_{1},...,n_{k}] →_{f} n (n the value of f at n_{1},...,n_{k}), or, equivalently, denotationally as the natural value in a suitable domain of functionals of finite types. Since our calculus does not allow for recursive definitions, the details of the operational and denotational semantics do not matter: Operationally, any sufficiently complete reduction strategy (call-by-value, call-by-name, full normalisation) will do, and denotationally, any Cartesian closed category containing the type of integers can be used. For our purposes it is most convenient to work with a denotational model, for example, the naive set-theoretic hierarchy D of functionals of finite types over the integers^{12} (setting Z = {...,−2,−1,0,1,2,...} and X → Y = {f | f : X → Y }):

D(int) = Z, D(A → B) = D(A) → D(B), D = ⋃_{A∈Type}D(A)

A functional environment is a mapping ξ: Var → D. FEnv denotes the set of all functional environments. If Γ is a context, then ξ: Γ means ∀x ∈ dom(Γ).ξ(x) ∈ D(Γ(x)).

For every typed λ-term Γ ⊢ r : A and every functional environment ξ : Γ the denotational value [[r]]ξ ∈ D(A) is defined by

i) [[n]]ξ = n

ii) [[x]]ξ = ξ(x)

iii) [[r s]]ξ = [[r]]ξ([[s]]ξ)

iv) [[λx^{A}.r]]ξ(a) = [[r]]ξ[x ↦ a]

v) [[f[r⃗]]] = [[f]]([[r⃗]]ξ)

where in the last clause [[f]] is the number-theoretic function denoted by f. Our implementation of the λ-calculus is modelled in a similar way as e.g. in [1] using functions eval and apply, but, in order to model the C++ implementation as truthfully as possible, we make the pointer structures for the classes and objects explicit by letting the functions eval and apply modify these pointer structures via side effects.

afterwards. One could optimize this, however at the price of having a much more complicated translation, and therefore a much more complex correctness proof of the translation.

12Recursion can be interpreted in a domain-theoretic model [12].

We model only the fragment of C++ that we used in Section 1.2 to translate the simply typed λ-calculus into C++. Hence we assume that classes have instance variables, one constructor, and one method corresponding to the operator() method. The constructor has one argument for each instance variable and sets the instance variables to these arguments. No other code is performed. The method has one argument, and the body consists of an applicative term, where applicative terms are simplified C++ expressions in our model. So, a class is given by a context representing its instance variables, the abstracted variable of the method and its type, and an applicative term.

Applicative terms are numbers, variables, function terms applied to applicative terms, the application of one applicative term to another applicative term (which corresponds to the method call in case the first applicative term is an object), or a constructor applied to applicative terms.

When a constructor call of a class is evaluated, its arguments are first evaluated. Then, memory for the instance variables of this class is allocated on the heap, and these instance variables are set to the evaluated arguments. The address to this memory location is the result returned by evaluating this constructor call. The only other possible result of the evaluation of an applicative term is a number, so values are addresses or numbers. Hence, the data sets associated with our model of C++ classes are defined as follows (letting X + Y and X × Y denote the disjoint sum and Cartesian product of X and Y, X^{∗} the set of finite lists of elements in X and X →_{fin} Y the set of finite maps from X to Y):

Addr  = a set of numbers denoting addresses of classes on the heap
Constr = a set of strings denoting constructors, i.e. class names
Val  = Z + Addr
F  = a set of names for arithmetic C++ functions
App  = Z + Var + F × App^{∗}+ App × App + Constr × App^{∗}
Context = Var →_{fin} Type
Class  = Context × Var × Type × App
VEnv  = Var →_{fin} Val
Heap  = Addr →_{fin} Constr × Val^{∗}
CEnv  = Constr →_{fin} Class

Applicative terms (∈ App), which we write as n, x, f[a_{1},...,a_{n}], (a b) and c[a_{1},...,a_{n}], correspond to the C++ constructs n, x, f(a_{1},...,a_{n}), (∗ (a))(b) and newc(a_{1},...,a_{n}), while classes (∈ Class), written in the form (Γ;x : A;b) with Γ = x_{1} : A_{1},...,x_{n}: A_{n}, correspond to a C++ class definition of the form

class c : CA_BD_aux{
  public: A1 x1;
           ...
           An xn;
  c(A1 x1,A2 x2, ... , An xn){

                  this->x1 = x1;
                  ...
                  this->xn = xn;}
  virtual B operator () (A x){
                 return b;};};

The type B is omitted in (Γ;x: A;b) since it can be derived, and the class name c is associated with the class through the class environment CEnv.

The fact that the parsing function as well as the functions eval and apply have side effects on the classes and the heap can be conveniently expressed using a partial state monad (the object part of which is)

M_{X}(Y) := X →^{∼} Y × X

where X →^{∼} Y × X is the set of partial functions from X to Y × X. Elements of M_{X}(Y) are called actions and can be viewed as elements of Y that may depend on a current state x ∈ X and also may change the current state. Monads are a category-theoretic concept whose computational significance was discovered by Moggi [10]. We need to work with partial instead of total functions because the operations eval and apply defined below do not yield defined results in general. We will however prove that for inputs generated by translating well-typed λ-terms the results will always be defined.

Using the monad terminology the functionalities of the parsing function P and the operations eval and apply can now be written as

P : Context → Term → M_{CEnv}(App)
eval : CEnv → VEnv → App → M_{Heap}(Val)
apply : CEnv → Val → Val → M_{Heap}(Val)

Hence, parsing has a side effect on the class environment, while eval and apply have side effects on the heap. The function P corresponds to the assignment t ↦ t^{C++} introduced in Section 1.2, but makes the dependencies on the context and the class environment explicit.

We use the following standard monadic notation (roughly following Haskell syntax): Suppose e_{1} : M_{X}(Y_{1}), …, e_{k+1} : M_{X}(Y_{k+1}) are actions where e_{i} may depend on y_{1} : Y_{1}, …, y_{i−1} : Y_{i−1} . Then

do{y_{1} ← e_{1} ; ... ; y_{k} ← e_{k}; e_{k+1}}: M_{X}(Y_{k+1})

is the action that maps any state x_{0} : X to (y_{k+1},x_{k+1}) where (y_{i},x_{i}) ≃ e_{i} x_{i−1} , for i = 1,...,k + 1 (≃ denotes the usual “partial equality”). We also allow letexpressions with pattern matching within a do-construct (with the obvious meaning). We adopt the convention that computations are “strict”, i.e. the result of a computation is undefined if one of its parts is. Furthermore, we use the standard monadic notations

return : Y → M_{X}(Y)  return y x = (y,x)
mapM : (Z → M_{X}(Y)) → Z^{∗} mapM f a⃗ = do{y_{1} ← f a_{1} ; ...
→ M_{X}(Y^{∗})  ... ; y_{k} ← f a_{k}; return (y_{1},...,y_{k})}

as well as

read : X → M_{X→_{fin}Y} (Y), read x m ≃ (m x,m)
add : Y → M_{X→_{fin}Y} (X), add y m ≃ (x,m[x ↦ y]) where x = fresh(m)

Here, fresh is a function with the property that if m : X →_{fin} Y, then fresh(m) ∈ X \ dom(m) ^{13}. With these notations the definitions of P, eval and apply read as follows

P Γ u = return u, if u is a number or a variable
P Γ f[r⃗] = do{a⃗ ← mapM (P Γ) r⃗; return f[a⃗]}
P Γ (r s) = do{(a,b) ← mapM (P Γ) (r,s) ; return (a b)}
P Γ (λx^{A}.r) = do\begin{cases}a ← P Γ[x ↦ A] r; c ← add(Γ;x: A;a) ; \\ return c[dom(Γ)]\} \end{cases}

eval C η n = return n
eval C η x = return (η x)
eval C η f[a⃗] = do{n⃗← mapM (eval C η) a⃗; return [[f]](n⃗)}
eval C η (a b) = do{(v,w) ← mapM(eval C η) (a,b) ; apply C v w}
eval C η c[a⃗] = do{v⃗← mapM (eval C η) a⃗; add (c,v⃗)}
apply C h v = do{(c,w⃗) ← read h; let (y⃗: B⃗;x: A;a) = C c;
eval C [y⃗,x ↦ w⃗,v] a}
apply C n v = ∅

where ∅ is the undefined action, i.e. the partial function with empty domain^{14}.

Lemma 1.1. (1) P Γ r is total and if P Γ r C = (a,C′), then C ⊆ C′.

(2) If eval C η a H = (v,H′), then H ⊆ H′.

(3) If apply C v w H = (v′,H′), then H ⊆ H′.

Proof. Property (1) is direct by induction on the term r. Properties (2) and (3) can be proved by a straightforward simultaneous induction on the definitions of eval and apply, i.e. by “fixed point induction” [21]. ⊓ ⊔

Due to the complexity of C++ it would be a major task, which would require much more man power than was available in our project, to formally prove that our mathematical model, given by eval and apply, coincides with the operational semantics of C++.^{15} (Note that other models of fragments of object-oriented languages in the literature face the same problem and their correctness w.r.t. real languages is therefore usually not shown.) However, when going through the definitions we observe that the evaluation function eval is indeed defined in accordance with the expected behaviour of C++: An integer n is evaluated by itself, and a variable is evaluated by returning its value in the current environment η. The application of a native C++ function to arguments a_{1},...,a_{n} is carried out by first evaluating a_{1},...,a_{n} in sequence, and then applying the function f to those arguments. (a b) corresponds in C++ to the construct (∗ (a))(b). First a and b are evaluated. Because of type correctness, a must be an element of the type of pointers to a class, and the value of a will therefore be an address on the heap. On the heap the information about the class used and the values of the instance variables of that class are stored. Then (∗ (a))(b) is computed by evaluating the body of the method of the class in the environment where the instance variables have the values as stored on the heap, and the abstracted variable has the result of evaluating b. This is what is computed by eval C η (a b) (which makes use of the auxiliary function apply). The expression c[a⃗], which stands for the C++ expression newc(a_{0},...,a_{n}), is evaluated by first computing a_{0},...,a_{n} in sequence. Then new storage on the heap is allocated. Note that in our simplified setting, the constructor of c simply assigns to the instance variables the values of a_{0},...,a_{n}. Consequently, the intended behaviour of C++ is that it stores on the heap the information about the class used and the result of evaluating a_{0},...,a_{n}, which is what is carried out by eval.

13In our applications X will be a space of addresses which we assume to be infinite, i.e.

we assume that the allocation of a new address is always possible.

14It would be more appropriate to let apply C n v result in an error, but, for simplicity, we identify errors with non-termination.

15The formalisation of the semantics of Java in [17] was a major project, and still this book excludes some features of Java like inner classes. Note that C++ is much more complex than Java.

The formal correctness proof for the translated code with respect to our mathematical model of (a fragment of) C++ is based on a Kripke-style logical relation between a C++ value (∈ Val × Heap) and a denotational value (∈ D(A)). The relation is indexed by the class environment C and the type A of the term. The relation

∼_{A}^{C}⊆ (Val × Heap) × D(A),

where A ∈ Type,C ∈ CEnv, is defined by recursion on A as follows:

(v,H) ∼_{int}^{C} n :⟺ v = n
(v,H) ∼_{A→B}^{C} f :⟺ ∀C′⊇ C,∀H′⊇ H,∀(w,d) ∈ Val × D(A) :
(w,H′) ∼_{A}^{C′}d ⟹ apply C′v w H′∼_{B}^{C′}f(d)

Note that the formula apply C′v w H′∼_{B}^{C′}f(d) above states that apply C′v w H′is defined and the result is in relation ∼_{B}^{C′}with f(d). The formula eval C′′η a H′∼_{A}^{C′′} [[r]]ξ in the theorem below is to be understood in a similar way. We also set

(η,H) ∼_{Γ}^{C} ξ:⇔ dom(Γ) ⊆ dom(η) ∩ dom(ξ) ∧ ∀x ∈ dom(Γ)(η(x),H) ∼_{Γ(x)}^{C} ξ(x)

The main result below corresponds to the usual “Fundamental Lemma” or “Adequacy Theorem” for logical relations:

Theorem 1.2. Assume Γ ⊢ r: A, P Γ r C = (a,C′), C′′⊃ C′and ξ: Γ. Then for all (η,H) ∈ VEnv × Heap:

(η,H) ∼_{Γ}^{C′′}ξ ⟹ eval C′′η a H ∼_{A}^{C′′}[[r]]ξ.

Proof. The proof is by induction on the typing judgement Γ ⊢ r: A. In the proof we will use the properties (1) and (2) of Lemma 1.1 as well as the following property of the relation ∼_{A}^{C}, which is clear by definition, and which in the following will be referred to as “monotonicity”:

If (v,H) ∼_{A}^{C}d and H ⊆ H′and C ⊆ C′, then (v,H′) ∼_{A}^{C′}d.

We now consider the four possible cases of how Γ ⊢ r: A can be derived.

Γ,x: A ⊢ x: A. We have P(Γ,x: A) x C = return x C = (x,C). Assume C′⊇ C, ξ : (Γ,x : A) and (η,H) ∼_{Γ,x:A}^{C′} ξ. We need to show eval C′η x H ∼_{A}^{C′}[[x]]ξ. Since eval C′η x H = (η(x),H) and [[x]]ξ = ξ(x) ∈ D(A), and the assumption (η,H) ∼_{Γ,x:A}^{C′}ξ entails (η(x),H) ∼_{A}^{C′}ξ(x), we are done.

Γ ⊢ λx^{A}r: A → B, derived from Γ,x: A ⊢ r: B. P Γ λx^{A}r C = (c[dom(Γ)],C′) where P(Γ,x: A) r C = (a,C_{1}), with C_{1} ⊇ C by (1), c = fresh(C_{1}) and C′= C_{1}[c ↦ (Γ;x : A;a)]) ⊇ C. Assume C′′⊇ C′, ξ : Γ and (η,H) ∼_{Γ}^{C′′}ξ. We need to show eval C′′η c[dom(Γ)] H ∼_{A→B}^{C′′} [[λx^{A}r]]ξ. We have eval C′′η c[dom(Γ)] H = (h,H_{1}) where v⃗= map η dom(Γ) (the usual map function), h = fresh(H) and H_{1} = H[h ↦ (c,v⃗)]). In view of the definition of ∼_{A→B}^{C′′} we assume C′′′⊇ C′′, H′⊇ H_{1} and (w,H′) ∼_{A}^{C′′′}d. We need to show apply C′′′h w H′∼_{B}^{C′′′}[[r]]ξ[x ↦ d]. Clearly, apply C′′′h w H′= eval C′′′η_{1} a H′where η_{1} = [dom(Γ),x ↦ v⃗,w]. Furthermore, (η_{1},H′) ∼_{Γ,x:A}^{C′′′}ξ[x ↦ d], by the assumptions (η,H) ∼_{Γ}^{C′′}ξ and (w,H′) ∼_{A}^{C′′′}d and monotonicity. Using the induction hypothesis we obtain eval C′′′η_{1} a H′∼_{B}^{C′′′} [[r]]ξ[x ↦ d] since P(Γ,x: A) r C = (a,C_{1}) and C_{1} ⊇ C′′′.

Γ ⊢ r s: B, derived from Γ ⊢ r: A → B and Γ ⊢ s: A. By (1), P Γ r C = (a,C_{1}) with C ⊆ C_{1} and P Γ s C_{1} = (b,C_{2}) with C_{1} ⊆ C_{2}. Therefore, P Γ (r s) C = (a b,C_{2}). Assume C′⊇ C_{2}, ξ: Γ and (η,H) ∼_{Γ}^{C′}ξ. We need to show eval C′η (a b) H ∼_{A}^{C′}[[r s]]ξ. By induction hypothesis and (2), eval C′η a H = (v,H_{1}) for some H_{1} ⊇ H with (v,H_{1}) ∼_{A→B}^{C′} [[r]]ξ and, using monotonicity, eval C′η a H_{1} = (w,H_{2}) for some H_{2} ⊇ H_{1} with (w,H_{2}) ∼_{A}^{C′}[[s]]ξ. Hence, apply C′v w H_{2} ∼_{B}^{C′}[[r]]ξ([[s]]ξ) and we are done, since eval C′η (a b) H = apply C′v w H_{2} and [[r s]]ξ = [[r]]ξ([[s]]ξ).

Γ ⊢ f[r_{1},...,r_{k}] : int, derived from Γ ⊢ r_{i} : int, i = 1,...,k. By (1), P Γ r_{1} C = (a_{1},C_{1}) with C ⊆ C_{1} and P Γ s C_{i+1} = (a_{i+1} ,C_{i+1} ) with C_{i} ⊆ C_{i+1} , i = 1,...,k− 1. Hence, P Γ f[r⃗] C = (f[a⃗],C_{k}). Assume C′⊇ C_{k}, ξ : Γ and (η,H) ∼_{Γ}^{C′}ξ. We need to show eval C′η f[r⃗] H ∼_{int}^{C′} [[f[r⃗]]]ξ. By induction hypothesis and (2), eval C′η a_{1} H = (n_{1},H_{1}) for some n_{1} ∈ Z and H_{1} ⊇ H with (n_{1},H_{1}) ∼_{int}^{C′} [[r_{1}]]ξ, i.e. n_{1} = [[r_{1}]]ξ. Similarly, using monotonicity and (2), for i = 1,...,k −1 we have eval C′η a_{i+1} H_{i} = (n_{i+1} ,H_{i+1} ) for some n_{i+1} ∈ Z and H_{i+1} ⊇ H_{i} with n_{i+1} = [[r_{i+1} ]]ξ. It follows eval C′η f[r⃗] H = ([[f]][n⃗],H_{k}) = ([[f[r⃗]]]ξ,H_{k}). ⊓ ⊔

Corollary 1.3 (Correctness of the implementation). Assume ⊢ r : int and let C ∈ CEnv. Then P ∅ r C = (a,C′) for some C′⊇ C. Furthermore, for any heap H, any environment η and any C′′⊇ C′we have

eval C′′η a H = (n,H′)

where n is the value of r and H′is some extension of H.

Remark. The proof of Theorem 1.2 is rather “low level” since it mentions and manipulates the class environment and the heap explicitely. It would be desirable, in particular with regard to a formalisation in a proof assistant, to lift the proof to the same abstract monadic level at which the functions P, eval and apply are defined. A framework for carrying this out might be provided by suitable versions of Moggi’s Computational λ–Calculus, Pitts’ Evaluation Logic [11] and special logical relations for monads [2].

1.4 LAZY EVALUATION IN C++

Haskell is famous for its programming techniques using infinite lists. A wellknown example are the Fibonacci numbers, which are computed efficiently by using the following code:

fib = 1:1:(zipWith (+) fib (tail fib))

This example requires that we have infinite streams of natural numbers, and relies heavily on lazy evaluation. We show how to translate this code into efficient C++ code, by using lazy evaluation. The full code for the following example, in which we have translated λ-types and -terms into original C++, is available from [16].

The standard technique for replacing call-by-value by call-by-name is to delay evaluation by replacing types A by () → A where () is the empty type (i.e. void). However, according to the slogan “lazy evaluation = call-by-name+sharing” (which we learnt from G. Hutton [3]) lazy evaluation means more than delaying evaluation: it means as well that a term is evaluated only once. In order to obtain this, we define a new type Lazy(A). This type delays evaluation of an element of type A in such a way that, if needed, the evaluation is carried out – however, only once. Once the value is computed, the result is stored in a variable for later reuse. Note that this is a general definition, which is not restricted to lazy streams.The definition is as follows (we use the extended C++ syntax for λ-terms and -types introduced in Sect. 1.2, esp. r^^t for application, \ for λ, and –> for →):

template<typename X> class lazy{
  bool is_evaluated;
  union {X        result;
          () -> X compute_function;};
public:
  lazy(()-> X compute_function){
     is_evaluated = false;
     this->compute_function = compute_function;};
  X eval(){
     if (not is_evaluated){

              result = compute_function ^^();
              is_evaluated = true;};
     return result;};};
#define Lazy(X) lazy<X>*

Note that without support by the extended syntax the code above would be much longer and considerably more complicated.

Using the class lazy we can now easily define lazy streams of natural numbers (lazy lists, i.e. possibly terminating streams, can be defined similarly, but require the usual technique based on the composite design pattern for formalising algebraic data types as classes by introducing a main class for the main type which has subclasses for each constructor, each of which stores the arguments of the constructor)

template<typename X>class lazy_stream{
   public: Lazy(X) head;
             Lazy(lazy_stream<X>*) tail;
             ... Constructor as usual ... }
#define Lazy_Stream(X) lazy_stream<X>*

We define an operation which takes a function of type () → X and returns the corresponding element of type Lazy(X):

template<typename X> Lazy(X) create_lazy
      (()-> X compute_function){
                     return new lazy<X>(compute_function);};

In order to deal with the example of the Fibonacci numbers, one needs to define the operators used in the above mentioned definition of fib:

• lazy_cons_lazy<X> computes the cons-operation on streams and returns lazily a lazy stream:

   template<typename X>Lazy(Lazy_Stream(X)) lazy_cons_lazy
                (Lazy(X) head,
                 Lazy(Lazy_Stream(X)) tail){
     return create_lazy
                    (\ () x.new lazy_stream<X>(head,tail))};};

• lazy_tail<X> computes the tail of a stream lazily (we define here only its type):

   Lazy(Lazy_Stream(X)) lazy_tail<X>
                           (Lazy(Lazy_Stream(X)) s)

• lazy_zip_with<X> computes the usual zip with function (i.e.

zip with(f,[a,b,..],[c,d,..]) = [f a c,f b d,...]; we define here only its type):

   Lazy(Lazy_Stream(X)) lazy_zip_with<X>
      (X -> X -> X f,
        Lazy(Lazy_Stream(X)) s0,
        Lazy(Lazy_Stream(X)) s1)

The definition of lazy tail and lazy zip with is straightforward, once one has introduced a few combinators for dealing with Lazy(X).

Now we can define the stream of Fibonacci numbers as follows (plus is λx,y.x + y, one_lazy is the numeral 1 converted into an element of Lazy(int), create_lazy transforms elements of type ()->A into Lazy(A), and eval evaluates an element of type Lazy(A) to an element of type A):

()-><Lazy_Stream(int)> fib_aux =
 \() x. Lazy_Stream(int)
         eval(
          lazy_cons_lazy(
             one_lazy,
             lazy_cons_lazy(
               one_lazy,
               lazy_zip_with(
                 plus,
                 create_lazy(this),
                 lazy_tail(create_lazy(this))))));
Lazy_Stream(int) fib = eval(create_lazy(fib_aux))

Note that here we were using the keyword this in the definition of fib_aux. This is how a recursive call should be written. If we instead put fib_aux here, C++ will, when instantiating fib_aux, first instantiate fib_aux as an empty class, and then use this value when evaluating the right hand side. Only when using this we obtain a truely recursive definition.

When evaluated, one sees that the nth element of fib computes to fib(n) and this computation is the efficient one in which previous calls of fib(k) are memoized. Replacing Lazy(X) by () –> X, results in an implementation of the Fibonacci numbers which is still correct, but requires exponential space since memoization is lost (on our laptop we were not able to compute fib(25)).

Generalization. The above technique can easily be generalized to arbitrary algebraic types, in fact to all class structures available in C++. If, for example, one replaces in a tree structure all types by lazy types, then only a trunk of the tree structure is evaluated and kept in memory, namely the trunk which has been used already by any function accessing this structure.

1.5 CONCLUSION

In this paper we have shown how to introduce functional concepts into C++ in a provably correct way. The modelling and the correctness proof used monadic concepts as well as logical relations. We also have shown how to integrate lazy evaluation and infinite structures into C++.

This work lends itself to a number of extensions, for example, the integration of recursive higher-order functions, polymorphic and dependent type systems as well as the combination of larger parts of C++ with the λ-calculus. The accurate description of these extensions would require more sophisticated, e.g. domaintheoretic constructions and a more systematic mathematical modelling of C++. It would be as well be interesting to expand our fragment of C++ in order to deal with side effects. This would allow for instance to prove that our lazy construct actually gives rise to an efficient implementation of the Fibonacci function.

We believe that if our approach is extended to cover full C++, we obtain a language in which the worlds of functional and object-oriented programming are merged, and that we will see many examples, where the combination of both language concepts (e.g. the use of λ-terms with side-effects) will result in interesting new programming techniques.

REFERENCES

[1] H. Abelson, G. J. Sussman, and J. Sussman. Structure and interpretation of computer programs. MIT Press, 1985.

[2] J. Goubault-Larrecq, S. Lasota, and D. Nowak. Logical relations for monadic types. In Julian C. Bradfield, editor, Proceedings of the 16th International Workshop on Computer Science Logic (CSL’02), volume 2471 of Lecture Notes in Computer Science, pages 553–568, Edinburgh, Scotland, UK, September 2002. Springer.

[3] G. Hutton. Programming in Haskell. Cambridge University Press, Cambridge, UK, 2006.

[4] Atshushi Igarashi, Benjamin Pierce, and Philip Wadler. Featherweight Java: A minimal core calculus for Java and GJ. In Loren Meissner, editor, Proceedings of the 1999 ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages & Applications (OOPSLA‘99), volume 34(10), pages 132–146, N. Y., 1999.

[5] A. Jung and J. Tiuryn. A new characterization of lambda definability. In M. Bezem and J. F. Groote, editors, Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science, pages 245–257. Springer, 1993.

[6] R. M. Keller. The Polya C++ Library. Version 2.0. Available via

http://www.cs.hmc.edu/∼keller/Polya/, 1997.

[7] O. Kiselyov. Functional style in C++: Closures, late binding, and lambda abstractions. In ICFP ’98: Proceedings of the third ACM SIGPLAN International conference on Functional programming, page 337, New York, NY, USA, 1998. ACM Press.

[8] K. Läufer. A framework for higher-order functions in C++. In COOTS, 1995.

[9] B. McNamara and Y. Smaragdakis. Functional programming in C++. In ICFP ’00: Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, pages 118–129, New York, NY, USA, 2000. ACM Press.

[10] E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.

[11] A. M. Pitts. Evaluation logic. In G. Birtwistle, editor, IVth Higher Order Workshop, Banff 1990, Workshops in Computing, pages 162–189. Springer, 1991.

[12] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[13] G. D. Plotkin. Lambda definability in the full type hierarchy. In R. Hindley and J. Seldin, editors, To H.B. Curry: Essays in Combinatory Logic, lambda calculus and Formalisms, pages 363 – 373. Academic Press, 1980.

[14] J. C. Reynolds. Types, abstraction and parametric polymorphism. In IFIP’83, pages 513–523. North-Holland, 1983.

[15] S. Schupp. Lazy lists in C++. SIGPLAN Not., 35(6):47–54, 2000.

[16] A. Setzer. Lazy evaluation in C++. http://www.cs.swan.ac.uk/

∼csetzer/articles/additionalMaterial/
lazyEvaluationCplusplus.cpp, 2006.

[17] R. Stärk, J. Schmid, and E. Börger. Java and the Java Virtual Machine – Definition, Verification, Validation. Springer, 2001.

[18] R. Statman. Logical relations and the typed lambda-calculus. Information and Control, 65:85 – 97, 1985.

[19] J. Striegnitz. FACT! – the functional side of C++.

http://www.fz-juelich.de/zam/FACT .

[20] W. W. Tait. Intensional interpretation of functionals of finite type. Journal of Symbolic Logic, 32:198 – 212, 1967.

[21] G. Winskel. The formal semantics of programming languages: an introduction. MIT Press, Cambridge, MA, USA, 1993.