[Prev][Next][Index][Thread]
conditionals
The treatment of conditionals seems much less ad-hoc if presented in the
context of a more general language such as the programming language underlying
the NuPRL type theory. If we regard bool as 1+1, then the case analysis form,
which has the general shape
Case e x.e' y.e''
is "automatically" strict only in the first position since the second and
third positions are unsaturated terms, and hence cannot sensibly be evaluated.
(For those unfamiliar, this form is evaluated as follows: evaluate e; the
result must be either Inl(u) or Inr(v); in the former case, evaluate [u/x]e';
in the latter evaluate [v/y]e''. Of course, both u and v are *, the sole
element of type 1. In the general case the arguments carry information.)
In addition to the disjoint union type, in Martin-Lof's type theory there are
also the finite types, one of which is N2=bool. There the non-strictness of
the non-principal positions is essentially "by decree": the evaluation rule
for these forms specifies that only one non-principal argument is evaluated,
according to the value of the principal argument. (I'm doing this from
memory, I hope this is right.)
This brings up a related point: just what is meant by "call-by-value"? If we
use the uniform notation of type theory, we see that there are two possible
senses of this word. In one sense we can understand the CBV/CBN distinction
to be a property of the evaluation rule for the application form --- do we or
do we not evaluate the argument position of App(Fn,Arg) before continuing with
the evaluation of the body of the value of Fn, which must be a lambda. In
another sense we can regard it as applying to all combining forms, so that,
for example, in the finite types discriminator form, all positions would be
evaluated under the generalized interpretation of CBV.
Under the narrow interpretation, we do not get into questions like "should or
should not cons evaluate its arguments" since cons would be a combining form,
not an application of a constant. But even under the more general
interpretation, the case analysis form would be unproblematic since its
non-principal arguments are unsaturated, and hence could only evaluate to
themselves.
Thus:
1. The "unnaturality" in the pre-cpo case for conditionals isn't all that
unnatural.
2. There is some ambiguity in what is meant by "call-by-value" that has lead
to some confusion in the literature.
Bob