Computing During Typing
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,
posted by EntropyFails @ 1:18 AM
