Qi and the "Magic" Prime Type
The Qi type system allows for some very interesting types not typicallyavailable to non-FOL type systems. To better understand what you can do
with this system, I have made a simple and naive prime type to show off
the power of the Qi types. The idea behind it seems very simple, namely
we make a number subtype that matches only primes. Then, we can define
functions that take only prime numbers and we can be certain that only
prime numbers can get into this function.
To begin this process, we need to have a function that determines
primes. Taking the very simple approach to generating primes used in
the book, we create a prime? function with the following definition.
(define prime?
{ number --> boolean }
X -> (prime*? X (round (sqrt X)) 2))
(define prime*?
{ number --> number --> number --> boolean }
X Max Div -> true where (> Div Max)
X Max Div -> false where (integer? (/ X Div))
X Max Div -> (prime*? X Max (+ 1 Div))
)
Next, we need to have a type function that tells the compiler that our
prime type is a subtype of numbers. Anyplace we can use a number, ie in
+ or any other math function, we want to be able to use primes. The Qi
Language book describes this type and we will use the pattern described
in the book. As an aside, this ends up being so useful that future
versions of Qi may just need to include this type natively.
(datatype subtype
(subtype B A); X : B;
_____________________
X : A;
_____________________
(subtype prime number);
)
Finally, we now can make our prime type by using the following
definition. Note that this definition is incomplete and try to
understand why it does not allow us to define a function that takes a
number and returns a prime. However, this function should allow us to
find primes at the top level (and hence in loaded files as well). We
will expand on the definition below. Basically, the function should say
that if we have a number and it passes the prime? function, then we
should consider it a prime.
(datatype prime
if(and (number? X) (prime? X))
_________
X : prime;
)
Now that we have an incomplete definition, let us see it in use.
(2+) 3 : prime
3 : prime
(3+) 4 : prime
error: type error
(4+) 5 : prime
5 : prime
(5+) 6 : prime
error: type error
(6+) 8 : prime
error: type error
(7+) 9 : prime
error: type error
(8+) 11 : prime
11 : prime
(9+) 13 : prime
13 : prime
That's a smart type! *grin*
To understand why this function does not complete our definition of
prime, we should try to build a function that takes in a prime and
finds the next prime on the number line. Let us call it next-prime. It
should take a prime and find the next prime in the number line by
stepping up the number line by one and testing for prime-ness.
(define next-prime
{ prime --> prime }
X -> (next-prime* (+ 1 X))
)
(define next-prime*
{ number --> prime }
X -> X where (prime? X)
X -> (next-prime* (+ 1 X))
)
However, if we try to compile the code up to this point, we find that
we get the following not-so-helpful error message.
Correctness Check Failure; rule 1 of next-prime*
Why does this happen? Obviously, the type system cannot prove that X->
X is a prime where (prime? X). While in the non-typesafe version of Qi,
this function does indeed perform as requested. But because the type
checker cannot prove that it will output ONLY primes, it cannot
typecheck our program. To make our function work, we have to let the
typechecker understand that if a number passes (prime? X) then it
definitely is a prime.
Fortunately for us, Qi provides a mechanism that can check the guards
and give a type depending on if a guard passes. Qi has a special type
for guards called "verified" that only matches when the guard itself
returns true. The guard obviously runs at runtime but Qi can use the
verified to ensure that we have correct types even at compile time. Our
assumption is that if (prime? X) is "verified" then X is a prime. In Qi
notation we then have the new prime type as follows.
(datatype prime
if(and (number? X) (prime? X))
_________
X : prime;
____________________
(prime? X) : verified >> X : prime;
)
We now have a complete (but very inefficient) version of the class of
numbers we know as primes as a native Qi type. No non-prime will ever
typecheck to the type prime even during runtime or after mathematical
manipulation. Let us try it out.
(2+) (next-prime 5)
7 : prime
(3+) (next-prime 7)
11 : prime
(4+) (next-prime 101)
103 : prime
(5+) (next-prime 103)
107 : prime
(6+) (next-prime 107)
109 : prime
(7+) (next-prime 109)
113 : prime
(8+) (next-prime 113)
127 : prime
(9+) (next-prime 4)
error: type error
(10+) (next-prime* 4)
5 : prime
A good follow up exercise would be to take the stream datatype defined
in the Qi Language book and make a stream of primes with these
functions. Also, you could extend the type to use a new prime? function
that implements a wheel sieve to ensure much faster testing for primes.
As a final question, is there any way to rid ourselves of the number?
test inside of primes? I've tried using sequents, subtypes, and a
host of other methods but it always causes the program to crash on
typechecking with sec.SQRT: &&X is not a NUMBER.
Hope you enjoyed my little prime type and happy hacking!
EntropyFails
5 Comments:
Very cool! :-)
Thank you!
Since your blog expresses some interest in Qi, I’ll link to it on my sidebar the next time I update my page.
Try out some weird Qi types of your own there! I had a lot of fun building this types. And I typically hate types... *grin*
By 
EntropyFails, at
10:06 AM
Question: Can Qi code call ordinary Lisp functions? Or would that cause the type system to faint dead away?
Somehow I missed your comment, sorry.
Yes, Qi can call ordinary lisp functions just fine. However since Qi runs in case sensitive mode, you have to put your lisp calls in the front. For example, I've compiled CL-PPCRE into my lispinit.mem and I can do the following in Qi.
(2-) (MULTIPLE-VALUE-LIST (CL-PPCRE:SCAN-TO-STRINGS "(a)*b" "xaaaab") )
["aaaab" #["a"]]
Neato eh?
By EntropyFails, at
12:04 PM
s/the front/capital letters
*sigh*
By EntropyFails, at
12:12 PM
