[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

New type specifier?

Unfortunately, even if you had a VOID type specifier, it would not be
reasonable for the compiler to warn about uses of VOID items. It is only
a semantic error if you rely on the particular value that returns, not
if you use a value that happens to come back. For example, consider:
As I understand it, you're suggesting that this would declare that the
data-flow from the alternative branch of the IF to have a void second value.
The problem is that a program such as:
       (FOO X)
     (SETQ *FOO* (CONS A B))
     (IF (CAR *FOO*) (CDR *FOO*) NIL)))
is using B legitimately because it is never accessing the second value unless
the first value is true. The problem is that whether a value is "used" is relative,
not absolute. Consider even the program:
       (FOO X)
     (PRINT B)
Surely, you might say, if anything "uses" B, this does. But what if I tell you
now that BAR is not exported and is called internally only from BAZ, which is
defined by:
             (SETQ BAR-OUTPUT-IS-VALID (BAR X)))))
The effect of having used the void value has been contained and is in the global
context cannot be said to have been used. I claim the output of the function BAZ
is meaningful in all situations. In the final analysis, I think the kind of error 
you seek to detect is inherently undetectable for fairly deep-seated philosophical
reasons. I would be amazingly irrated if compilers became pretentious enough to
claim that understood my intent in a situation like this, since I think it's 
probably possible to construct a proof that they cannot.

Your VOID specifier does have the slight advantage that it provides useful
self-documentation from me to myself about my intent in the program. It might 
even prove useful to programs -writing- programs. It's just that in the general
case of reading programs, it's of little or no use in proving that a program 
is incorrect because of issues related to this idea of the global vs local 
relevance of a computation.