A SK Combinator in the Qi Type System, a Comparison with Haskell
\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.
\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.
(datatype sk
___
Bot : s0;
___
Bot : k0;
___
Bot : (app A B);
___
Bot : (other A);
\
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.
\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 : (combine_done done done done);
___
Bot : (combine_done done more more);
___
Bot : (combine_done more done more);
___
Bot : (combine_done more more more);
\
\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).
____
Bot : (sk_eval s0 s0 done);
___
Bot : (sk_eval k0 k0 done);
___
Bot : (sk_eval (other A) (other A) done);
\
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."
\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 k0 X) (app k0 Xp) D);
Bot : (sk_eval X Xp D);
___
Bot : (sk_eval (app s0 X) (app s0 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 D);
___
Bot : (sk_eval (app (other A) X) (app (other A) Xp) 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 : (combine_done D1 D2 D);
___
Bot : (sk_eval (app (app (other A) X) Y)
(app (app (other A) Xp) Yp) 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 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);
\
\
___
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.
\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 (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);
\
\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 X done);
Bot : (sk_eval X Y Q);
Bot : (sk_eval_aux Y Z Q);
___
Bot : (sk_eval_aux X Z more);
\
\
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
0 Comments:
