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.
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.
Just a note:
You can get the new version of Qi at the
Google Qi page.You can also download the
Win32 Installer. Enjoy!
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!
\
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!
\
Labels: qi
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.
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/listbut 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...
