(Picking up on Sperber's thread but, from a different perspective.)
One design choice in Scheme concerns required procedures: should they
ever be required to be total and effective over any of the fundamental
types in Scheme? For example, must eqv? always return either #t or #f?
The question is answered, I hope, by asking what a "fundamental type" in
Scheme /is/. I would first claim, uncontroversially I hope, that:
The fundamental types (booleans, numbers, characters, strings, and so
forth) in Scheme form an axiomatically defined proper class equipped
with a natural, albeit uncomputable equivalence relationship. The
required procedure eqv? is a sub-equivalence relationship: it returns #t
only for truly equivalent values but may return #f even for truly
equivalent values. The most obvious evidence of this first claim is
the question of equivalence among procedure objects.
(The "natural" equivalence relationship among Scheme values is
substitutability of terms in an operational model of execution where
"substitutability" can be defined in terms of "observable behaviors"
such as operations on ports.)
Only slightly more controversially, I think, I would also claim that:
/Equivalence is not total and computable over _any_ of the disjoint types./
/*"Proof (by counterexample)":*/ /implicitly forced promises are an
invited extension to the language./
One could similarly prove that the /type/ of an object is not total and
computable. Where the standard currently says something like "always
returns an exact integer" or "always returns a boolean", that should
really be interpreted as something like "never returns a value that is
provably of any type defined as disjoint from [integers | booleans | etc.]".
Big yawn, right? Except that it leaves us in some binds:
Suppose that the Report required eqv? to always return and always return
#t or #f. Then it is absolutely required, as a consequence, that eqv?
sometimes give inaccurate results (false negatives). This is
unacceptable /as a requirement/, certainly, in the absence of a proof
that it is inescapable in some convincing sense.
Suppose that an (execution of an) implementation /knows/ that eqv? has
been called and passed arguments for which it is unable to compute an
accurate answer -- what should it do? Surely, the report contains an
unnecessary restriction if it /prohibits/ the implementation from
returning a value whose semantics allow execution to continue without
committing the implementation to an equivalence decision it is
unprepared to make.
We can generalize that: the report can not require that /any/ primitive
procedure be total and computable. This specifically precludes any
procedure defined to "always" return either #t or #f or to always
return, say, an exact integer (except in the weak sense that "exact
integer" means "a value for which type predicates of types disjoint from
exact integers never return true").
None of these statements change, at all, the reliably deterministic
behavior of non-divergent Scheme programs. What is changed, if we
admit that /none/ of the primitive procedures can be given a total,
computable specification, is what one can /prove/ about Scheme programs
and how programs with no portably deterministic behavior behave.
Useful proofs, in this interpretation of Scheme's types, can only prove
relations between "nominal" input and output values -- proving effective
totality over any reasonable class of fundamental Scheme types is
definitionally ruled out. And, so what: it isn't the least charm of a
portable program when one discovers it has a serendipitous yet well
defined and completely explicable use when applied over unanticipated
members of the classes of values it refers to.
Lisp is, in some sense, the ultimate pursuit of parsimony in programming
-- it aims to be the language in which anything that only needs to be
said once can be said, in fact, exactly once. That is why it is
defined as a (family of) languages in which all types are proper classes
and all run-time values dynamically typed -- programs are procedures
over /proper classes/ as such. Scheme is, in some sense, a persistent
attempt to express that essence of lisp simultaneously precisely and
pragmatically, without /much/ commitment to compatibility with historic
lisps (a commitment to preserve only arbitrary choices such as
s-expression syntax).
And so:
The report should not assert that #f is the only false value.
Eqv? should be permitted to return an unspecified value.
The result of any Scheme computation that is strict in some unspecified
value should be unspecified.
If an implementation reifies unspecified values as such, it must not
execute the program in any way that is strict with respect to the
unspecified properties of the value. For example, (write (if
(unspecified) 'a 'b))) should be an error while (write (begin (if
(unspecified) 'a 'b) 'c))) should be permitted to print c.
-t
(Separately argued and on additional basis, but also supported here:
char->integer should not be total.)
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
http://lists.r6rs.org/pipermail/r6rs-discuss/attachments/20070128/50ffec73/attachment.htm
Received on Sun Jan 28 2007 - 05:58:30 UTC