comprehension types

[Mark Tarver]

Again pillaging Turner; he includes what he calls the Axiom of Comprehension.
His formulation is:

COMP: z is a member of {x:f} <-> f[z/x]

It means that for any function f that returns a boolean we can construct a type
of all those objects for which f returns the value true. f is a characterising
function for that type.  COMP is the analogue of Frege's axiom V.

In programming terms a comprehension type is a type characterised by any lambda function that returns a boolean.  Let's see this in Shen.

(datatype comprehension

let Y (newv)
X : A;
(/. Y Z) : (A --> boolean);
(test! (/. Y Z) X);
________________________
X : (- (comp (/. Y Z)));

F : (A --> boolean);
X : A >> P;
______________________
X : (- (comp F)) >> P;

if (trap-error (eval [F X]) (/. E false))
___________________
(- (test! F X));)

What does this say?  The first rule says that X inhabits a comprehension type
if (/. Y Z) : (A --> boolean), X : A, and you can prove that X meets the
test of the characterising function.

The second (left) rule says that if X inhabits a comprehension type then X inhabits the type of the domain of the characterising function.

The last says that we can prove X passes the test of the characterising function by evaluating the application of that function to X.  If the evaluation fails, the
test is not met, but if true is returned, then good.

We can test this.

(34+) (+ 3 4) : (comp (/. X (prime? X)))
7 : (comp (lambda X7663 (prime? X7663)))

(35+) (define f
        {(comp (/. X (prime? X))) --> number}
         X -> (* X 2))
(fn f) : ((comp (lambda X (prime? X))) --> number)

(36+) (f 11)
22 : number

(37+) (f 9)
type error

Mark