Programming Kung Fu Qi

Existential Data Constructors in Haskell and Qi

2007-08-23T09:27:00.000-07:00

In Haskell, if we have a type A and a set of functions from A to some other type, we may wish to encapsulate this logic inside of a new general type that does not contain a reference to A. We would like to be able to pass different data and functions to this type constructor and have the dependent functions work across all types, given a proper datatype for our function and data that matches that datatype. Haskell calls this pattern "Existential Data Construction."

In A History of Haskell: Being Lazy With Class , Hudak, Hughes, Wadler, and Jones provide the following Haskell datatype as motivation for existential data constructors.


data T = forall a. MkT a (a->Int)
f :: T -> Int
f (MkT x g) = g x

Reading this type is fairly straight forward. We say that for any type a, we can call a constructor consisting of a value of that type and a function from type a -> Int and get a type T back. F then takes this supplied T value and uses pattern matching to deconstruct it and forces the call of G on X. Given that G is of type (a->Int) and X is of type a, we can be certain this call will work.

I'm belaboring this point because I think it is important to understand that the Qi type system has this expressive power without requiring a (forall a) existential constructor in the type. In Qi, we can simply specify some generic type A on the right hand side of the type colon around a variable bound below the sequent refinement rule and rest assured that the type theory will deduce the existence of and proper type for A at compile time.

Here is how T looks inside of Qi.

(datatype t
X : A;
L : (A --> number);
======
(@p mk_t (@p X L)) : t;
)

We can read this as saying, "If I need to prove something is of type t I must first prove that it is a constructor that has an X of some arbitrary type A and a function L of type A --> number."

From there, we can define the function f in a similar manner as the Haskell code.


(define f
{ t --> number }
(@p mk_t (@p X G)) -> (G X))

Running this shows how the type system ensures that the A's match up inside the constructor.


(3+) (f (@p mk_t (@p 3 (+ 4))))
7 : number

(4+) (f (@p mk_t (@p a (+ 4))))
error: type error

Like in Haskell, this existential datatype constructor truly covers all types A, as I will show below. In the following code, the type A is bound to (number --> number). Qi, like Haskell, really means it when it says, "any type A".


(7+) (/. X (+ X 3))
#function :LAMBDA [X] [+ X 3] : (number --> number)

(8+) (f (@p mk_t (@p   (/. X (+ X 3))
                     (/. Y   (Y 7))   ))   )
10 : number

I hope this explanation helps further the understanding of the Qi type system for Haskell users interested in Qi. Feel free to ask any questions you may have.

Haskell-like Type Classes in Qi

2007-08-17T10:58:00.000-07:00

In my studies of Qi, I often use Haskell as an endless pool for mining good ideas. I find that by translating these ideas into Qi, I end up learning both Qi and Haskell better than I would have done by trying to understand them separately. For example, I was immediately able to understand that "Multi-parameter Type Classes with Undecidable instances" was really just "Sequents with bad syntax." But one area that Haskell reigns supreme is the Type Class.

Qi does have a sub-classing mechanism. If you define a type under the universal truth that (subtype integer number) then you can define a type rule that says


      (subtype B A); X : B;
      _____________________

      X : A;

and integers can now go wherever numbers go. Basically, it is a promise to the compiler that you are REALLY sure the implementations of the types match up and all the proper functions have been provided. Honest. You promise... That tends to fail in practice. And this sub-classing system does not provide any ability to do ad hoc polymorphism.

The Haskell idea is to use special syntax to pass around a hidden object that carries all of the required functions and is properly typed. They call this a Type Class. It is an incredibly handy feature because it provides a way to guarantee that you have met the basic needs of a function that requires the type class. It also allows function overloading, a feature Qi lacks.

So how would this feature look if ported inside of Qi? I would imagine it would looks something like the following code snippet. Note that the "class_" prefix on * is due to Qi not allowing the redefinition of operators. I'll use that notation convention throughout, as I rebuild the (num N) class in Qi.


(define square
  { (num N) ==> N --> N }
  X -> (class_* X X))

The meaning of the statement is the same as Haskell. If I have a (num N) class then I can use the class_* to call the proper function. Internally, Qi would transform this construct into the following along the same manner as Haskell.


(define square
  { (num N) --> N --> N }
  D X -> (num_* D X X))

The code to perform this transformation will not be provided. This code would have to be intimately tied into the type system and would require a very large change to Qi. It may be worth it, but it is not the point of this article. I will perform the transformation by hand and demonstrate from there.

For the purposes of this article, I will be providing the base types integer and float. They both have their own type specific operations. I will create instances of them into the (num N) class which will also propagate that instance to the subtype (eq N).

Haskell defines the EQ class as


class  Eq a  where
    (==), (/=)       :: a -> a -> Bool

Haskell hides the creation of the constructor type for EQ, but in the final transformation it gets an explicit expression inside the compiler. The final transformation should create both a new Qi datatype and some new generic functions that the type class requires. I provide the transformation in Qi below.


(datatype eq
  Equal    : (A --> (A --> boolean));
  NotEqual : (A --> (A --> boolean));
  ===
  (@p mkeq (@p Equal NotEqual)) : (eq A);
)

(define class_equal
  { (eq N) --> N --> N --> boolean }
  (@p mkeq  (@p Equal _))  
  X Y -> (Equal X Y))


(define class_notequal
  { (eq N) --> N --> N --> boolean }
  (@p mkeq  (@p _ NotEqual))
  X Y -> (NotEqual X Y))

As you can see, the idea is to pass along the proper EQ object for the function type and use pattern matching to splice in the arguments and the proper function and then call it. Getting this transformation to take arbitrary code and make these datatypes and functions requires most of the work. The final result can work as these hand written functions do, but a real implementation would structure things differently.

The instance declaration in Haskell looks something like the following


instance Eq Integer where 
  x == y                =  x `integerEq` y

instance Eq Float where
  x == y                =  x `floatEq` y

The final transformation of the Qi code would look like the following snippet. It provides the needed functions for the type class by taking the type specific functions and putting them into a type class container. This is the same container that we send to every function that requires a type class. All we need to do is provide the base implementations in the proper spots. In a full Qi type class implementation, we would have to use some special syntax or data structure to cause these functions to auto-generate themselves.


(define instance-eq-integer
  { A --> (eq integer) }
  _ -> (@p mkeq  (@p equal-integer notequal-integer)))


(define instance-eq-float
  { A --> (eq float) }
  _ -> (@p mkeq  (@p equal-float notequal-float)))

When we run the code, it behaves as expected.


(39+) (class_equal (instance-eq-float 0) 2.3 2.3)
true : boolean

(40+) (class_equal (instance-eq-float 0) 2.3 2.4)
false : boolean

(41+) (class_equal (instance-eq-integer 0) 2 2)
true : boolean

(42+) (class_equal (instance-eq-float 0) 2.0 2)
error: type error

Notice that line 42 fails. To perform this kind of analysis, we will need a type class that captures both equality and the idea of being a number, with a way to translate them from the integers. Haskell defines the (num N) type in a way very close to the form below.


class  (Eq a) => Num a  where
    (+), (-), (*)    :: a -> a -> a
    negate           :: a -> a
    abs, signum      :: a -> a
    fromInteger      :: Integer -> a

We can define an equivalent structure in Qi by embedding the eq subclass directly into the mknum structure. The compiler would also need to provide a function to walk the subclass tree.


(datatype num
  Subclass : (eq A);
  Plus   : (A --> (A --> A));
  Minus  : (A --> (A --> A));
  Mult   : (A --> (A --> A));
  Neg    : (A --> A);
  Abs    : (A --> A);
  SigNum : (A --> A);
  FromInteger : (integer --> A);
  ===
  (@p
  Subclass
  (@p mknum (@p Plus 
            (@p Minus
            (@p Mult
            (@p Neg
            (@p Abs
            (@p SigNum FromInteger)))))))) : (num A);
)

(define num_to_eq
  {(num N) --> (eq N)}
  (@p
  (@p mkeq  (@p E Ne))
  (@p mknum (@p _
          (@p _
          (@p _
          (@p _
   (@p _
   (@p _ _)))))))) -> (@p mkeq  (@p E Ne)))

The basic function definitions work like equal type class from above.


(define class_*
  { (num N) --> N -->  N --> N  }
  (@p
  _
  (@p mknum (@p Plus 
          (@p Minus
          (@p Mult
          (@p Neg
   (@p Abs
   (@p SigNum FromInteger))))))))

  X Y -> (Mult X Y))

And we declare the instance by providing all of the functions in their proper slots.


(define instance-num-integer
  { A --> (num integer) }
  _ -> 
  (@p
  (instance-eq-integer 0)
  (@p mknum (@p plus-integer 
          (@p minus-integer
          (@p mult-integer
          (@p neg-integer
   (@p abs-integer
   (@p signum-integer frominteger-integer)))))))) )

(define instance-num-float
  { A --> (num float) }
  _ -> 
  (@p
  (instance-eq-float 0)
  (@p mknum (@p plus-float 
          (@p minus-float
          (@p mult-float
          (@p neg-float
   (@p abs-float
   (@p signum-float frominteger-float)))))))) )

So now we have what we need to take on 2.0 == 2.


(class_equal (num_to_eq (instance-num-float 0)) 
             2.0 
             (class_frominteger (instance-num-float 0) 2))
true : boolean

If we encapsulate that into a function 'istwo?' we can see the transformation a bit more clearly.


(define istwo?
  { (num N) --> N --> boolean }
  D X -> (class_equal (num_to_eq D) (class_frominteger D 2) X))

istwo? : ((num A) --> (A --> boolean))

(10+) (istwo? (instance-num-integer 0) 2)
true : boolean

(11+) (istwo? (instance-num-integer 0) 3)
false : boolean

(12+) (istwo? (instance-num-float 0) 2.0)
true : boolean

Ideally, the above 'istwo?' function should be auto-generated by the following Qi like code. Note that the type system would wrap the small constants in frominteger and call the subclass datatype return function to make a valid class_equal call.


(define istwo?
  { (num N) ==> N --> boolean }
  X -> (class_equal 2 X))

To finish, I'll implement squares and sumsquares that work across the type class (num N).


(define square
  { (num N) --> N --> N }
  D X -> (class_* D X X))

(define sumsquares
  { (num N) --> N --> N }
  D X -> (class_+ D (square D X)
                    (square D X)))

(16+) (square (instance-num-float 0) 6.0)
36.0 : float

(17+) (square (instance-num-integer 0) 2)
4 : integer

(18+) (sumsquares (instance-num-integer 0) 2)
8 : integer

(19+) (sumsquares (instance-num-float 0) 6.0)
72.0 : float

In short, type classes are a very powerful programming tool that Qi lacks and should probably have. They give Qi ad hoc polymorphism and define types that also have guarantees about which functions it supports. It would take a fairly large change to the Qi codebase to support the shorthand syntax, but I hope this article has proven that we can implement the powerful Haskell type system in Qi.

Thank you for your time.

Download the full code used to make this article.

Qi 9 Win32 Installer

2007-07-17T20:56:00.000-07:00

Just a note:

You can get the new version of Qi at the Google Qi page.

You can also download the Win32 Installer.

Enjoy!

A Simple SK Combinator Calculus Tutorial in Qi

2007-06-02T01:42:00.000-07:00

As a juxtaposition of my previous use of the Qi type checker to define the SK combinator calculus, I'll now define it very simply in the Qi language directly. I'll present this as a tutorial to those new to the SK combinator calculus.

The SK calculus shows us that at maximum there are only three rules of logic: Pattern Matching, Deleting, and Copying. It also shows that their is only one way of evaluating them, namely by application. You can think of the three rules as "Highlighting", "Cutting", and "Pasting." With those three simple operations, the entirety of logic and mathematics can be reproduced with only your mouse!

Let us take a loot at deletion... We'll call the operation K. Look at the following transformation. Copy the [[kx]y] into a text editor. Now highlight and "cut" all but the x using only the "cut" command and your mouse.

[[kx]y] -> x

Now, we'll make a new function S which stands for "paste". Try to make the following transformation of [[[sx]y]z] in a text editor. Remember you can only use "cut" and "paste".

[[[sx]y]z] -> [[xz][yz]]

K deletes information and S copies things and applies it to other functions.

Now it should be very easy to understand what the first two lines of following code is doing.

(define sk-eval*

[[k X] Y] -> X
[[[s F] G] X] -> [[F X] [G X]]

[ X Y] -> [(sk-eval X) (sk-eval Y)] 
X -> X)

The last 2 lines simply tell the function to evaluate the inside of our 2 element lists and return anything it doesn't know how to handle.

But you should notice that we have defined sk-eval* but not sk-eval, so we are not quite done yet. What do we mean by evaluation? We should mean that every element has been reduced and modified until we get the same thing back out of our evaluation function as we put into it. In math, an x for a function f with the properties f(x)=x is known as a fixed point. It simply means that we get the same input as output. You should notice that "X -> X" in the sk-eval* function (especially being last), makes this a case where we get to use the fix built-in function in Qi. It keeps applying the function to itself until it reaches a fixpoint. Then it stops.

(define sk-eval
X -> (fix sk-eval* X))

That's it! That's all it takes to complete the evaluator. In our cut and paste metaphor, we would continue to make the required copy and pastes until we could no longer match s and k's with the rules defined above.

Now let us see it in action.

(36-) (sk-eval [[[s k] k] a])
a
(37-) (sk-eval [[[s [[s k] k]] [[s k] k]] a])
[a a]

That's pretty easy. Now let us define some helper functions and show that this sk-eval function knows math.

(define sk    -> [s k])
(define kk    -> [k k])
(define ks    -> [k s])
(define z     -> (sk))
(define succ  ->  [ s [ [ s (ks)] k]])
(define plus  ->  [ [ s (ks)] [ [ s [ k [ s [ k s]]]]
     [ s (kk)]]])
(define mult  ->  [ [ s (ks)] k])
(define one   ->  [ (succ) (z)])
(define two   ->  [ (succ) (one)])
(define three ->  [ (succ) (two)])
(define four  ->  [ (succ) (three)] )
(define five  ->  [ (succ) (four)] )

And now it is time for it to do some math. We will use 1 and 0 to as markers for our functional application to ensure that our evaluator will output a string of the answer in 1's but ended by a 0.

(40-) (sk-eval [[[[(plus) (one)] (two)] 1] 0])
[1 [1 [1 0]]]
(41-) (sk-eval [[[[(mult) (three)] (two)] 1] 0])
[1 [1 [1 [1 [1 [1 0]]]]]]

You could easily host an named SK calculus with the addition of 2 lines of code. I'll leave that as an exercise to the reader.

That's all there is to the SK Combinator Calculus. It is a powerful enough system to define the entirety of mathematics and computation. It shows that all you need is a basic way to match symbols, delete symbols, and copy symbols and you have a Turing Complete system. (I know some squishy bio-computers that do this all the time and perhaps I'll explore that idea in another post.) From this very basic system, you get the entirety of reasoned knowledge. The universe is a strange place indeed.

I hope this helped spread understanding about the SK combinator calculus. Let me know of any questions you have!

A SK Combinator in the Qi Type System, a Comparison with Haskell

2007-05-26T22:02:00.000-07:00

Today I present another proof of the Turing completeness of the Qi type system. I have derived the code for this article from an article about Turing complete Haskell types named The GHC typechecker is Turing-complete by Robert Dockins. In keeping with the tradition of his article, this message is also in a compilable form as long as you grab the starting and ending comment markers. Qi could use a literate code mode.

The SKI combinator calculus is a computation system reduced to its most minimal form. There are exactly 2 operators, S and K. S applies its first two arguments to the third argument while K deletes the second of its two arguments. From that simple strategy, all the known computable functions can be derived. This article will show how this is done in Qi.

I have taken the approach of directly translating, as much as possible, the Haskell article's code into Qi. This should assure you that the same computations are going on and perhaps better convince you of the complete mapping of the SK calculus to Qi types. I will not be providing a correctness proof here.

Firstly, we define empty types that resolve to the primitives s, k, and the pairing operation app. I also define a dummy type (other A) that will allow us to test the application of arbitrary subexpressions that we can conveniently label. Notice that these definitions all type to any variable. I label this variable Bot in the program to indicate that we do not really care about its actual type, we are just using it to host a typechecking operation in the same way as the Haskell program. Either the program will typecheck indicating a successfully application or it will return a type error. We takes these values as true and false respectively.

\
(datatype sk
___
Bot : s0;
___
Bot : k0;
___
Bot : (app A B);
___
Bot : (other A);
\

In keeping with the Haskell code, we now define a single step sk reduction named sk_eval. The evaluator will always reduce the leftmost-outer redix. It will always be reflexive on normal forms. I then create a transitive closure over a sk_eval reduction. I have named the type that does this sk_run.

I will define a combination type to reduce some of the more expensive operations in parallel. If we have an ((S x) y) we know that we will have to reduce both x and y. When we are done reducing x and y, we will need a type to tell the typechecker that we have finished these operations. The following code defines the combine_done type that takes the status of 2 operations and returns done if they both are done.

\
___
Bot : (combine_done done done done);
___
Bot : (combine_done done more more);
___
Bot : (combine_done more done more);
___
Bot : (combine_done more more more);
\

Now we add the sk_eval type for the default evaluations. S, K, and (other A) all are done when they are equal to each other.

\
____
Bot : (sk_eval s0 s0 done);
___
Bot : (sk_eval k0 k0 done);
___
Bot : (sk_eval (other A) (other A) done);
\

All of the previous rules have derived from nothing. That's why the line above the ___ is blank. The next rules are evaluation strategies for when we get near the bottom of the sk tree. If we have been asked if (K x) is equal to (K y) we must ensure x = y. The same goes for (S x).

As a general reminder about those who have not learned sequent notation you can consider them as saying IF the top part can be proven, THEN the bottom part is true. However you should remember that the type checker is working backwards from the type that we will provide it. So you can think of the operation in Qi as, "If I have something that fits the pattern at the bottom, then I will try to prove the top."

\
Bot : (sk_eval X Xp D);
___
Bot : (sk_eval (app k0 X) (app k0 Xp) D);

Bot : (sk_eval X Xp D);
___
Bot : (sk_eval (app s0 X) (app s0 Xp) D);
\

Getting that nice "other" type working gives us some problems. We cannot reduce it any further but we may have to reduce other parts of pairs that are nearby the other type. The one-arity case is very easy.

\
Bot : (sk_eval X Xp D);
___
Bot : (sk_eval (app (other A) X) (app (other A) Xp) D);
\

However in the 2 case, we will need to ensure that the elements to the right fully reduce. That is to say if we have a question if ((p x) y) = ((p x1) y1) we must fully reduce and prove x = x1 and y = y1. The combine_done type now comes in handy as it allows us to fully reduce and prove this assertion.

\
Bot : (sk_eval X Xp D1);
Bot : (sk_eval Y Yp D2);
Bot : (combine_done D1 D2 D);
___
Bot : (sk_eval (app (app (other A) X) Y)
              (app (app (other A) Xp) Yp) D);
\

You can read the bottom part as saying that if we are trying to prove some sk evaluation that has an (other A) at the head we must then prove that X = Xp and Y = Yp and that they are all done before moving on. We can now do the 3-arity version of the other type as we know it will have to reduce the first 3 arguments before it can accept them. We also do the same thing for a single s0 here.

\
Bot : (sk_eval X Xp D1);
Bot : (sk_eval Y Yp D2);
Bot : (sk_eval Z Zp D3);
Bot : (combine_done D1 D2 D4);
Bot : (combine_done D3 D4 D);
___
Bot : (sk_eval (app (app (app (other A) X) Y) Z )
              (app (app (app (other A) Xp) Yp) Zp) D);

Bot : (sk_eval X Xp D);
___
Bot : (sk_eval (app s0 X) (app s0 Xp) D);
\

Now we can define s and k themselves. We have 2 important cases for k. ((K x)y) = x and (((K x) y) z) = (x z)

\
___
Bot : (sk_eval (app (app k0 X) Y)  X  more);

___
Bot : (sk_eval (app (app (app k0 X) Y) Z)  (app X Z) more);
\

Now we define s as (((S f) g) x) = ((f x) (g x)).

\
___
Bot : (sk_eval (app (app (app s0 F) G) X)
              (app (app F X) (app G X))
              more);
\

The final sk_eval rule will prove that ((((p q) x) y) z) = (a z) only when (((p q) x) y) = a. This, along with the other rules above for more simple applications, will reduce the sk combinator on a leftmost-outermost basis.

\
Bot : (sk_eval (app (app (app P Q) X) Y)  A  D);
___
Bot : (sk_eval (app (app (app (app P Q) X ) Y ) Z)
              (app A Z) D);
\

Like the Haskell code, I take the transitive closure of sk_eval with an auxiliary type. It insures that it is done when x = x. It also provides transitivity by saying that if we must prove some sk_eval_aux x = z, then we can prove it by proving an sk_eval x = y and an sk_eval_aux y = z.

\
___
Bot : (sk_eval_aux X X done);

Bot : (sk_eval X Y Q);
Bot : (sk_eval_aux Y Z Q);
___
Bot : (sk_eval_aux X Z more);
\

Now we can create the sk_run class that runs a query. It must prove that x = y by way of using the sk_eval_aux class.

\
Bot : (sk_eval_aux X Y more);
___
Bot : (sk_run X Y);

)
\

