10.2.3 Subtypes
TBoS p.269-272
A is a subtype of B if every inhabitant of A is an inhabitant of B. Here we define subtype and
also the type int of all integers. We declare that int is a subtype of number, that anything that passes
the integer? test is an int and that +, - and * can be used to construct ints. We can now verify the type
of +int.
(1+) (datatype subtype
(subtype A B); X : A;
_____________________
X : B;)
type#subtype : symbol
(2+) (datatype int
if (integer? N)
________________
N : int;
____________________
(subtype int number);
if (element? F [+ - *])
__________________________
F : (int --> int --> int);)
type#int : symbol
(3+) (define +int
{int --> number --> number}
M N -> (+ M N))
+int : (int --> (number --> number))
|
|
