Delaying evaluation

One form of delayed evaluation which we have already seen is conditional evaluation. In an if .. then .. else .. expression only two of the three sub-expressions are evaluated. The boolean expression will always be evaluated and then, depending on the outcome, one of the other sub-expressions will be evaluated. The effect of a conditional expression would be different if all three of the sub-expressions were always evaluated. This explains why there is no cond function [of type (bool * 'a * 'a) -> 'a] in Standard ML.

Similarly, a recursive computation sometimes depends upon the outcome of evaluating a boolean expression [as with the takewhile function [*]]. In cases such as these, the evaluation of expressions can be delayed by placing them in the body of a function. By packaging up expressions in this way, we can program in a `non-strict' way in Standard ML and we can describe recursive computations and we can define infinite objects such as the list of all natural numbers or the list of all primes. Consider the following function.

fun FIX f x = f (FIX f) x;


What is the type of FIX?

The purpose of the FIX function is to compute fixed points of other functions. [Meaning: x is a fixed point of the function f if f (x) = x.] How is this function used? Consider the facbody function below. No derived forms are used here in order to make explicit that this is not a recursive function [not a val rec .. ].

val facbody = fn f => fn 0 => 1
                       | x => x * f (x - 1);

If this function were to be given the factorial function as the argument f then it would produce a function as a result which was indistinguishable from the factorial function. That is, the following equivalence would hold.

fac = facbody(fac)
But this is just the equivalence we would expect to hold for a fixed point. What would then be the result if we defined the fac function as shown below.

val fac = FIX (facbody);

The fac function will then compute the factorials of the integers which it is given as its argument. Notice that neither the declaration of fac nor the declaration of facbody were recursive declarations; of the three functions which were used only FIX is a recursive function.

This effect is not specific to computing factorials, it would work with any recursive function. The functions below use FIX to define the usual map function for lists.

val mapbody = fn m => fn f => 
    fn [] => [] | h::t => f h :: m f t;

fun map f l = (FIX mapbody) f l;

This method of defining functions succeeds because the FIX function delays a part of the computation. In its definition the parenthesised sub-expression FIX f which appears on the right-hand side is an unevaluated function term [sometimes called a suspension] equivalent to fn x => FIX f x. Crucially, this is the role of x in the definition; to delay evaluation. Without it the function would compute forever.

(* Always diverges when used *)

fun FIX' f = f (FIX' f);


What is the type of FIX'?

This version of the function makes it much easier to see that the fixed point equation is satisfied--that f (FIX' f) = FIX' f--and in a lazy variant of the Standard ML language the FIX' function would be perfectly acceptable and would operate just as FIX does.