Now we have finished defining the basics. Let's try it out. We will check that SKKb = b. Notice that we typecheck vs any particular data. As none of our types require anything from the value being typed, that means that it will match whenever the type is true, regardless of the actual type of what we are testing!


(1+) 1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other b))
1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other b))

Now we will turn on the type spier and watch the program reason its way through this type.

The first step asks the type checker the same question as before. It notices that it is not a default type and poses the type as a goal to the typechecker.


(25+) (spy +)
true : boolean

(26+) 1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other b))
______________________________________________ 9 inferences
?- 1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other b))

So it finds the sk_eval_aux rule that says if we set x = SKKb and z = b then we can use the transitive rule to evaluate the query. Here we see the firing of that rule as a goal to be proven.


>
______________________________________________ 80 inferences
?- 1 : (sk_eval_aux (app (app (app s0 k0) k0) (other b)) (other b) more)

Now we will see the sk_eval x y q rule where y has been replaced with the gensym V26232. The type checker now must prove this to continue. This is the point in where it descends out of the transitive closure and does a single evaluation of the input combinator.


>
______________________________________________ 150 inferences
?- 1 : (sk_eval (app (app (app s0 k0) k0) (other b)) V26232 V26233)

Obviously, it will use the s rule in this case to set the y above to be ((Kb)(Kb)). It then sets that to y and we return to the second part of the sk_eval_aux. That part determines if y = z.


>
______________________________________________ 217 inferences
?- 1 : (sk_eval_aux (app (app k0 (other b)) (app k0 (other b))) (other b) more)

Now it will try to find some sk_eval such that ((Kb)(Kb)) = y and y = b


>
______________________________________________ 287 inferences
?- 1 : (sk_eval (app (app k0 (other b)) (app k0 (other b))) V26371 V26372)

sk_eval will use the k0 rule to return y as (other b). We then return to the second part of the sk_eval_aux and set y = (other b). It will add the second part of that transitive closure rule as a goal.


>
______________________________________________ 352 inferences
?- 1 : (sk_eval_aux (other b) (other b) more)

This will, in turn, set (other b) as an x and ask if there is a y that matches.


>
______________________________________________ 422 inferences
?- 1 : (sk_eval (other b) V26500 V26501)

We know from the very first rules above that the other goal can match (sk_eval (other A) (other A) done) so it sets V26500 as (other b) and V26501 as done.

Now it only has to ask if (sk_eval_aux (other b) (other b) done) is a finished sk evaluation. The first auxiliary rule says that sk_eval_aux X X done is in fact a true type so it adds the goal, solves it, and finishes.


>
______________________________________________ 480 inferences
?- 1 : (sk_eval_aux (other b) (other b) done)

>
1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other b))

Now is SKKb = c?

(1+) 1 : (sk_run (app (app (app s0 k0) k0) (other b)) (other c))
error: type error

Now let us turn to some of the more complicated combinators. It is here that we find Haskell's type keyword to be more powerful than the Qi alternative "synonym". The Haskell type keyword allows both alias style synonyms like type Z = SK0 and parametric type synonyms such as type FoldN n = App (App n P) Q. Qi has no way of doing anything similar to parametric type synonyms, so we will be forced to convert the concise definitions in the Haskell code into the full app form inside for Qi.

I will define a bunch of useful alias synonyms to help us.

\
(synonyms

 p     (other p0)
 q     (other q0)
 r     (other r0)

 sk0   (app s0 k0)
 skk0  (app (app s0 k0) k0)
 sks0  (app (app s0 k0) s0)
 ssk0  (app (app s0 s0) k0)
 sss0  (app (app s0 s0) s0)
 kk0   (app k0 k0)
 ks0   (app k0 s0)

 i0    skk0
 b0    (app (app s0 ks0) k0)
 c0    (app (app s0 (app (app b0 b0) s0)) kk0)
 w0    (app c0 (app (app b0 m0) (app (app b0 b0) (app c0 i0))))
 l0    (app (app c0 b0) m0)
 y0    (app (app s0 l0) l0)
 ki0   (app k0 i0)

 m0    (app (app s0 i0) i0)
 omega (app m0 m0)

 z       sk0
 succ0   (app s0 (app (app s0 ks0) k0))

 plus0   (app (app s0 ks0) (app (app s0 (app k0 (app s0 (app k0 s0))))
    (app s0 kk0)))
 mult0   (app (app s0 ks0) k0)
 one     (app succ0 z)
 two     (app succ0 one)
 three   (app succ0 two)
 four    (app succ0 three)
 five    (app succ0 four)
)

\

When we try out these types, we will find that Qi will fully expand the synonyms and then check the type. It's not pretty to look at, but it works.


(1+) 1 : (sk_run (app succ0 two) three)
1 :
(sk_run
(app (app s0 (app (app s0 (app k0 s0)) k0))
 (app (app s0 (app (app s0 (app k0 s0)) k0))
  (app (app s0 (app (app s0 (app k0 s0)) k0)) (app s0 k0))))
(app (app s0 (app (app s0 (app k0 s0)) k0))
 (app (app s0 (app (app s0 (app k0 s0)) k0))
  (app (app s0 (app (app s0 (app k0 s0)) k0)) (app s0 k0)))))

(2+) 1 : (sk_run (app succ0 two) four)
error: type error

(5+) 1 : (sk_run (app i0 p)  p)
1 : (sk_run (app (app (app s0 k0) k0) (other p0)) (other p0))

(6+) 1 : (sk_run (app (app (app c0 k0) i0) p) p)
1 :
(sk_run
(app
 (app
  (app
   (app
    (app s0
     (app (app (app (app s0 (app k0 s0)) k0) (app (app s0 (app k0 s0)) k0))
      s0))
    (app k0 k0))
   k0)
  (app (app s0 k0) k0))
 (other p0))
(other p0))

(7+) 1 : (sk_run (app (app y0 ki0) p) p)

(8+) 1 : (sk_run (app m0 p) (app p p))
1 :
(sk_run
(app (app (app s0 (app (app s0 k0) k0)) (app (app s0 k0) k0)) (other p0))
(app (other p0) (other p0)))

(10+) 1 : (sk_run (app (app (app c0 p) q) r) (app (app p r) q))
(11+) 1 : (sk_run (app (app (app b0 p) q) r) (app p (app q r)))
1 :
(sk_run
(app (app (app (app (app s0 (app k0 s0)) k0) (other p0)) (other q0))
 (other r0))
(app (other p0) (app (other q0) (other r0))))

(12+) 1 : (sk_run omega omega)
*** - Program stack overflow. RESET

So there you have it, a full SK evaluator inside the Qi type system. I feel that this displayes a lot of evidence for Qi typing being Turing complete, which we already knew. However, I hope that this further shows how much easier it is to reason about the types when using the sequent notation. I find the Qi code much easier to read than the Haskell code. The main area where Haskell shined over Qi is in the parametric type classes. Qi could definately use an extension to the "synonym" keyword. Moreover, Haskell is much better about displaying the type synonyms, leading to less visual junk on the page.

So for those of you that love Haskell, I hope this shows how Qi types work and their comparable expressive power with Haskell. For those of you who love Qi, hopefully you can now more easily read Haskell multi-parameter type classes. And for Qi implementors, I think it shows some directions for further growth of the Qi language. It's been a long article, thank you for your time and I hope you enjoyed it!

\

Foldl and Foldr

2007-05-21T19:28:00.000-07:00

The Haskell prelude defines the types for foldl and foldr as follows.


foldl
type: foldl :: (a -> b -> a) -> a -> [b] -> a
foldr
type: foldr :: (a -> b -> b) -> b -> [a] -> b

In Qi, I have followed that convention in the Qi Prelude.

The reason for defining it this way is fairly easy to see. If we have a binary operator that works over one type and we have an element and a list of that type, then we can use one functions as a drop in replacement for the other. The following code randomly selects foldr or foldl and uses it on a list.


(47-) ((if (> (random 2) 0) foldr foldl) / 1 [1 2 3])
3/2
(48-) ((if (> (random 2) 0) foldr foldl) / 1 [1 2 3])
1/6

But for as how humans tend to think about calling functions, these type orders make reasoning about foldr and foldl more difficult than they need to be. Allow me a few examples to illustrate.


(26-) (foldl + 1 [ 1 2 3 4 5])
16
(27-) (foldr + 1 [ 1 2 3 4 5])
16
(28-) (foldr * 1 [ 1 2 3 4 5])
120
(29-) (foldl * 1 [ 1 2 3 4 5])
120
(30-) (foldr / 1 [ 1 2 3 4 5])
15/8
(31-) (foldl / 1 [ 1 2 3 4 5])
1/120
(32-) (foldr - 0 [ 1 2 3 4 5])
3
(33-) (foldl - 0 [ 1 2 3 4 5])
-15

Obviously there is no difference between foldl and foldr for associative operators. But when we have non-associative operators I think the type order ends up harming readability. I will define a foldr* and foldl* with the type order that feels more natural to me, to display my point. Perhaps this will serve as a useful guide to others who are attempting to understand the difference between foldl and foldr. It should also serve as a reminder that when we try to make one type of programming task easy, we may end up making other reasoning tasks about programs more difficult.


