New type specifier?

[Kent M Pitman <KMP@SCRC-STONY-BROOK.ARPA>]

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:
 (DEFUN FOO (X)
   (IF X (VALUES T 3) (VALUES NIL (THE VOID NIL))))
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:
 (DEFUN BAR (X)
   (DECLARE (SPECIAL *FOO*))
   (MULTIPLE-VALUE-BIND (A B)
       (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:
 (DEFUN BAR (X)
   (MULTIPLE-VALUE-BIND (A B)
       (FOO X)
     (PRINT B)
     A))
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:
 (DEFUN BAZ (X &AUX BAR-OUTPUT-IS-VALID)
   (LET ((BAR-OUTPUT-AS-A-STRING
           (WITH-OUTPUT-TO-STRING (*STANDARD-OUTPUT*)
             (SETQ BAR-OUTPUT-IS-VALID (BAR X)))))
     (IF BAR-OUTPUT-IS-VALID 
         BAR-OUTPUT-AS-A-STRING
         NIL)))
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.