Negative Types

10.2.2 Negative Types

This requires advanced features discussed in TBoS. Something belongs to the type (not number) if it cannot be proved to be of the type number.

(datatype not

   X : A; !; fail!;
   _____________________
   X : (mode (not A) -);   
   
   _____________________
   X : (mode (not A) -);)
  
type#my-prover-types

f : (not number)
f : (not number)

f : (not symbol)
type error

[4 r] : (list (not string))
[4 r] : (list (not string)) 

4. The Core Language

4.6 Sequences

5 Defining Functions

6. Packages

7. Shen-YACC

8. Shen Prolog

9. Types

10 Sequent Calculus

10.2 Exotic Types