Tiny Ollibot Example Server - Call-by-need functions

Solution for combining parallel evaluation and exceptions

Robert J. Simmons, Frank Pfenning

These examples are derived from Figures 5 and 10 in Substructural Operational Semantics as Ordered Logic Programming.

In par-exn1.olf, we describe an issue with the parallel evaluation of pairs combined with exceptions. In this example, we modify the computation frames to allow exceptions to deal generically with suspended parallel computations.

Parallel evaluation for pairs (Figure 5), plus unit

Now the suspended computation created by pair evaluation is marked as a comp2, to distinguish it from a comp waiting on only one return.

eunit : eval(unit) ->> return(unit).

epair1 : eval(pair E1 E2) ->> comp2(pair1) • eval(E1) • eval(E2).
epair2 : comp2(pair1) • return(V1) • return(V2) ->> return(pair V1 V2).

elet1 : eval(split E (λx1.λx2. E' x1 x2)) ->> comp(split1 E') • eval(E).
elet2 : eval(split1 (λx1.λx2. E' x1 x2)) • return(pair V1 V2) ->> eval(E' V1 V2).

Exceptions (Figure 10), including exceptions for comp2 frames

Because we have generically defined a suspended computation, we can generically define what to do if the left branch, the right branch, or both branches generate failure.

The alternative semantics that raises an exception if one branch raises an exception and the other fails to terminate is not natural to encode in this setting; the natural setting for such a thing would seem to be either linear destination-passing with affine resources or some alternate logic that can correctly deal with having a single atomic resource to the left of two ordered contexts.

etry   : eval(try E1 E2) ->> catch(E2) • eval(E1).
eraise : eval(raise) ->> fail.
ecatch : catch(E2) • fail ->> eval(E2).
eret   : catch(E2) • return(V) ->> return(V).

epop   : comp(F) • fail ->> fail.
epop1  : comp2(F) • fail • return(V) ->> fail.
epop2  : comp2(F) • return(V) • fail ->> fail.
epop3  : comp2(F) • fail • fail ->> fail.

The troublesome examples from before now correctly evaluate to unit.

%trace * eval(try (pair raise (pair unit unit)) unit).
eval(try (pair raise (pair unit unit)) unit)
catch(unit)eval(pair raise (pair unit unit))
catch(unit)comp2(pair1)eval(raise)eval(pair unit unit)
catch(unit)comp2(pair1)faileval(pair unit unit)
catch(unit)comp2(pair1)failcomp2(pair1)eval(unit)eval(unit)
catch(unit)comp2(pair1)failcomp2(pair1)return(unit)eval(unit)
catch(unit)comp2(pair1)failcomp2(pair1)return(unit)return(unit)
catch(unit)comp2(pair1)failreturn(pair unit unit)
catch(unit)fail
eval(unit)
return(unit)
%trace * eval(try (pair (pair unit unit) raise) unit).
eval(try (pair (pair unit unit) raise) unit)
catch(unit)eval(pair (pair unit unit) raise)
catch(unit)comp2(pair1)eval(pair unit unit)eval(raise)
catch(unit)comp2(pair1)comp2(pair1)eval(unit)eval(unit)eval(raise)
catch(unit)comp2(pair1)comp2(pair1)return(unit)eval(unit)eval(raise)
catch(unit)comp2(pair1)comp2(pair1)return(unit)return(unit)eval(raise)
catch(unit)comp2(pair1)return(pair unit unit)eval(raise)
catch(unit)comp2(pair1)return(pair unit unit)fail
catch(unit)fail
eval(unit)
return(unit)
%trace * eval(try (pair (pair raise unit) (pair unit raise)) unit).
eval(try (pair (pair raise unit) (pair unit raise)) unit)
catch(unit)eval(pair (pair raise unit) (pair unit raise))
catch(unit)comp2(pair1)eval(pair raise unit)eval(pair unit raise)
catch(unit)comp2(pair1)comp2(pair1)eval(raise)eval(unit)eval(pair unit raise)
catch(unit)comp2(pair1)comp2(pair1)faileval(unit)eval(pair unit raise)
catch(unit)comp2(pair1)comp2(pair1)failreturn(unit)eval(pair unit raise)
catch(unit)comp2(pair1)faileval(pair unit raise)
catch(unit)comp2(pair1)failcomp2(pair1)eval(unit)eval(raise)
catch(unit)comp2(pair1)failcomp2(pair1)return(unit)eval(raise)
catch(unit)comp2(pair1)failcomp2(pair1)return(unit)fail
catch(unit)comp2(pair1)failfail
catch(unit)fail
eval(unit)
return(unit)