This chapter will present example applications of the most interesting components of our framework. Most examples were tried under the Teyjus toplevel, but they could be easily executed from within a main module, as is also contained in the distribution. The example program will always be bound by existential quantification so as to prevent the toplevel from printing it in the solution part. The application of the predicate of interest follows this definition immediately, then the system output is given. Each example will be explained in detail.
According to the typing rules in chapter 2, our framework allows type inference for a large class of programs, unfortunately not (yet) completely for recursive types. It also contains functionality for type checking polymorphic programs. Here is an example of mixed type inference / type checking of a polymorphically typed program:
sigma Program\
Program =
tlet
(all (a\ in (a –> a))) (tabs (a\ tlam a (y\ y)))
(f\ pair (app f (pair u u)) (app f u)),
infer_tp Program TP.
The answer substitution:
TP = (unit ** unit) ** unit
|
As can be seen in the last line of code, the function f is applied
twice: once to a pair of unit values, then to only the unit value. This
is an example of so-called let-polymorphism, which the system can handle
due to a few small extensions presented in [].
This demonstrates the application of the rules of the structural operational semantics as given on page ??.
sigma Program\ Program = snd (pair u (lam (x\ snd (pair u u)))), eval Program Result. The answer substitution: Result = lam (x\ snd (pair u u)) |
As we can see clearly, normal evaluation is not capable of simplifying all
parts of the program: the body of the resulting lambda abstraction could
obviously be improved (reduction of the application of the pair accessor
snd), but the eval-predicate cannot step into the body of
functions: this is the application domain of the partial evaluator.
Taking the same example as before for the evaluation rule, we see that partial evaluation can achieve more:
sigma Program\ Program = snd (pair u (lam (x\ snd (pair u u)))), part_eval Program Result. The answer substitution: Result = lam (W1\ u) |
Due to the importance of the partial evaluator in this project, we will give a thorough overview of its capabilities.
sigma Program\ Program = lam (x\ pair (fst x) (snd x)), part_eval Program Result. The answer substitution: Result = lam (W1\ W1) |
As can be seen, the program above destructs a pair into its components
using the fst and snd accessors and rebuilds it again
with the pair constructor. This is redundant and will always be
eliminated. Of course, this works in much more complex examples, too,
where some resulting datastructure may contain parts which are for some
reason reconstructed in this way. The rule is safe, because the accessors
always get values only as is ensured by the monad: effect behaviour will
remain identical.
We will not give any example for this, because this trivial simplification
was already demonstrated in earlier ones. When given a pair at binding
time, fst and snd will immediately reduce it. So will
rep_rtp when given an abstracted value of recursive type.
Values of sum type constructed by inl and inr cannot be
simplified by themselves, but case statements can — even in many
ways! It is trivial that a case statement will be simplified if the
outermost constructor of the condition (of sum type) is known. This will
reduce the whole case statement to the appropriate case arm. There are,
however, two further simplifications:
sigma Program\
Program =
lam (x\
case x
(l\ inr l)
(r\ inr r)),
part_eval Program Result.
The answer substitution:
Result =
lam (W1\ let_comp (case W1 (W2\ inr W2)
(W2\ W1))
(W2\ W2))
|
The result, in which the terminating computation of the case statement
could be inlined now (see further below in this chapter), shows that the
second case arm has been changed — but why? The answer is similar to
redundant pair-reconstruction: the condition is destructed during the
choice of the case arm, only the parameter of its constructor will be
bound within the case arm. But inr reconstructs it again! Such
reconstructions are spotted by the partial evaluator: the condition will
be substituted for all occurances of inl l in the first case arm
and all occurances of inr r in the second case arm. Changing the
above program only slightly (actually: a single letter) shows us the
third simplification rule for case statements:
sigma Program\
Program =
lam (x\
case x
(l\ inl l)
(r\ inr r)),
part_eval Program Result.
The answer substitution:
Result = lam (W1\ W1)
|
This may be surprising at first, but is easily understandable: first the partial evaluator discovers that the condition is reconstructed in both case arms. Then it applies its third rule: when two case arms are structurally equivalent, the whole case statement can be eliminated, simply because its result does not depend on the condition of the case statement! This allows it to reduce the example to the identity function. Note again that the condition of the case statement is always a value, which is guaranteed by the monad. Therefore, all these rules are sound: equivalent values can always be substituted for each other without changing the meaning of the program including effect behaviour (this is called referential transparency).
In some cases the partial evaluator can detect that a recursive function is guaranteed to terminate. This happens when evaluation will never reach a recursive call. Here is an example:
sigma Program\
Program =
app (
lam (x\
rec (f\ y\
case x
(l\ l)
(r\ app f y))))
(inl u),
part_eval Program Result.
The answer substitution:
Result = lam (W1\ u)
|
The partial evaluator sees that the application of the lambda abstraction
in this example is possible, which causes x to be substituted
in the body of the recursive function. This again allows the partial
evaluator to simplify the case statement, which removes the recursive
call that is in the eliminated second arm. Finally, it turns out that
the recursion variable f is not used any more in the body of the
recursive function. Therefore it is safe to rewrite the recursive function
to a normal lambda abstraction. This might allow application of this
resulting function to another value immediately (e.g. when this result
is used as a higher-order function in an argument to another function).
We will not give any examples for this rule since it has been used
in previous examples already. The only cases when we can reduce a
function application happen when the function is a lambda abstraction
(guaranteed to terminate) or if it is recursive and some external
termination analyser, which can be “plugged” into the system, proves
its termination. This guarantees that the partial evaluator always
terminates and that its power only depends on the crucial predicate
funcall_terminates, which has been described in our chapter on
implementation.
We consider the following example:
sigma Program\
Program =
lam (x\
pair
(fst x)
(lam (y\ fst x))),
part_eval Program Result1.
The answer substitution:
Result1 =
lam (W1\
let_comp
(fst W1)
(W2\ pair W2
(lam (W3\ let_comp (fst W1)
(W4\ W4)))))
|
The output is somewhat longer, but it should still be possible to see that
the pattern “let_comp (fst W1) ...” appears twice. Although
the second occurance happens to be in a deeper lambda abstraction
where it is not guaranteed to be called if the outermost function is
applied, it does not hurt (and maybe help) to eliminate this duplicated
computation using the corresponding module for this (see appendix
B). When applied to the result of the last example
(elim_cse Result1 Result2), the output will be:
The answer substitution:
Result2 =
lam (W1\
let_comp (fst W1)
(W2\ pair W2 (lam (W3\ W2))))
|
As can be seen, the redundant computation has been eliminated. This is always safe, because this operates on lifted computations without side effects only.
This feature, implemented in module “let_ext”, makes it possible to inline terminating lifted computations again if this does not duplicate them in a nonlinear way (each case arm is considered separately). This would rule out the last example, but improve the one presented in the section on case statements. This program:
lam (W1\ let_comp (case W1 (W2\ inr W2)
(W2\ W1))
(W2\ W2))
|
could then be changed to:
lam (W1\ case W1 (W2\ inr W2) (W2\ W1)) |