10.2.4 The Type of All Sets
set is a type operator that applies to any list without duplicated elements. This code again uses some
advanced material from TBoS.
(1+) (datatype set
_____________
[] : (set A);
X : A; Y : ((set A) & (without X));
===================================
[X | Y] : (mode (set A) -);
X : (set A);
_____________
X : (list A);
X : P; X : Q;
====================
X : (mode (P & Q) -);
________________
[] : (without X);
if (not (= X Z))
Y : (without Z);
______________________
[X | Y] : (without Z);
______________________________________________
(not (element? X Y)) : verified >> Y : (without X);)
type#set : symbol |
We can show this works and define set union.
(2+) [1 2 3] : (set number)
[1 2 3] : (set number)
(3+) [1 2 3 1] : (set number)
type error
(4+) (define un
{(set A) --> (set A) --> (set A)}
[] S -> S
[X | Y] S -> [X | (un Y S)] where (not (element? X (un Y S)))
[_ | Y] S -> (un Y S))
(fn un) : ((set A) --> ((set A) --> (set A))) |
|
