At some point when using Qi, you may find yourself wanting to do a bit more than the system provides natively. Perhaps you want to double click a .qi file and have it run in Qi. Perhaps you want to do some text processing and you need the CL-PPCRE regular expression library. If you do have either of those needs, you are in luck. I’ll explain how to do both in this article. But I'll try to keep an eye towards what's going on under the hood in Qi so we can better understand the motivation for this code.
First, let us cover passing files to the Qi.bat file and having them run. This is equivalent to double clicking on a .qi file in windows explorer with the proper file type associations set. The current Qi.bat that comes with Qi 6.2 does not allow you to pass .qi files on the command line into Qi. If we look at Qi.bat, we find that it simply loads CLISP with the startup_qi.txt file on the command line as an argument. It has 2 lines
(TERPRI)
(qi::qi)
Terpri prints a newline to the output stream then calls the main (qi::qi) function. If we want our system to understand arguments, we will have to do it before the (qi::qi) line. This is because at that point, Qi takes over and we have lost our chance to get back to the arguments. What we need to do is initialize the qi environment ourselves and load our .qi file given on the command line. Finally, we can call (qi::qi) knowing our file has been loaded into the system. In the following, we find a load_n_launch function that does exactly this. Note that while the function is mostly written in Lisp, it can makes calls to the qi subsystem via the package operator. It is important to remember that even at this point we have entered a "Qi like" environment. To better understand why, we need to understand how Qi bootstraps itself.
The Qi Bootstrap - How to build your own Qi
- Creating a .lisp file from the language .qi file. Qi is written in Qi. It creates a Lisp file from the version in the Qi language. We will call this qi.lisp.
- Running the install.txt code on the new qi.lisp file. Qi has an "Install Qi" folder in the distribution where you should find a fresh CLISP exe and initialized memory file. It should also have the "Qi 6.2.txt" which corresponds to what I have called qi.lisp. It also has install.txt which is a lisp program that performs the following operations.
- Makes a "qi" package
- Loads the qi.lisp file and compiles it into memory.
- Saves the memory as a new startup image.
- Finally, you can run lisp.exe -M with the new memory image that was created. You include the startup_qi.txt file to launch the qi read-print-eval loop.
So we understand the qi bootstrap process better now and we can see why things in our qi_startup.txt can be a bit wierd. Let us specify an argument loading version of qi_startup.txt
(TERPRI)
(DEFUN LOAD_N_LAUNCH (X)
(COND ((EQ X NIL) "Done Loading")
(T (qi::load (CAR X))
(LOAD_N_LAUNCH (CDR X)))))
(qi::initialise_environment)
(LOAD_N_LAUNCH EXT:*ARGS*)
(qi::qi)
All we have to do now is create a version of the qi.bat file that launches qi. It should simply run the lisp.exe with the lispinit.mem file that the Qi bootstrapper created and pass along any arguments it recieves. I personally like to have it be able to load from anywhere so I include the full path in the specification of the executable and the memory image.
"D:\tools\Qi 6.2\lisp.exe" -M "D:\tools\Qi 6.2\lispinit.mem" "D:\tools\Qi 6.2\qi_launcher.txt" %1
Of course, when you are playing with your memory images, make sure to keep a backup around in case something goes awry. Now if you double click a .qi file (assuming you never tried before), will ask you to choose which program to run it with. Select the "Choose from a list" option, then select the
"Browse" option and find your version of Qi.bat. Your program should launch and include all the wonderful functions you have defined. It makes debugging much easier in my opinion.
Obviously, you could place whatever code you wanted in the load_n_launch spot. Just call qi::qi to get into the main qi loop at the end of it and everything should work fine. But this brings us to the second issue, what about lisp functions we want to load? Unfortunately, we could not place them in the load_n_launch spot because QI already has changed many important things like case sensitivity and which characters count as "comments" among other things. If we try to load a lisp file, we will likely encounter errors.
So how do we get CL-PPCRE into Qi? The easiest way is to include the entire package into our memory image. Once we have a lisp memory image with the functions included in it, we can then make a Qi image that will have access to the original functions. While the steps below work, they create monster images in terms of memory size. So be certain you only include the things you really need. Oh, and there are better ways of doing this but I don't know about them yet. Feel free to enlighten me.
- Download the latest version of CLISP
- Download the latest version of CL-PPCRE
- Run CLISP and type (load "path\\to\\CL-PPCRE\\load.lisp")
- Type (EXT:SAVEINITMEM) to save the lisp image. Then type (CD) if you don't know what directory it saved them in.
- Copy the lispinit.mem and the contents of the CLISP/full directory, into your Install Qi directory.
- Type lisp.exe -M lispinit.mem install.txt
- Copy lisp.exe and lispinit.mem into the main Qi directory.
And that will give you a customised version of Qi! You can now perform wonders such as
(1-) (CL-PPCRE:SCAN-TO-STRINGS "(a)*b" "xaaaab")
"aaaab"
But remember, Qi only reads off one result at the top level. To see the rest of your results, you have to use multiple-value-list
(2-) (MULTIPLE-VALUE-LIST (CL-PPCRE:SCAN-TO-STRINGS "(a)*b" "xaaaab") )
["aaaab" #["a"]]
If you have anything else you need to load, you can do it in the above manner.
So in short, we can have our cake and eat it too. If you can get something working in CLISP, you should be able to get somethign working in Qi. I hope these tips help your Qi experience and let me know what you think!
Qi Programming Basics: Where Guards and Backtracking.
In Pattern Matching Basics, we learned about values that must match literals or named parameters. We also learned that this pattern matching can fail. We learned that on the right hand side, you can return a value when the left hand side matches. But what if we want to ensure our variable matches also meet some other specific conditions?
Having covered the left hand side of the arrow operator, we can now cover the right hand side of the -> operator, which deals with restricting function calls. The “where” allows us to call whatever function we want to and have it return only if said “where’ function returns true. If the where returns false, we continue down the function definitions until we find both a left hand pattern match, and a right hand “where” clause satisfaction. Let us take a simple example, greater-than-10
(define greater-than-10
X -> true where (> X 10)
_ -> false
)
(11-) (greater-than-10 20)
true
(12-) (greater-than-10 5)
false
Just as the pattern matching side acts as a sieve for the structure of the input, the where clause acts as functional sieve to ensure that the data matches certain parameters. It makes it easy to define recursive functions. Simply specify the basic cases first and the recursive cases after. The prime? function given in the Qi language book shows this behavior well and I’ll include it here
(define prime?
X -> (prime1? X (sqrt X) 2))
(define prime1?
X Max Div -> true where (> Div Max)
X Max Div -> false where (integer? (/ X Div))
X Max Div -> (prime1? X Max (+ 1 Div)))
So prime calls prime1? setting X to the prime we want to test for, Max to the sqrt of X to limit the prime testing, and Div to 2. If the Div is greater than the Max, it returns true because obviously we have tested for primeness up to the sqrt of X. If it finds any integer divisors, the number is obviously non prime so it returns false. If we pass the first 2 where clauses, then we know we need to test another number so it adds 1 to Div and calls itself recursively and thus walks up to Div > Max. This specifies the prime numbers and is easy to read, but inefficient.
So now that we understand the simple basics of the where clause, we use them to implement some very interesting constructs. Qi provides some syntactic sugar to make writing these sorts of constructs easier, but we should remember that we are only truly dealing with the “where” clause fundamentally. We need to learn about a few new important operators and a new literal. First, we introduce the <- notation that we use instead of -> to signify that if the pattern on the left matches, and the function on the right does not fail, then we can return the result. We specify the idea of “failure” by the literal #\Escape, which is also known as the failure object. We will also introduce a form called “fail-if” that can help make these functions more readable and robust.
Let us begin with a simple case of a binary tree of numbers built out of lists. We will use the empty list to signify a null tree. So we have structures like [L X R] where L and R are lists of that type or empty lists.
(62-) [[[[] 4 [] ] 2 [[] 5 []]] 1 [ [[] 6 []] 3 [ [] 7 []] ]]
[[[[] 4 []] 2 [[] 5 []]] 1 [[[] 6 []] 3 [[] 7 []]]]
Now let us use an old backtracking standby of the computer science world, DFS. DFS, for those who do not know, stands for Depth First Search. A DFS goes to the left hand side and right hand side while printing its way around the list. How it prints depends on if we have want a preorder DFS, an inorder DFS, or a postorder DFS. You can find more on the concept at the
Wikipedia Tree Search Algorithm page. We can define a tree that looks like the tree on that page as follows. (Here we use the “set” function to set a symbol to the value of the list, to make things easier to read.)
(70-) (set *b-list* [ [[[] g []] h [[[] f []] i [[] e []]]] a [[] b [[[] d []] c []]] ] )
[[[[] g []] h [[[] f []] i [[] e []]]] a [[] b [[[] d []] c []]]]
So how can we use the backtracking operator and the #\Escape symbol to implement this algorithm? First, we must note that we will need to return the #\Escape object for every result. This will ensure that our backtracking operations continue to happen even after we have matched something successfully and have “done” something (in this case print out an element). The basic case is when we have an empty node of only one element, for example [ [] 7 [] ] should print 7 and return the failure object.
[[] X []] -> (do (output "~A " X) #\Escape)
That accomplishes that for us. It is also the base case so we can put it at the top of the function. Obviously, we don’t want it to backtrack, as it is the basic case, so we use the -> operator to indicate that we wish to stop backtracking when this rule matches. But note that it does return the #\Escape element, as we don’t’ know where we are in the tree and we want any additional backtracking left on the stack to continue. The important point to remember is when a function returns something other than #\Escape, we halt the computation.
What about the rest of the function? It depends on if we want preorder, inorder, or postorder printing of elements. We will start with the preorder case as we can follow the computation a bit more easily. It should print the first element, then print the left tree, then print the right tree. But at each of those operations, we want it to backtrack and continue on even after it has printed or displayed part of the tree for us. In this way, we can use the function stack as our “visit” stack. (Stacks are a requirement of DFS) By going back up the computational stack, we can find the next element that we should print. For Preorder we have
[L X R] <- (do (output "~A " X) #\Escape) [L X R] <- (dfs-pre L) [L X R] <- (dfs-pre R) So what this means is that it prints out the X, then returns #\Escape which fails. This causes us to backtrack to the next rule, the (dfs-pre L) rule. Note that this also uses the <- operator, so when it finishes with an #\Escape (which is the only thing our function returns) we then can go to the (dfs-pre R) rule. But what happens when the (dfs-pre R) rule fails? We want another default case to return #\Escape for any computation that has gone this far. _ -> #\Escape
Putting this together gives us the following definition.
(define dfs-pre
[[] X []] -> (do (output "~A " X) #\Escape)
[L X R] <- (do (output "~A " X) #\Escape)
[L X R] <- (dfs-pre L)
[L X R] <- (dfs-pre R)
_ -> #\Escape
)
(86-) (dfs-pre (value *b-list*))
a h g i f e b c d #\Escape
The letters above are the results from the “output” function. The #\Escape is the end of our computation, as our function only returns #\Escape, we should not feel surprised to see it at the end of our output from the top level.
We can accomplish post order by simply switching around the order that the function calls come in the list. Instead of printing first and backtracking to dfs L and dfs R, we can put the print at the end and come up with postorder.
(define dfs-post
[[] X []] -> (do (output "~A " X) #\Escape)
[L X R] <- (dfs-post L)
[L X R] <- (dfs-post R)
[L X R] <- (do (output "~A " X) #\Escape)
_ -> #\Escape
)
(88-) (dfs-post (value *b-list*))
g f e i h d c b a #\Escape
And finally, we can define inorder as the following, by placing the print in between the L and R cases.
(define dfs-in
[[] X []] -> (do (output "~A " X) #\Escape)
[L X R] <- (dfs-in L)
[L X R] <- (do (output "~A " X) #\Escape)
[L X R] <- (dfs-in R)
_ -> #\Escape
)
(89-) (dfs-in (value *b-list*))
g h f i e a b d c #\Escape
Now if you input the following at the top level and run that program again, you will be able to see each of the inputs and watch how the #\Escape return values help move this backtracking along.
(91-) (track dfs-in)
dfs-in
(92-) (step +)
True
Long time computer science types will realize that this is a foolish way to handle DFS, and I would like to point out that I chose this method because walking trees is fairly well known and simply helps us learn. We can define a DFS inorder much easier by simply appending lists together. It takes no more lines in Qi than it does in Haskell.
(define dfs-pre*
[] -> []
[L X R] -> (append (append [X] (dfs-pre* L)) (dfs-pre* R)) )
(95-) (dfs-pre* (value *b-list*))
[a h g i f e b c d]
Nicer, but not my point. *smile*
Now perhaps we want to fail on a specific test of a result as opposed to using only the #\Escape operator to handle backtracking. Could our dfs function return true and still allow for backtracking? Fortunately, Qi provides us with a special form called “fail-if” that does exactly that. It takes in a function and a value. It tests to see if the value causes the function to return true. If it dose, it starts backtracking. If the test returns false, however, it stops backtracking. It basically means “backtrack if true”. Let us make a version of dfs-pre that uses these semantics.
(define dfs-pre
[[] X []] -> (do (output "~A " X) true)
[L X R] <- (fail-if (/. Y Y) (do (output "~A " X) true))
[L X R] <- (fail-if (/. Y Y) (dfs-pre L))
[L X R] <- (fail-if (/. Y Y) (dfs-pre R))
_ -> true
)
(111-) (dfs-pre (value *b-list*))
a h g i f e b c d true
Now after listing this form, try to see how the backtracking operator connects to the “where” clause described earlier. We have a test like in where. (/. Y Y), and we pass over clauses that do not match this test. All we are missing is a way to ensure that we don’t double up on the clauses. We want to return the clause AND test it in our where. Let us try a final rewrite of dfs-pre that uses only the usual -> operators and the where. We would like it to look like.
(define dfs-pre
[[] X []] -> (do (output "~A " X) true)
[L X R] -> (let Result (do (output "~A " X) true)
Result) where (not Result)
[L X R] -> (let Result (dfs-pre L)
Result) where (not Result)
[L X R] -> (let Result (dfs-pre R)
Result) where (not Result)
_ -> true
)
However, you can see the Result variable goes out of scope at the end of the let and thus is not available to the where clause. If you tried to compile this you would get
======> Warning:
the following variables are free in dfs-pre: Result;
But you should remember that Qi deals with this internally and we can simply use the expressive power of the <- and fail-if operators to handle our backtracking for us.
Obviously, that serves as only the beginning of what we can accomplish with backtracking in Qi. In chapter 7 of the language book, we find a proplog based system that uses backtracking to build a backward chaining proof procedure. Hopefully, this guide should give you enough background on how the Qi where clause works so that you can fully understand the code in that chapter.
I hope you enjoyed this little guide to the Qi where clause and backtracking in general. Using backtracking can greatly enhance the expressiveness of your program and provide a powerful syntax for dealing with recursion and non-determinism. Please let me know any questions or comments that you have!
The Qi language has the ability to create functions that return different results depending on the inputs. In most languages besides Haskell, ML, and Prolog, you must simply specify inputs and then test each input to determine what you want the function to return. This ends up cluttering the function definition with many “if” or “case” statements. This in turn lowers the readability and writeability of the language in question. Advanced functional languages take advantage of a special syntax that allows the definition of the return value based on the inputs to the function.
A second, and more important, use for pattern matching is for binding the formal parameters of the function. In many languages, if you wish to extract different parts of the parameters in a function, you have to define local variables to hold the parts that you are interested in. In Qi, you use the pattern matching operator to do the special assignment for your cases up front. This simplifies the programming and makes the program more readable (and hence maintainable).
Qi provides 2 special operators for the purposes of parameter pattern matching. The -> operator is equivalent to the = operator in Haskell. It specifies that a pattern matched to the left of the arrow will produce the results specified on the right of the arrow, after rewriting the function on the right to use the values matched on the left. The other operator is _ and it basically tells the rewriter to “throw away” the input. Thus the Qi pattern matching system corresponds to what computer scientists call a priority rewrite system.
Now that we have dispensed with some dense technical verbiage, let us look at what all of this actually means to a Qi programmer. We will start with the first meaning of pattern matching, namely matching basic elements with no bound formal parameters (i.e. none of what you would call “variables”). We will take 3 animals, jane, chuck, and rex and make a function called likes_to_eat that lets us know that jane likes pizza, chuck like cereal, and rex likes dog_food.
(define likes_to_eat
jane -> pizza
chuck -> cereal
rex -> dog_food
)
(11-) (likes_to_eat jane)
pizza
(12-) (likes_to_eat rex)
dog_food
Seems simple enough, no? So now lets see what our function has to say about what bob likes to eat.
(13-) (likes_to_eat bob)
error: partial function likes_to_eat;
It produces an error as expected as we have not defined what bob likes in the above function. The error message could perhaps be more useful, but it does point us to the problem. Qi will also then ask if we want to “track” the function. This is Qi’s way of helping us find where we went wrong in our function call. If you say yes, Qi will display a lot of diagnostic messages when it encounters the likes_to_eat function so you can determine what went wrong.
So let us modify our function to return the symbol “unknown” whenever we don’t know the animal that the function was called with. We use the _ operator to tell the system that we don’t care about the input, we just want to return unknown if we reach the pattern.
(define likes_to_eat
jane -> pizza
chuck -> cereal
rex -> dog_food
_ -> unknown
)
Running this version gives us the following output.
(21-) (likes_to_eat bob)
unknown
Note the difference between this version and the following
(define likes_to_eat
_ -> unknown
jane -> pizza
chuck -> cereal
rex -> dog_food
)
(23-) (likes_to_eat jane)
unknown
The pattern matches from top to bottom. Thus the _ operator matches anything input and returns unknown as a result, even though we have specified jane later on in the function. This is only the beginning of how tricky these sorts of rewrite rules can be, but as long as you remain aware of the order of evaluation, you should have relatively few problems with them.
While returning “unknown” is OK, we may want a more useful error message. We now want to modify our function likes_to_eat to display a helpful error message that tells us WHAT caused the function to fail. We also want to stop the computation at this point. Qi provides a helpful function called “error” that stops the program and returns a string. We will make the string say “likes_to_eat has not heard of bob” if we input bob.
To make the program work as we described, we want to return the following function (error "likes_to_eat has not heard of ~A" bob). Of course, you can immediately see that bob is a variable that we will need to input into the error function. This allows us to introduce the concept of formal parameters. In Qi, formal parameters start with an upper case letter. For simplicities sake, let us call the variable which will bind to bob X. Now our result becomes (error "likes_to_eat has not heard of ~A" X) where X is bound to bob. The Qi syntax makes this rule easy to write, just put X on the left of the arrow. We thus create a new definition of likes_to_eat.
(define likes_to_eat
jane -> pizza
chuck -> cereal
rex -> dog_food
X -> (error "likes_to_eat has not heard of ~A" X)
)
(26-) (likes_to_eat bob)
error: likes_to_eat has not heard of bob
Now let us take a look at a more complicate pattern matching question. In Qi, we can use any of the special constructor forms on the left hand side of the arrow operator. These forms are “list”, “cons”, and “@p”. We can also use the “|” operator inside a list to extract the cons form. I recommend reading the Qi Language book to better understand these forms, but a simple exercise should suffice to show any programmer versed in list processing how they operate.
(43-) (list a b c)
[a b c]
(44-) [ a b c ]
[a b c]
(45-) (cons a (cons b (cons c [])))
[a b c]
(46-) (@p 1 2)
(@p 1 2)
(47-) [ a b | c]
[a b . c]
(48-) [ a | b c]
error: Improper use of |
(48-) [ a | [b c] ]
[a b c]
Let us create an analog of the Haskell take function that takes N arguments from a list and returns the elements extracted. Defining it recursively, we find that if N is 0, then return [] or if the list is [] for any N, return []. Finally, return the application of take to itself by making a list of the head elements and the tail elements being the results of take N – 1.
(define take-alpha
0 _ -> []
_ [] -> []
N [X | XS] -> [ X | (take-alpha (- N 1) XS) ] )
For the first 2 patterns, we can easily see what the patterns match to. For the final pattern, we find that we get a number N and something called [ X | XS ]. This form means that X is the single element head of the list and XS is the remainder of the list. Each call to take-alpha reduces the number of elements in the list by one and reduces the N by one.
(50-) (take-alpha 2 [ a b c])
[a b]
The first 2 patterns work slightly differently than Haskell programmers may be used to. To show this, let us define a function take-beta that reverses the first 2 rules.
(define take-beta
_ [] -> []
0 _ -> []
N [X | XS] -> [ X | (take-beta (- N 1) XS) ] )
(51-) (take-alpha 0 bad_thing)
[]
(52-) (take-beta 0 bad_thing)
[]
(53-) (take-alpha bad_thing [])
[]
(54-) (take-beta bad_thing [])
[]
This differs from Haskell in that Haskell would return the bottom operator for the middle 2 elements because it could not match bad_thing to the list or the number respectively. The typesafe version of Qi would throw an error at compile time if we attempted such a call. In that case, Qi provides a default symbol called #\Escape that works along the lines of the Haskell bottom operator (with significant differences not described here). Regardless, we can see that the notion of “more defined” that we find in Haskell does not apply to the general version of Qi.
You can make the left hand side of the equation as complicated as you wish. We will create a list that has alternating types, the first being a number and the second being a tuple created by the @p operator. For example, we would like the function to make [ 1 (@p 3 4) 5 (@p 8 5)] add up to 26. We want it to be able to do it for any valid list length. The definition follows.
(define complicated-list-add
[] -> 0
[ X | [ (@p Y Z) | XS]] -> (+ (+ X (+ Y Z)) (complicated-list-add XS))
)
Testing this function gives
(58-) (complicated-list-add [ 1 (@p 3 4) ])
8
(59-) (complicated-list-add [ 1 (@p 3 4) 5 (@p 8 5)])
26
If we try to simply input 3 numbers we get the following error.
(60-) (complicated-list-add [ 1 2 3])
error: partial function complicated-list-add;
The pattern matcher could not match 2 to (@p X Y) so it returns the same error we saw when we tried to call likes_to_eat with bob. It doesn’t know how to apply it and it gives us an error. If we wished, we could add error handling in the same manner as likes_to_eat.
One final point remains on the basics of pattern matching in Qi. What happens if we have a variable that we didn’t specify on the left hand side of the arrow? The rewrite rule described above wouldn’t know how to decipher it as we didn’t explicitly define it. Qi has chosen the route of warning the user but defining the function as opposed to generating an error. We can see the behavior below.
(define bad-rewrite
X -> Y)
======> Warning:
the following variables are free in bad-rewrite: Y;
bad-rewrite
(62-) (bad-rewrite 10)
Y
If you are a Lisp programmer, you may worry about variable capture due to this rewrite rule. Fortunately, Qi handles this case for us via the rewrite system and we don’t have to worry about it in this case. This also means we can return proper names from functions in the relatively few cases where we want to do this. But expressive power always means we need to take care of how we code things, thus the reason for the warning.
(63-) ((/. Y (bad-rewrite Y)) 12)
Y
Whew. Congrats to all that made it to the bottom of this pedantic look at the Qi pattern matching system. You should note that this only covers rewrite rules without guards (the Qi “where” special form). If you delve further into Qi, you will find that the combination of the arrow and where can allow native backtracking of the functions that you call. Yes, I said native backtracking of function calls! More on that later.
Enjoy your Qi!
PS: Mark Tarver, the main implementer of Qi, had this to say about the warn vs error issue with Qi variables.
The main motivation for this is to allow users to mix
Lisp code into Qi code. Since Lisp reverts to the
uppercase when case sensitivity is invoked (Qi is
case sensitive), if you want to mix Lisp into Qi you have to violate
the free variable condition.
(0-) (define implode
Chars -> (COERCE Chars STRING))
======> Warning:
the following variables are free in implode: COERCE; STRING;
implode
(1-) (implode [#\a #\b #\c])
"abc"
You see the idea, that is why you get a warning and
not an error. Being able to mix the two is a big plus.
However if you really want to block off functions like
bad-rewrite then (strong-warning +) will do it and you
get an error and not a warning.
(3-) (strong-warning +)
true
(4-) !0
0.
(define implode
Chars -> (COERCE Chars STRING))
error: the following variables are free in implode: COERCE; STRING;
Mark
The Qi type system allows for some very interesting types not typically available 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
The Qi Programming language extends Common Lisp to provide complete First Order Logic types, function guards, and pattern matching. When you program it, it feels a bit like Lisp and a bit like Haskell. It has native and pure lambda expressions which means you get all the wonders of currying, partial application, and continuations with none of the Monads. You get all this and more for the low, low price of GPL.
Welcome to the Programming Kung Fu Qi blog. I’ll be posting about whatever I can learn of this language and hopefully we can develop a community of people interested in finding out what Qi offers to the computer science world.
Get your hack on by downloading Qi at...
http://www.lambdassociates.org/
Then hop on the Qi discussion board at...
http://groups.google.com/group/QilangEnjoy!