(define foldl*
  { A --> ( A --> B --> A ) --> [B] --> A }
 Z F Ls -> (foldl F Z Ls))
(define foldr*
  { [A] --> ( A --> B --> B ) --> B --> B }
 Ls F Z -> (foldr F Z Ls))

(51-) (foldl* 10 - [1 2 3 4])
0
(52-) (foldr* [1 2 3 4] - 10)
8

I think this quite clearly shows that foldl starts from 10 and keeps subtracting to the right while foldr performs the 4 - 10 and moves to the left. In fact, I think that this shows that even the names of foldl and foldr are backwards from the perspective of the neophyte programmer. Nothing about a quick glance at the following gives away the fact that the first operation will be 4 - 10.


Hugs> foldr (-) 10 [ 1, 2, 3, 4]
8

vs. the re-ordered version, where this is clear.


(52-) (foldr* [1 2 3 4] - 10)
8

I believe that my reordering makes the purpose of foldl and foldr more clear. We can instinctively feel, at a glance, that foldl is taking the list and pushing it left into the first argument by way of the operator. Likewise, we can feel that foldr is "smooshing" the list to the right into the starting value.

I hope that this helps by giving both a little insight into how making code easier to be drop in replacements for other code can actually hurt readability and by helping people to better understand foldl and foldr. As always, let me know what you think.

Qi 7.2 Win32 Self-Extracting Installer With CLISP bundled

2007-04-30T10:24:00.000-07:00

Greetings Blogland,

I have made a quick and dirty one download installer for Qi for the Windows platform. It installs CLISP under the Qi directory and adds a link for Qi in the start menu. I'm using NSIS to create the software so if anyone wants to make the installer better, let me know. I'll be adding the installer code to the SVN repository atthe google code page.

I've also added a Featured Download on the right hand site to help people get to Qi quicker and easier. This is an easy area that needs more work so if anyone feels like maintaining packages, create them and let me know. I'll keep the Windows package up to date but if anyone wants to take the Linux or OS X side, I'd appreciate it.

Here is the direct download link
http://code.google.com/p/qilang/downloads/list

but you can easily see it at
http://code.google.com/p/qilang/

Hopefully this will help spread Qi to new and interesting places. Let me know if you have any problems with the installer, please let me know.

Until Later...

Tour of Qi 7.2 and 6.2 diff

2007-03-21T23:42:00.000-07:00

Since my computer is still not back up to speed after my crash (I was making backups during the crash. Praise be the Gods of Irony, I hath mended my ways. Smite me no more!), I thought I'd take a quick tour over the differences between Qi 6.2 and 7.2. So fire up your diff browser and join along on this magical ride in CodeLand!

And like any good tour, it starts off with a mystery!

Why on earth is it named Qi 7.2!? I could see going from 6.2 to 7.0 as it now runs on a new Lisp compiler and has some added language features. But I can see no real reason to name it Qi 7.2 other than Mark COULD name it Qi 7.2. Anyway, like any good tour, we now will move on without actually solving the mystery.

Right away, we find the new definition of "no waffle" for the CMUCL compiler. We also come across a great comment quote:

\No waffle from the CMU or CLisp compiler. Speed max, safety min because Qi has a type checker.\

I like telling the compiler, "Speed Max, Safety Min! because I know better than you!" Of course, Qi has to do a lot of work to "know better" than the compiler, but it's every programmers dream to tell the compiler "full optimization, I've got this nailed!"

From here, we find some code to handle the different types of closures on CMU, namely the INTERPRETED-FUNCTION type. It almost makes me want to stop and dig into the difference between FUNCTION and EVAL::INTERPRETED-FUNCTION, but this is a tour so we have to get moving.


(DEFUN fix-closures ()
      #+CMU   (SETQ *closures* '(FUNCTION COMPILED-FUNCTION EVAL::INTERPRETED-FUNCTION))
      #+CLISP  (SETQ *closures* '(FUNCTION COMPILED-FUNCTION))
      #-(OR CLISP CMU) (ERROR "Qi does not recognise this platform ~A" (LISP-IMPLEMENTATION-TYPE)))

Our next bit of action is when we find the brand new curry rules for tuples. If you have noticed, some of my posts contain monster tuples with so many @p's that your eyes almost bleed. Now Qi will turn (@p name x_loc y_loc) into (@p name (@p x_loc y_loc)) for me! I'm already dreaming of the @p's I get to kill with this feature. We would go hunting for them... but it is a .... we'll YOU know.

The system function table lets us know that we should expect 2 new system functions, mlet and new-assoc-type. Like a sign in an amusement park, it entices with future happiness. And then, in a moment, it has passed by.


(define compile_to_machine_code
  Name Rules -> (do (PUSHNEW Name (value *userdefs*))
                          (compile_to_lisp 
                                (put-prop Name lambda (compile_to_lambda 
                                      (compile_to_lambda+ Name Rules))))))

Now we come along and find that compile_to_machine_code stores the name of our function along with a "lambda" property that it keeps the lambda compilation in. It isn't something that you would often think about, but if you end up using property lists with the same name as functions in your code, you would want to know about this.


\Make association between Qi type and Lisp type.\
(DEFUN new-assoc-type (X Y) (PUSHNEW  (LIST X Y) *assoctypes*) 'associated)

And now we come along to something dangerous and FUN! A play with at your peril type of function. You can now create your own match between a Qi type to a Lisp type. Originally, the assoc list only contained things like numbers, strings, symbols, but now you can add your own. Obviously, use this at your own peril as the typechecker will believe anything you tell it. I believe there may be an article on using that in a pathological manner and seeing what happens. But our boat flows on...


  \Params [F X] -> (lisp_code Params [apply F (lisp_code Params X)])   where (element? F Params) \

  \Above changed in 7.1\

  Params [F X] -> [apply F (lisp_code [F | Params] X)]   where (element? F Params)

Here we find that the function call now does not recursively lisp_code on the applied function anymore. This won't change the meaning of the code but perhaps it produces faster code on CMU? Perhaps compiling the apply doesn't matter as the params are already taken care of in X? Tour guides often speculate wildly on their subject matter. I choose not to break with that tradition here.


 \Translate mlet into let.    Works for dotted pairs.\
  (define expand-mlet
     [@p W X Y | Z] -> (expand-mlet [@p W [@p X Y | Z]]) 
     [mlet V W X Y | Z] -> (expand-mlet [let V W [mlet X Y | Z]])
     [mlet X Y Z] -> (expand-mlet [let X Y Z])
     [X | Y] -> (map-dotted-pair expand-mlet [X | Y])
     X -> X)

Yet another gem in 7.2! This will really save on the number of parens in my code. You can now (mlet X 2 Y 3 (+ X Y)) to get 5! The only think I need to implement now is a lambda that does pretty much the same thing. I.e. (/. [ X Y ] (+ X Y)) converts to 2 lambdas in the correct order. You'd think you could do this with a Macro, but you would be wrong. /. is a special form, not to be messed with in any macro. I've tried!

After some boring CMU details that I'll skip over, we find that the typechecker now calls curry_type in a few more places, presumably to handle the new tuple action, but maybe its just for more complete typing in general. But let us not dally, we are nearly finished!

And like any good tour, some couple breaks up during it sending us out with a zoom!


\Modified in 7.1 to allow stops to be embedded in alphanums.\
\I gave up on Qi-YACC! \

(define process-prolog-chars

Apparently, poor Qi Yacc didn't want to parse the input properly. But do not worry, she's still around. And perhaps even she can be cajoled into parsing things correctly with some fancy trickery not yet invented by the human mind. Who knows, it even could be YOOOOUUU!

Please exit the boat carefully and I hope you have enjoyed this Diff Tour of Qi 6.2 and Qi 7.2. We will return to your irregularly scheduled coding posts after a nice clean OS install.

The Real Reason Why Building Software is not like Building Bridges

2007-02-26T07:16:00.000-08:00

I have seen many articles expounding on how software is not like bridge building. They attempt to reason about the problem via poorly formed analogies and often miss the actual critical differences between software development and bridge development. You will see things like the number of bolts and rivets compared to the number of lines of code. You will hear about the size of the software problem space vs. the size of the bridge builder's problem space. But none of these articles has ever hit the nail on the head for me, so I thought I would draw an apt analogy that can help both software programmers and bridge engineers understand each other.

Imagine you are a bridge engineer and have been teleported to an alternate universe to build the Golden Gate Bridge. You have things that look like beams, bolts, and welding torches. You set out to build the bridge and one day your crew finally finishes it. The first traveler gets on the bridge and drives across it, but he winds up in Des Moines, Iowa.

"What happened?" you exclaim! Your crew laughs at the traveler's predicament. "It must be a bork," they say. One of the crew goes out half way on the bridge, turns a bolt 90 degrees clockwise, and shouts back to send another driver across. Another brave traveler, dubbed "beta-tester" for some reason, sets off across the bridge and finds herself in China. The crew laughs heartily and shouts back, "Give it another spin!" With another 90 degree turn, and another brave traveler later, someone actually drives across the bridge into San Francisco as intended! There is much cheering and the sound of the popping of the Champaign floats across the ocean.

Just then, you notice a Volvo trying to drive across. You stare in awe at this strange universe wondering if the Volvo ever managed to get across. You tap one of your crew in the back and ask, "Do you think the Volvo will get to the right place?" He drops both his Champaign glass and his jaw. "VOLVO!!!!" he screams! "No, No, NO!" a crew member exclaims. "Didn't you know your world had Volvo's?" you ask. "Of course," he replies, "but we didn't think anyone would be foolish enough to try to drive it across the bridge!"

Flabbergasted, you wait for the inevitable. Half way across, the poor Volvo starts to float off the ground. It starts to spin over and over again. Horrified, you ask, "Can we make it so we can allow Volvos to drive across after we rescue that poor soul?" "Certainly," comes the reply of the crew chief, "but we'll have to raise the entire bridge by another 4 feet. We could either lift it from the bottom or just put an extra 4 feet of concrete on the surface of the bridge." You choose the latter option, saddened by the fact that your beautiful bridge now has a thick white coat of concrete to accommodate the simple Volvo.

Thinking your task has finished, you look forward to running far, far away from this universe and back into ours. You then notice 2 cars starting to drive across the bridge in tandem. A familiar feeling of dread fills you as you stammer out, "What happens if the bridge is used in parallel?" "RUN!" comes the screaming reply. No longer questioning the logic of this world, you take off. Looking back, you see a single bolt fall from the top of the bridge. As it falls, it begins to absorb the bridge itself. More and more of the bridge falls INTO the bolt. The cars, bolt, and bridge are lost forever. That is until the crew chief comes over to where the bridge was and pushes a button at the edge of the road. The bridge instantly reappears. He also posts a sign, "No driving on the bridge in parallel."

Before finally finishing with this world, you turn to ask your crew how this universe works. "It's quite simple," comes the reply. "Any bolt, beam, or other bridge part can be a bridge to any other part of the universe. It is even possible for a part to become a black hole leading to nowhere, as you saw." "Why do you build bridges then?" you ask. "We build bridges for the same reason you build bridges, because they are useful. We cannot help the fact that our universe is very strange. We envy your bridges that always lead to the same place and your parts that do not become black holes. From what you told us of your world, your software builders are in the same situation as us. Give them our sympathy and our camaraderie." With that, you return home with a far greater appreciation of what your programmer friends have to go through.

Thus ends our journey to the alternate dimension. Unfortunately for software developers, this place actually exists for us. The Halting Problem shows that we can never be certain of any result about any computation. It may run properly, it may become an endless loop, or it may give the completely wrong result. Adding concurrency adds on even more uncertainty into the situation. And we can PROVE this logically. There is no escape from the Halting Problem weirdness. Every single line of code added may blow up the bridge, dump you in China, or create a black hole.

THAT is the real bridge to programmer metaphor. And it is why software development will always be hard.

Now to help you all remember allow me to coin Gleason's Law:

"Any sufficiently complex software is indistinguishable from magic."

Monads in Qi

2007-02-05T10:34:00.000-08:00

It is hard to even begin to learn the cutting edge of functional language theory these days without talking about monads. In languages running in a purely functional manner, monads offer a way of dealing with the outside environment in a safe and controlled manner. In a pure environment, monads provide us a way to carry data computations via pure functional composition and still have computations that happen "on the side." A lot of research into functional languages requires a solid understanding of monads and thus to apply their results to the Qi programming language, I'll define a few monad operations here and define a type theory that can handle the list monad

Since you can find a wide variety of monads for the language Haskell, I will start by describing monads in Haskell and use that to define representations inside of the Qi language. Basically, a monad is a type that defines two operations. The operations are "lift" and "pipe". In Haskell, they are often called "return" and "bind" respectively. As long at the two functions hold the following identities, we can consider the type to be a monad.

Here is a definition of the rules a monad must follow in a pure version of scheme.


   (pipe (lift x) f)   = (f x)
   (pipe m lift)       = m
   (pipe (pipe m f) g) = (pipe m (lambda (x) (pipe (f x) g)))

In Haskell, the Monad m class is defined by


class Monad m where
   return :: a -> m a
   (>>=)  :: m a -> (a -> m b) -> m b

We can see that return "lifts" a value of type a into the monad class m a. Bind takes in a monad of type "a" and a function that takes in a value of type "a" and gives a monad of type "b". Bind then returns to us a monad of type "b" where the monad "a" has been transformed by the function into a monad of type "b". Once we have these two functions working as defined, we have a monad. Notice that we have not defined these functions yet. Haskell allows us to define a higher order type that we promise that all implementations of the type will have the listed functions and they will match the given type signatures. These sorts of definitions are not as easy in Qi, yet.

One of the basic monad types in Haskell is the list monad. We define list monads as having type Monad [] and we can make a set of functions that follow the monad laws over Monad []'s.


instance Monad [ ] where
   (x:xs) >>= f = f x ++ (xs >>= f)
   []     >>= f = []
   return x     = [x]

Let us rewrite these rules in Qi.


(define bind
[] _ -> []
[X | Xs] F -> (append (F X) (bind Xs F)))

(define return
X -> [X]  )

Well that was easy! Let us try out this new monad... We'll take a list of [10 20 30] and a function that takes an X and returns [X X+1] and give it to bind to see what it does with it.


(2-) (bind [10 20 30] (/. X [ X (+ X 1) ] ) )
[10 11 20 21 30 31]

So far, so good. Let us check the monad laws to see if this version follows those laws. Law 1 says that (bind (return X) F) == (F X)


(5-) (define f X -> [ X (+ X 1) ] )
f

(6-) (bind (return 2) f)
[2 3]

(7-) (f 2)
[2 3]

Law 2 says (bind Monad return) == Monad


(8-) (bind [ 4 5 6] return)
[4 5 6]

Law 3 says that (bind (bind Monad F) G) = (bind Monad (/. X (pipe (F X) G)))


(9-) (define g X -> [ (+ X 33) (+ X 44) ] )
g

(10-) (bind (bind [10 20 30] f) g)
[43 54 44 55 53 64 54 65 63 74 64 75]

(11-) (bind [10 20 30] (/. X (bind (f X) g)))
[43 54 44 55 53 64 54 65 63 74 64 75]

So we have proven that our monad list does in fact honor the monad laws. However, we are not running the type checker in Qi on this problem, so the monad we get is the same one that we can get in any functional language. We have to wait until runtime to see the error of the following attempt at using a monad.


(14-) (bind [10 20 a] (/. X (bind (f X) g)))
1+: a is not a NUMBER

So now the question becomes, can we get a monad into the TYPED version of Qi. Firstly, we must note that Qi has no notion of polymorphic type overloading. Hence we cannot easily make a general purpose "bind" operator that all monads can use. We also should note that the type checker treats a polymorphic list as a special case, and thus we cannot perform a direct translation like the one from Haskell. In some way, we will have to contain our lists in another type.

Let us take the simplest translation. If something is of type (list A) then we can make a monadic list type of (monad list A) via the following sequent rules.


(datatype monad

X : (list A);
=====
[X] : (monad list A);

)

Monadic lists are simply lists inside of a container list and any list in a container can be a monad list of that type. We should read this as saying, "We can construct monads from lists by adding a list around it and we can construct lists from monads." We note that Qi allows you to go back from a monadic representation to the list based one as long as you properly use the type. Unfortunately, Qi has no notion of modules so we cannot seal off this behaviour from other functions in our code.

Continuing, we will define some helper functions to allow us to manipulate the monad data structure inside the instance functions. Of course, Qi has no notion of either class or instance and allows us to pull lists from monads. But if we ignore these quirks for the moment, we can define a reasonable monad list type that works. I include a constructor function "list_monad" and a few internal data access helpers.


(define list_monad
{ (list A) --> (monad list A) }
X -> [X] )

(define m_head
{ (monad list A) --> A }
X -> (head (get_list X)))

(define m_tail
{ (monad list A) --> (monad list A) }
X -> [ (tail (get_list X))] )

(define m_cons
{ A --> (monad list A) --> (monad list A) }
X [Xs]-> [(cons X Xs)])

(define join
{ (monad list (monad list A)) --> (monad list A)}
  Xs              -> (join-help [[]] Xs))

(define join-help
{ (monad list A) --> (monad list (monad list A)) --> (monad list A) }
Final [[]] -> [ (reverse (get_list Final)) ]
Final ML -> (let XRest (m_tail (m_head ML))
  (if (= XRest [[]])
             (join-help (m_cons (m_head (m_head ML)) Final)
                 (m_tail ML))
             (join-help (m_cons (m_head (m_head ML)) Final)
                              (m_cons (m_tail (m_head ML)) (m_tail ML))) )))

Our m_ functions and join properly deal with getting (list A)'s from their containers and putting them back in. Join has to take the job of flatten and check for the end of a list and if we find it, drop it from the "Final" list. This accounts for the if statement in the function. It obviously makes heavy use of the data manipulation functions which lowers legability. We can read it as saying, "Take the first element head of the list (remember that we have a monad list of a monad lists here) and put it on the final list. Then take the rest of that head list and put it back on the processing queue. The Final output list is built in reverse order so we are forced to reverse the computation at the end of the join. Not pretty, but it works for the purpose of monad construction.

Now we are in a position to define "bind" and "return" as before.


(define bind
{ (monad list A) --> ( A --> (monad list B)) --> (monad list B) }
XS F -> (join [(map F (get_list XS)) ]))

(define return
{ A --> (monad list A) }
X -> [[X]]
)

Note that we basically take the list out of the monad container and apply normal list functions to it, wrapping it up back in the monad container when we return.

Testing it out gives:


(14+) (bind (list_monad [10 20 30]) (/. X (list_monad [X (+ X 1)]) ))
[[10 11 20 21 30 31]] : (monad list number)

And our monad type is certainly not a list


(31+) (head (bind (list_monad [4 5 6]) return))
error: type error

Now let us assure ourselves that our monad list is polymorphic to type A. We now define a fractal symbol function f.


(36+) (define f
{ symbol --> (monad list symbol) }
X -> (list_monad [ x o x]) where (= X x)
_ -> (list_monad [ o o o]))

And let us use it with our monad functions


(37+) (bind (return x) f)
[[x o x]] : (monad list symbol)

(38+) (bind (bind (return x) f) f)
[[x o x o o o x o x]] : (monad list symbol)

(39+) (bind (bind (bind (return x) f) f) f)
[[x o x o o o x o x o o o o o o o o o x o x o o o x o x]] : (monad list symbol)

So there you have it, a very simple, poorly performing basic list monad of polymorphic type A in the Qi Programming Language. Feel free to offer any questions or criticism that you have. Thanks for reading.

Computing During Typing

2007-01-26T01:18:00.000-08:00

I'm going to take another dive here into the Qi type system to give an idea of the expressive power possible in it. Qi has a fully Turing capable type system and that means that we should be able to express truths about natural numbers directly in the form of types. The computation of the truth will happen at compile time! For the purposes of this exercise, we will define "truth" as having matched to type "has_truth" and we will define falsehood as having raised a type_error or returning _|_ as represented by an infinite loop.

We will start by encoding the Peano axioms into a Qi type. We will represent the natural numbers and truth as Qi Types. Then we will define the basic rules of arithmetic and describe the basics of everybody's favorite commutative semigroup. Finally, we will discuss falsehood and how Qi handles it, along with infinite loops, blown stacks, and some other real world programming issues.

As a quick refresher for those of you not well versed in sequent notation, you can think of them as saying "If the top parts have these types, THEN the bottom construction is valid for the labeled type." Or alternatively, you can think of them as saying, "If we have a type that looks like one on the bottom, AND if we can take the components of it and prove them of types on the top, THEN we can type the bottom element as labeled." Now I'm not so certain my explanation helps...

For Peano's first axiom, let us define the natural numbers as 0 and its successors labeled as [suc X] where X is a natural number. We include 0 as a convenience here, but it would be possible to define the type without it. We also include the sixth axiom here, namely the idea of successors which are represented as nested lists.


___
zero : nat;

X : nat;
=======
[suc X] : nat;

Taking his second axiom, let us ensure that every natural number is equal to itself. Note that this imports the notion of lexical equivalence from Qi into our type theory, but as = will always return, we can be assured that it is not going to cause any indefinite delay in the type theory. And it is in equality that we wish to test for truthhood, so we will need to define the type "has_truth" here.


if(= A1 A2)
A1 : nat ; A2 : nat;
===========
[ A1 = A2 ] : has_truth;

In effect, we are saying that equal things "have truth." Alternatively, I could have named the type is_equals. Read it however you like.

Peano's third axiom will end up causing no end to our headaches inside the Qi type system while giving us our expressiveness at the same time. It says A = B iff B = A.


[ A = B ] : has_truth;
======
[ B = A ] : has_truth;

We can drop the forth axiom due to us using a 2 sided system. Then using the fifth we find that if a = b is true and b is a natural number then a is a natural number. Given that A = B is true and B is a natural number, we can prove A is a natural number.


[ A = B ] : has_truth; B : nat;
______
A : nat;

Having already listed the sixth earlier, we turn to the seventh Peano axiom, the equality of successors. This axiom, unlike the third axiom, really simplifies the job that the type checker has to do. I like the seventh Axiom. It's not like that mean, mean third axiom. It makes me wonder how much math do you have to do in order to find some of Peano's axiom's more "friendly" than others. I see a Psych 101 experiment there. *grin*


[A = B] : has_truth;
_____
[[suc A] = [suc B]] : has_truth;

With the setup I used, we have no way of returning "not" so we have trouble with Peano's eighth axiom. It is sufficient to point out that we have imported the equality operator from Qi for which this property holds. So Axiom 2's code is our key here. And for this code, we can obviously leave out the ninth.

On to the group operator +...

We define a new type of number that is the result of addition.


A : nat ; B : nat;
========
[ A plus B ] : nat ;

Now we can create the zero-to-identity rule which states that nothing changes when we add 0 to other numbers.


A : nat;
=======
[A = [ A plus zero ]] : has_truth;

Now we must create the plus-to-successor rule that allows us to define addition over other numbers. We state that a + Sb = S ( a + b).


A : nat ; B : nat;
[ C = [suc [ A plus B] ] ] : has_truth;
====
[ [A plus [suc B]] = C ] : has_truth;

Note that here we actually use an assignment to a variable to introduce a new equation. The best way of thinking of this equation is from the bottom up. If we are trying to find out the truth of an equation with a plus in it which does NOT have a zero, then we must find a new equation C that has one of our numbers subtracted by one, and take the successor of THAT.

The real trick is to notice that C is a completely new construction created by our type system. The top part of the equation acts as a hypothetical that the proof checker then tries to solve. Peano's beloved seventh rule helps us find computable theorems even with an automated prover.

So what do we get for all this? We get a type that can perform numerical computations at compile time!

Lets try 0 = 0


[ zero = zero ] : has_truth
______________________________________________ 9 inferences
?- [zero = zero] : has_truth


>
______________________________________________ 62 inferences
?- zero : nat


>
______________________________________________ 112 inferences
?- zero : nat


>
[zero = zero] : has_truth

So far, that went swimmingly! Lets try something harder. S( 0 + 1) = 2.


(8+) [ [suc [ zero plus [ suc zero] ]] = [suc [ suc zero]] ] : has_truth
______________________________________________ 9 inferences
?- [[suc [zero plus [suc zero]]] = [suc [suc zero]]] : has_truth


>
______________________________________________ 71 inferences
?- [[zero plus [suc zero]] = [suc zero]] : has_truth


>
______________________________________________ 138 inferences
?- zero : nat


>
______________________________________________ 188 inferences
?- zero : nat


>
______________________________________________ 238 inferences
?- [[suc zero] = [suc [zero plus zero]]] : has_truth


>
______________________________________________ 300 inferences
?- [zero = [zero plus zero]] : has_truth


>
______________________________________________ 363 inferences
?- zero : nat


>
[[suc [zero plus [suc zero]]] = [suc [suc zero]]] : has_truth

That worked great! We can see the proof tool using Peano's seventh like it was born to formalize! (Being a lambda calculus, it was. *grin*)

Lets take on 3 + 2 = 5


(9+)
[ [ [suc [suc [suc zero]]] plus [suc [suc zero]] ] =
[suc [suc [suc [suc [suc zero]]]]] ] : has_truth

This gives us has_truth in 1081 inferences. The type checker does 5 = 3 + 2 in 363 steps.

I mentioned that I'd wrap up on some real world issues. Since the type checker can insert any rule it needs to and search for ways to make the theorems work, we have a Turing complete type system. And this means that some things will never complete their type checking. So we have to explicitly deal with the _|_ type in some manner to get sensible behaviour out of the system.

For example, let us take Peano's eighth axiom of zero != [suc zero]. If we ask this type theory about [zero = [suc zero]] : has_truth, it will have to either fail or return _|_. Unfortunately for us, the need for Peano's third axiom dooms us to get a _|_ style value back from the type checker, i.e. it never completes.


>
______________________________________________ 222 inferences
?- [[suc zero] = zero] : has_truth


>
______________________________________________ 293 inferences
?- [zero = [suc zero]] : has_truth

This particular example is an area where the Qi type checker should probably understand that calling the same definition that you just called and failed to type before is a mistake. But any automated system will only recognize a small subset of these sorts of errors, so Qi's failure to type_error here is forgivable in these pathological types.

So typing can blow the stack, (as in this case), or it can fail to type raising a type_error. Either of these we can use as falsehoods. If we wanted to extend the system further, we could encode negation into the system and have the ability to return True, False or a _|_ style answer.

I hope this sheds some light into the Qi type system. There's a lot more you can do with it obviously. Hopefully you enjoyed the article and hopefully I can find time to post more.

Best wishes,

Qi Macros and Type Patterns

2006-05-16T22:27:00.000-07:00

Taking a step back to the Magic Prime Type, we find that the pattern that we used to generate the prime type may be useful to encapsulate in some manner. The pattern goes as follows: If you have a base class like number, and you have a derived class such as prime, then you can create these "prime like" classes as long as you have a function that returns true for the basic and derived type. Simply put, if we could just swap different lexical elements into our prime datatype constructor, we could have a useful piece of code for creating exotic types such as the “even” type or perhaps the “catalan” type. Obviously, when we talk about placing lexical elements inside of code, we are talking macros!

So what would the Lisp-like macro look like for our “subtype-with-test” function? Something like the following, only better.


(DEFMACRO subtype-with-test ( BaseType NewType BaseTest NewTest)
`(datatype ,NewType
   if(and ( ,BaseTest X ) ( ,NewTest X ) )
   ____
   X : ,NewType ;

   ___
   ( ,NewTest X) : verified >> X : ,NewType ;

   ( subtype B A ) ; X : B ;
   ___
   X : A;

   ___
   (subtype ,NewType ,BaseType);
 )
)

However, if you try to input that into Qi, you’ll find it will not make a compiling as something seems to happen to the ;. We need to use the "macroexpand" function mentioned in Appendix B of FPIQ language book. Fortunately for us, the syntax makes our final Qi macro a bit easier to read than the lisp version. We first create a pattern that looks like a function call that matches our macro. We’ll name it the same as above and it will take the same arguments.


(define macroexpand
  [subtype-with-test BaseType NewType BaseTest NewTest] ->
  [datatype NewType
    if[and [ BaseTest X ]
           [ NewTest X ]]
    ______
    X : NewType ;

    ____
    [ NewTest X ] : verified >> X : NewType ;

   [ subtype B A ] ; X : B ;
   ___
   X : A;
   
    ___
   [ subtype NewType BaseType ]; ]
   X -> X
)

And that’s all there is to it! Just remember to make sure to include the X-> X pattern at the bottom. Every single token receives a macroexpand so we need to ensure that it works as intended for all but our special "subtype-with-test" macro. Note that the pattern match serves as our macro definition. We define it in no other place.

Now doing the following creates a brand new type!


(subtype-with-test number prime integer? prime?)

We should note that the macroexpanded "subtype-with-test" prevents the evaluation of the 4 inputs. So we find the typical problem with variable capture. We don’t have the ability to name our classes X, A, or B!!! *laugh* Not a big loss, but we can modify the code and learn to deal with variable capture. We do this in the same way we deal with it in Lisp, namely gensyms.


define macroexpand
  [subtype-with-test BaseType NewType BaseTest NewTest] ->
  (let X (gensym "Temp")
  (let A (gensym "Temp")
  (let B (gensym "Temp")
  [datatype NewType
    if[and [ BaseTest X ]
           [ NewTest X ]]
    ______
    X : NewType ;

    ____
    [ NewTest X ] : verified >> X : NewType ;

   [ subtype B A ] ; X : B ;
   ___
   X : A;
   
    ___
   [ subtype NewType BaseType ]; ] )))
   
   X -> X
)

One important point to note is that the "Temp" (or whatevever you want to name your gensym) must start in UPPER CASE! Otherwise, Qi won’t be able to tell it is a variable!

Qi does warn about these sorts of issues however, if you see the free variable warning in a macro, capture them with gensyms to turn this sort of output …


(0-) (load "test/pmacro2.qi")
======> Warning:
the following variables are free in macroexpand: B; X; A;


WARNING:
DEFUN/DEFMACRO: redefining function macroexpand in D:\tools\Qi 6.2\startup_qi.tx
t, was defined in D:\tools\Qi 6.2\Install Qi\Qi 6.3.txtmacroexpand

Real time: 0.0156303 sec.
Run time: 0.015625 sec.
Space: 185740 Bytes
loaded

into this much nicer output…


(0-) (load "test/pmacro3.qi")

WARNING:
DEFUN/DEFMACRO: redefining function macroexpand in D:\tools\Qi 6.2\startup_qi.tx
t, was defined in D:\tools\Qi 6.2\Install Qi\Qi 6.3.txtmacroexpand

Real time: 0.0312606 sec.
Run time: 0.03125 sec.
Space: 194036 Bytes
Loaded

Note the lack of compiler warnings about free variables. However it will always warn you about redefining macroexpand. Of course, since we are defining VARIABLES in the datatype, no real variable capture can happen. Our macro requires lower case symbols to even operate. But this example shows how to avoid the issue in the odd case where you want to make a macro that you can define different variable names inside it. (Can anyone think of a good reason to do this?)

So let us try this new macro out! We’ll create an even test and create a new type called "even" that can only type to actual even numbers.


(12+)  (define even?
{ number --> boolean }
X -> (integer? (/ X 2)) )
even? : (number --> boolean)

(13+) (subtype-with-test number even integer? even?)
even : unit

(14+) 3 : even
error: type error

(15+) 4 : even
4 : even

(16+)  100 : even
100 : even

(17+) 101 : even
error: type error

I’d say that is an impressive job for one line of code! Let me know what you think!

Treaps in Qi

2006-05-15T21:21:00.000-07:00

Delving back into the type system for this post, I thought I would take on the strange and wonderful Binary Search Tree known as the treap. For those that don’t know, a treap is a binary search tree that has a “priority” element attached to the key. It uses the random priority to ensure balancing of the tree. It does this by ensuring the tree is in binary search tree form with respect to the keys, and in heap form with respect to the priorities. We will create a simple type of string based treap in Qi and perhaps extend it to a more general version if I find the time to finish it. *grin*

The datatype for treap can be either list based or tuple based. I’ll begin with the tuple version as it shows off a bit more of the power of Qi pattern matching, but a list version would be more readable. We can signify empty leaves with the null list in either case.


_______
[] : treap;

And now we will create the recursive type. It takes a key and a priority and has a left branch and a right branch. Using the tuple to define the leaves means we place the key and priority in their own tuple and use that as the first element. Then we can put the left and right branches in their own tuple as the second element of our treap node. We’ll use the ever handy left/right sequent operator to ensure we can prove things about treaps using the datastructure only and typing the internal parts.


Key : string; Priority : number; LeftTreap : treap; RightTreap : treap;
===============================
(@p (@p Key Priority) (@p LeftTreap RightTreap)) : treap;

Now when we wish to insert a key into the treap, we must first make a random number to assign it for heap priority.


(define treap_insert
{string --> treap --> treap}
K Tree -> (treap_insert* K (- (random 40000000) 20000000) Tree))

Now the fun begins. The base case seems simple enough, just make a treap that looks like the above definition but has LeftTreap and RightTreap set to [].


(define treap_insert*
{string --> number --> treap --> treap}
K P [] -> (@p (@p K P) (@p [] []))

Now it could be that we are trying to insert an element that we already have. If so, we simply return the treap we had to begin with.


K P (@p (@p K* P*)
  (@p L R))
-> (@p (@p K* P*) (@p L R)) where (= K K*)

Note that our pattern matched definition is well typed. L is a treap and R is a treap. K is a string and P is a number. We match the new key and priority as K and P. We match the treap node’s priority as K* and P* and the branches as L and R. If you mess up using them in your definition, the complier complains loudly.

Now we know the K is not equal to the current treap node, if it is less than the tree node we insert it somewhere on the left tree. AFTER we do this, then we order the treap by heap priority, preserving the BST ordering as we move our way up the tree. We’ll use the same pattern as the element above.


K P (@p (@p K* P*)
  (@p L R))
-> (let Tree (@p (@p K* P*)
             (@p (treap_insert* K P L)
     R))
    (if (> P* P)
   (rotate_right Tree)
   Tree))

    where(str-lt K K*)

So if our new priority is less than the old one, we move it up the treap. That makes it reverse heap ordering, but we are not splitting hairs here. *grin*

So now we need to find out how to rotate a treap node up a treap. Rotate right takes the L branch and finds its left and right treaps and their keys. It then puts the left L treap as the current left, uses the left treap node’s key/priority as the current key/priority and makes a new right treap with the original left nodes right hand treap paired with the old right hand side, placing the old key/priority there. The code below serves as our heapify.


(define rotate_right
  {treap --> treap}
(@p (@p Key Priority)
    (@p (@p (@p K* P*)
       (@p A1 A2))
   B))

-> (@p (@p K* P*)
  (@p A1
      (@p (@p Key Priority)
   (@p A2 B)) ))
    
)

Pattern matching makes the change short and sweet. Type checking ensures that we have a valid treap at the end.

Now we can finish our definition of treap_insert with the right hand insert


K P (@p (@p K* P*)
  (@p L R))

-> (let Tree (@p (@p K* P*)
        (@p L
     (treap_insert* K P R)))
    (if (> P* P)
   (rotate_left Tree)
   Tree))

We can make a rotate_left along the lines of the rotate_right


(define rotate_left
{treap --> treap}
(@p (@p Key Priority)
    (@p A
        (@p (@p K* P*)
       (@p B1 B2))))       -> (@p (@p K* P*)
      (@p
         (@p (@p Key Priority)
      (@p A B1))
          B2))
)

All we need to do now is define a string less than function str-lt that compares strings. And here we run into a problem. We have no type safe way of comparing strings in Qi. So we’ll have to modify Qi to know about our version of the string compare function. We’ll build it from the ground up by giving CHAR-CODE a type. In deference to Haskell, let us name the function “ord”.

You can patch it with


42c42
<>    occurrences occurs-check or output prf print profile profile-results prooft
ool provable?
47c47
<>    track tuple? undebug unprf union unprofile untrack value version
1527c1527
<>     number? 1 occurs-check 1 occurrences 2 or 2 prf 1 print 1 profile 1 profil
e-results 1 prooftool 1
1586,1587c1586
<     (boolean --> (boolean --> boolean)) ord (character --> number)
<> B) --> (A --> B))
---
>     (boolean --> (boolean --> boolean)) prf ((A --> B) --> (A --> B))
2397,2398d2395
< (DEFUN ord (x) (CHAR-CODE x)) <> string --> boolean}

But it would help to simply search for the word “difference” as it is an internal function used only 3 times in the program outside its own definition and add the code yourself to learn how. There you find the arity list that you must add the ord function too and the type list where you specify the type. Then you can add the DEFUN for ord by the other system function defuns. Run the installer and you will get a version of Qi that has our “ord” function.


--- EDIT ---

I'm adding a much better way of doing this in Qi that Mark pointed out on the mailing list.

Lisp contains a function STRING<, so if you want to bring this into Qi,
then the following will do it.

(0-) (define string<
    X Y -> (if (empty? (STRING< X Y)) false true))
======> Warning:
the following variables are free in string<: STRING<;
string<

(1-) (newfuntype string< (string --> string --> boolean))
string<

(2-) (tc +)
true

(3+) string<
string< : (string --> (string --> boolean))

(4+) (string< "ghgjj" "ghhhg")
true : boolean 

--- EDIT END ---

Now we can define our string less than function, “str-lt”.


(define str-lt
  {string --> string --> boolean}
  S1 S2 -> (str-lt* (explode S1) (explode S2)))

(define str-lt*
 {(list character) --> (list character) --> boolean}
  [] _  -> false
  _  [] -> true
  [X |_] [Y | _] -> true where (< (ord X) (ord Y))
  [_ |L1] [_ | L2] -> (str-lt* L1 L2)
)

And now we have a working, input-only treap. I think at this point I will take a break and perhaps return the program efficiency and changing of the syntax in another article. Let me know of any questions or comments you have so far please!

Here is the full file. I'll create a place to download my code sometime soon.


(datatype treap

  _______
  [] : treap;


  Key : string; Priority : number; LeftTreap : treap; RightTreap : treap;
  ===============================
  (@p (@p Key Priority) (@p LeftTreap RightTreap)) : treap;
)


(define treap_empty?
  { treap --> boolean }
  Tree -> true where (= Tree [])
  Tree -> false
)

(define rotate_left
  {treap --> treap}
  (@p (@p Key Priority) 
      (@p A
          (@p (@p K* P*)
       (@p B1 B2))))       -> (@p (@p K* P*)
      (@p 
         (@p (@p Key Priority)
      (@p A B1))
          B2))
)

(define rotate_right
    {treap --> treap}
  (@p (@p Key Priority) 
      (@p (@p (@p K* P*)
       (@p A1 A2))
   B))
 
  -> (@p (@p K* P*)
  (@p A1
      (@p (@p Key Priority)
   (@p A2 B))
      ))
)

(define treap_insert
 {string --> treap --> treap}
 K T -> (treap_insert* K (- (random 40000000) 20000000) T))

(define treap_insert*
  {string --> number --> treap --> treap}
 K P [] -> (@p (@p K P) (@p [] []))

 K P (@p (@p K* P*)
  (@p L R))  
 -> (@p (@p K* P*) (@p L R)) where (= K K*)

 K P (@p (@p K* P*)
  (@p L R))  
 -> (let Tree (@p (@p K* P*)
               (@p (treap_insert* K P L) 
     R))
      (if (> P* P)
   (rotate_right Tree)
   Tree))
    
    where(str-lt K K*)

 K P (@p (@p K* P*)
  (@p L R)) 

 -> (let Tree (@p (@p K* P*)
        (@p L
     (treap_insert* K P R)))
      (if (> P* P)
   (rotate_left Tree)
   Tree))
)


(define str-lt
  {string --> string --> boolean}
  S1 S2 -> (str-lt* (explode S1) (explode S2)))

(define str-lt*
 {(list character) --> (list character) --> boolean}
  [] _  -> false
  _  [] -> true
  [X |_] [Y | _] -> true where (< (ord X) (ord Y))
  [_ |L1] [_ | L2] -> (str-lt* L1 L2)
)

Qi Optimization and Catalan Fun!

2006-05-08T22:17:00.000-07:00

We start this week by delving a bit into number theory and seeing what we can accomplish with Qi. We will start with a simple approach to the problem and then perform some optimizations on our program. We will use pattern matching, backtracking, and arrays to enhance the performance of our sequence in order to better understand Qi. Hopefully, this process will show the powers of Qi to search complicated number spaces and what limitations we run into when using Qi in general as well.

Let us start with the empty string, "". We can define this as 0. If we put a pair of parenthesis around the empty string, we get the new string "()". We can call this string 1. Putting a pair of parenthesis around the 1 gives us "(())" or what we will call 2. Alternatively, we can concatenate 1 to 1 to get another version of the string, "()()". Doing this for 3 gives us "((()))" , "()()()" , "(()())", "(())()" and "()(())". These obviously represent basic addition facts if you think of concatenation as + and the parenthesis as + 1. Or we can think of these strings as the number of ways we can parenthesize a string of length N. We have defined these strings via 2 basic operations, either by interning previous strings with parenthesis or by either concatenation be it left-handed or right-handed. This feels reminiscent of the S and K combinators, but perhaps that’s a topic for another time.

So from that description, we can devise a simple Qi program to output those strings. We will call this function get-cstrings. The base case is 0 and we define it as the empty string.


(define get-cstrings
0 -> [""]

Now for the recursive case, we either perform the "interning" operation by putting a pair of parentheses around the previously created number, or by taking any previous number combination that adds to our number and concatenating them together. We define the intern function as intern-all which takes a list of strings and interns each string. We also define the left and right concatenation function as lr-apply. It takes in the interned strings and adds the concatenation strings to it. This gives us the full function definition as follows.


(define get-cstrings
  0   -> [""]
  N   -> (let NewList (intern-all (get-cstrings (- N 1) ))
           (lr-apply N NewList))
)

Turing to intern all, we need to take a list and add the parentheses around each element. So we use map to apply a function across the list. The function should take a string, and add parentheses around the front and back. Using this opportunity to apply the Lisp underbelly of Qi seems fun at this point, and gives us more to optimize later. So we take the string, turn it into a list, append the parentheses, and then turn it back into a string.


(define intern-all
  Xs -> 
       (map
          (/. Elem 
             (COERCE (append [ #\( | (COERCE Elem LIST) ] [ #\) ] ) STRING)) 
          Xs
       )
)

Turing our attention to lr-apply now, we note that it walks from 1 up to n-1, forming new strings from pairs of older strings by concatenating them to each other. So we will start with lr-apply


(define lr-apply 
  0 Xs  -> Xs
  N Xs -> (lr-apply* 1 (- N 1) Xs))

And now we need to define the recursive lr-apply* that creates these strings. It takes in the left number and the right number, along with the strings we have built so far. It adds the new strings to the final list. When the right number becomes greater than the left number, we stop. Using the helper function lr-work, we try the following definition.


(define lr-apply*
  L R Final ->
   (let A (get-cstrings L)
   (let B (get-cstrings R)
        (lr-apply* (+ L 1) (- R 1) (lr-work A B Final))))
    where (>= R L)
  _ _ Final -> Final
)

The lr-work function takes the left list of strings and the right list of strings and combines them and adds them to the final list. It uses a helper function pair-this to concatenate an element to each element of the second list. If we had access to the Haskell prelude, we could define this more concisely. You can check the google group for a beginning implementation.


(define lr-work
 [] _ Final  -> Final
 [X | Xs] Ys Final -> (lr-work Xs Ys (pair-this X Ys Final))
)

(define pair-this
  _ [] Final -> Final
  X [Y|Xs] Final -> (pair-this X Xs (make-ap-pair X Y Final))
)

Finally, we have a function called make-ap-pair that takes 2 strings and returns their left and right concatenation. It uses a helper function named give-unique to ensure that the element has not already been placed in the list. We’ll use the Lisp function concatenate instead of any Qi functions.


(define make-ap-pair
 L-num R-num Xs -> (let AfterLeft (give-unique [(CONCATENATE STRING L-num R-num)] Xs)
                           (give-unique [(CONCATENATE STRING R-num L-num)] AfterLeft))
)

(define give-unique
  []  Xs             -> Xs
  [X | Left]  Xs  -> (give-unique Left Xs) where (element? X Xs)
  [X | Left ]  Xs  -> (give-unique Left [ X | Xs ])
)

Running this gives:


(2-) (get-cstrings 0)
[""]

(3-) (get-cstrings 1)
["()"]

(4-) (get-cstrings 2)
["()()" "(())"]

(5-) (get-cstrings 3)
["(())()" "()(())" "()()()" "(()())" "((()))"]

This function obviously grows the list very quickly. Look at the following.


(6-) (LENGTH (get-cstrings 3))
5

(7-) (LENGTH (get-cstrings 4))
14

(8-) (LENGTH (get-cstrings 5))
42

(9-) (LENGTH (get-cstrings 6))
132

(10-) (LENGTH (get-cstrings 7))
429

(11-) (LENGTH (get-cstrings 8))
1430

(12-) (LENGTH (get-cstrings 9))
4862

And c-strings 9 starts to take some noticeable time on my personal box.


(13-) (time (LENGTH (get-cstrings 9)))

Real time: 4.984375 sec.
Run time: 4.953125 sec.
Space: 3335576 Bytes
GC: 6, GC time: 0.0 sec.4862

(14-) (time (LENGTH (get-cstrings 10)))

Real time: 63.984375 sec.
Run time: 63.203125 sec.
Space: 12635520 Bytes
GC: 19, GC time: 0.0625 sec.16796

Obviously, we want to do better. So let us note that the function calls the previous function many times. If we memorize the array, we can find the previous runs with no difficulty. We will use a global array to hold the strings up to 10 named *clst*. We use backtracking to check to see if we already have memorized the result, if not, we compute it.


(define get-pstrings
  0   -> [""]
  N   <- (get-array (value *clst*) [N] #\Escape)
  N   -> (append (intern-all (get-pstrings (- N 1)) []) (lr-apply N []) ) where (> N 10)
  N   -> (let NewList (intern-all (get-pstrings (- N 1)) [])
         (let LrList (lr-apply N [])
             (put-array (value *clst*) [N] (append NewList LrList) )))
)

We can change the intern-all to make more sense and run much faster. Map ends up being slower than simply defining it recursively.


(define intern-all
 [] Out -> Out
 [X | Xs] Out -> (intern-all Xs [(CONCATENATE STRING "(" X ")") | Out] )
)

These simple changes gives us twice the performance.


(10-) (time (LENGTH (get-pstrings 9)))

Real time: 2.53125 sec.
Run time: 2.515625 sec.
Space: 730696 Bytes
GC: 2, GC time: 0.015625 sec.4862

(11-) (time (LENGTH (get-pstrings 10)))

Real time: 33.609375 sec.
Run time: 33.265625 sec.
Space: 2969960 Bytes
GC: 4, GC time: 0.03125 sec.16796

Many more obvious improvements can be made, but that suffices to show how you can flesh out a correct answer then modify it for efficiency.

Of course, if you took this sequence of integers and search for them you’ll find that this is a well known sequence called A000108, Segner numbers, or more often Catalan numbers.
Our favorite number list has the following interesting definition.

a(n) = binomial(2n, n)-binomial(2n, n-1)

We can easily understand how the binomial(2n,n) is part of the result, as we have strings of N left parentheses and N right parentheses. We must choose equal pairs of parentheses so we have N as the bottom element of the function. However, we must remove the unbalanced parenthesis so we take out the incorrect elements via subtracting the number of strings that are "unbalanced" or one off of balanced. Hence we find the binomial (2n, n-1).

However, if we think about this problem as we have programmed it above, we can come up with an equivalent definition that may help us understand the binomial function. In the program above, it takes the a(n-1) and interns each element, returning the same number. It then builds lists from combinations of previous results. So we have the equation

a(n) = a(n-1) + some_binomial_function

So let us determine what this binomial function turns out to be. Remembering Pascal’s rule of binomial(n-1,k)+binomial(n-1,k-1)=binomial(n,k) allows us to reduce the original definition into the following, with b for binomial.

a(n) = b(2(n-1),n-1) + b(2(n-1),n-2) + b(2(n-1),n-1) + b(2(n-1),n)
–b(2(n-1),n-3) - b(2(n-1),n-2)- b(2(n-1),n-2) - b(2(n-1),n-1)

And remembering the b(n,r)=b(n,n-r) gives us the following reduction.

a(n) = binomial(2(n-1), n-1) – binomial(2(n-1),n-3)

So now we found part of an a(n-1), thus we can find our some_binomial_function from

a(n) = binomial(2(n-1), n-1) –binomial(2(n-1),n-2) + some_binomial_function

some_binomial_functions = binomial(2(n-1),n-2) – binomial(2(n-1),n-3)

So we can see that the first part of the binomial function cancels out with the last part of the a(n-1) function, leaving only the final part as a subtraction. Thinking about what this "some_binomial_function" means, we can see that we take the substrings that we can add together to get a bigger substring, minus the number of invalid and duplicate substrings. This gives us the final version that computes our Qi functions output length.

a(n) = a(n-1) + binomial(2(n-1),n-2) – binomial(2(n-1),n-3)

Of course, we can make more optimizations and go further into the Catalan numbers, which I may do in the future. For now, I hope this serves as a fun introduction to Qi optimization and the always interesting Catalan sequence. Let me know what you think!

Building Lisp, Qi and other Fun Hacks

2006-04-29T10:31:00.000-07:00

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.
1. Makes a "qi" package
2. Loads the qi.lisp file and compiles it into memory.
3. 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

2006-04-27T01:00:00.000-07:00

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!

Qi Programming Basics: Pattern Matching

2006-04-23T00:20:00.000-07:00

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

Qi and the "Magic" Prime Type

2006-04-21T06:23:00.000-07:00

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

Welcome to Programming Kung Fu Qi

2006-04-21T05:44:00.000-07:00

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/Qilang

Enjoy!