Advanced Types in Qi

	The Power of Qi

Since Qi 6.1 was placed online, a number of correspondents on Usenet have been studying the Qi type theory. Much interest and controversy has been generated by the claim that the type system of Qi is the most powerful of its kind and more powerful than Haskell and ML. I have not personally contributed much to these discussions.

My experience of unmoderated groups has taught me that they are useful in reaching a wider audience, but not so helpful in exploring complex issues generated by new paradigms. But I now see there is a group of people who are genuinely interested in the type system of Qi but cannot see why the sequent calculus approach should be any better or more powerful than that of ML or Haskell. It is for these people that this page is written.

Why is Qi so Powerful?

I claimed controversially that the type system of Qi is the most powerful of its kind and more powerful than Haskell and ML. This caused some heat in certain quarters. I will raise the heat further by this addition.

Qi has the most powerful type theory of any language that will ever be invented.

A strong claim? Possibly, but nevertheless accurate. To understand why, we need to probe into the architecture of Qi.

What makes Qi a practical system for type-secure programming, is the compiler from sequent calculus notation into CLisp byte code. If we raise the bonnet of Qi and look into the engine it looks like this.

Since Qi is bootstrapped, this engine is written in Qi. The power and performance of the compiler makes possible the practical use of sequent calculus to define types. However there is something important in this picture. What is important here is that the sequent calculus notation that Qi uses is itself a programming language; Qi Prolog is an enriched Prolog that includes executable functional expressions. This means that the language for types in Qi is Turing-equivalent. This is not true of ML for example. The notation for defining types in ML is essentially that of a context-free BNF grammar. So the claim that Qi is more powerful in defining types than ML or Haskell is not hyperbole. It is fact. And the claim that Qi has the most powerful type theory of any language that will ever be invented is fact too, because Turing equivalence is the end of the line.

Is Qi Better than ML and Haskell?

This is not a scientific question, though people will argue it. The equation powerful = better seems fixed in people's minds. There are advantages in having a weak notation for types. One advantage is that type checking in ML is guaranteed to terminate. It is guaranteed to terminate in Qi too, provided that the user does not add non-terminating type rules. But in Qi you can send the type checker in a loop or collapse the type system completely by the wrong rule. Chapter 13 in FPQi gives some examples of this. It is the inevitable by-product of using a Turing-equivalent notation.

There is probably some mileage in looking at type notations which restrict the full power of Qi's sequent calculus; for example which try to enforce termination by requiring a subformula property or something similar. Qi is open source, so you can experiment with this.

What Sorts of Type Theories Can I Define in Qi?

Anything you can execute; and a few things you can't (though there is not much point in this). Lets look at an example. This example can be developed in depth. I hope that it will stimulate you to think and experiment.

Case Study: The Type Theory of Interval Arithmetic

Interval arithmetic was invented over 40 years ago by Ramon Moore to deal with computations which (e.g.) involve computing with quantities which may contain observational inaccuracies. In such a case we might know that the observational inaccuracy is plus or minus a certain quantity. Therefore the inputs to our computation can be represented as intervals and the arithmetic operations on intervals constitute interval arithmetic. Here is an early paper giving some equations for the four basic arithmetical operations in interval arithmetic. We will use one of these equations in what follows.

We might be interested in using interval arithmetic in a program for placing a satellite in orbit, given inexact inputs regarding payload, fuel, air resistance etc. We want to know that the program will not put the satellite into outer space or place it too low and see it burn. We need to provethat given inputs of a certain interval, that the output will fall in a certain interval too. One way of doing this is to get the type checker to prove that the program will always obey these constraints. But in order to do this, we have to program the type checker with the type theory of interval arithmetic.

Now actually there are two general models for developing the type theory of interval arithmetic; explicit interval arithmetic and implicit interval arithmetic. In explicit interval arithmetic, we use intervals as objects of computation. In implicit interval arithmetic, we just use numbers, but we use the theory of interval arithmetic in the type checker. One reason interval arithmetic is not popular is that standard arithmetical libraries are geared up to work with numbers and not intervals. But this objection does not apply if we use implicit interval arithmetic, because the intervals are not used in the computation itself. Lets see how to do this in Qi.

We can write the basic rule for implicit interval arithmetic in Qi exactly like this.

(datatype interval

if (number? N)
if (number? A)
if (number? B)
if (>= B A)
if (>= N A)
if (>= B N)
___________
N : (interval A B); )

Here an interval type is inhabited by a transfinite number of numbers corresponding to all the reals in the interval.

_______________________________________________________________________

Test 1.

(0-) (datatype interval

if (number? N)
if (number? A)
if (number? B)
if (>= B A)
if (>= N A)
if (>= B N)
_______________
N : (interval A B); )
interval

(1-) (tc +)
true

(2+) 3 : (interval 1 7)
3 : (interval 1 7)

(3+) 6 : (interval 7 9)
error: type error
_______________________________________________________________________

We add the rule for computing when the sum of two numbers falls in an interval

M : (interval C D);
N : (interval E F);
(= A (+ C E)) : boolean;
(= B (+ D F)) : boolean;
(= A (+ C E));
(= B (+ D F));
____________________
(+ M N) : (interval A B);

This rule is based directly on the rule for adding intervals. It basically says here that the sum of M and N falls into the interval which is the sum of the intervals to which M and N belong. Suppose we enter a function using interval sums into the computer having entered these type rules.

(define raise1
{(interval 10000 20000) --> (interval 1000 20000) --> (interval 11000 40000)}
N Raise -> (+ N Raise))

It fails because we need a rule that allows the computer to solve the equations (= A (+ C E)) and (= B (+ D F)).

Here it is

if (= A (+ B C))
____________
(= A (+ B C));

which says that if B + C does compute to A then you can consider (= A (+ B C)) as proved.

This does type check.

_______________________________________________________________________

Test 2.

(4+) (datatype interval

if (number? N)
if (number? A)
if (number? B)
if (>= B A)
if (>= N A)
if (>= B N)
_______________
N : (interval A B);

M : (interval C D);
N : (interval E F);
(= A (+ C E)) : boolean;
(= B (+ D F)) : boolean;
(= A (+ C E));
(= B (+ D F));
____________________
(+ M N) : (interval A B);

if (= A (+ B C))
____________
(= A (+ B C));)
======> Warning: redefining interval can cause type errors.
interval : unit

(5+) (define raise1
{(interval 10000 20000) --> (interval 1000 20000) --> (interval 11000 40000)}
N Raise -> (+ N Raise))
raise1 : ((interval 10000 20000) --> ((interval 1000 20000) --> (interval 11000 40000)))

_______________________________________________________________________

Interval Polytypes

Now what if we want to generalise raise1 by replacing numbers with variables?

(define raise2
{(interval A B) --> (interval C D) --> (interval (+ A C) (+ B D))}
N Raise -> (+ N Raise))

This does not type check. It fails because the computer cannot prove (= A (+ C E)) : boolean; and (= B (+ D F)) : boolean; in

   M : (interval C D);
   N : (interval E F);
   (= A (+ C E)) : boolean;
   (= B (+ D F)) : boolean;
   (= A (+ C E));
   (= B (+ D F));
   ____________________
   (+ M N) : (interval A B);

Why? Because the positions are now held by algebraic terms and not numbers. We need an extra rule to allow it to infer that these terms are numbers.

N : number, A : number, B : number >> P;
___________________________________
N : (interval A B) >> P;

This just says if we have N : (interval A B) as an assumption and we are trying to prove P then we can assume N, A and B are all numbers instead and try to prove P.

Can we type check raise2? No, we still get a type error. Why? Well, suppose we switch on spy to observe the type checker. Here is a chunk from the script.

______________________________________________ 2416 inferences
?- (= (+ type205 type207) ((+ type205) type207)) : boolean

Raise : (interval type207 type208)
N : (interval type205 type206)

>
______________________________________________ 2441 inferences
?- (+ type205 type207) : V16516

Raise : (interval type207 type208)
N : (interval type205 type206)

>

The problem is that we are using + both to the left and the right of the :. To the left it is curried automatically by Qi because Qi curries everything to the left of the : as part of a function expression. To the right it is not, because it is part of a type. This is not hard to fix, but we'll take the lazy way and just choose to write + in curried form in the type. I leave it as an exercise for you to devise a more user-friendly solution.

(datatype interval

if (number? N)
if (number? A)
if (number? B)
if (>= B A)
if (>= N A)
if (>= B N)
_______________
N : (interval A B);

M : (interval C D);
N : (interval E F);
(= A ((+ C) E)) : boolean;
(= B ((+ D) F)) : boolean;
(= A ((+ C) E));
(= B ((+ D) F));
____________________
(+ M N) : (interval A B);

if (= A ((+ B) C))
____________
(= A ((+ B) C));

N : number, A : number, B : number >> P;
___________________________________
N : (interval A B) >> P;)

(define raise2
{(interval A B) --> (interval C D) --> (interval ((+ A) C) ((+ B) D))}
N Raise -> (+ N Raise))

Now we get a new error.

(19+) (define raise2
{(interval A B) --> (interval C D) --> (interval ((+ A) C) ((+ B) D))}
N Raise -> (+ N Raise))
+: type221 is not a NUMBER

The problem is the rule

if (= A ((+ B) C))
____________
(= A ((+ B) C));

The equation contains algebraic terms and the computer tries to prove the identity by summing the terms. But the terms are not numbers now, but algebraic variables which cannot be summed by the evaluator.

The solution to this final problem is symbolic evaluation. The computer is given an algebraic identity of the form a = a, which it should evaluate to true. Using symbolic evaluation, the computer can prove that raise2 is type secure. The correct rule is:

if (symeval [= A B])
____________
(= A B);

where symeval is the symbolic evaluator. Note we use square brackets in the side condition to show we are dealing with a list structure, not trying to perform addition.

What of the code for the symbolic evaluator? A really good symbolic evaluator is not a trivial task (the whole of the Boyer-Moore can be looked upon as a symbolic evaluator for Lisp). You must imagine something portentious. If your imagination fails, then write the code. Here is what is needed to get raise2 past the type checker.

(define symeval
[= X X] -> true
_ -> false)

Putting It All Together

OK; lets draw all this scattered code together and put all the rules in one place.

_______________________________________________________________________

Test 3.

(34+) (datatype interval

if (number? N)
if (number? A)
if (number? B)
if (>= B A)
if (>= N A)
if (>= B N)
_______________
N : (interval A B);

M : (interval C D);
N : (interval E F);
(= A ((+ C) E)) : boolean;
(= B ((+ D) F)) : boolean;
(= A ((+ C) E));
(= B ((+ D) F));
____________________
(+ M N) : (interval A B);

if (symeval [= A B])
_________________
(= A B);

N : number, A : number, B : number >> P;
___________________________________
N : (interval A B) >> P;)
======> Warning: redefining interval can cause type errors.
interval : unit

(35+) \Switch off the type checker to sneak in my symbolic evaluator.\ (tc -)
false

(36-) \Very idle version of symbolic evaluation, sans types.\
(define symeval
[= X X] -> true
_ -> false)
symeval

(37-) \Switch on the type checker to see if it all works.\ (tc +)
true

(38+) (define raise2
{(interval A B) --> (interval C D) --> (interval ((+ A) C) ((+ B) D))}
N Raise -> (+ N Raise))
raise2 : ((interval A C) --> ((interval B D) --> (interval ((+ A) B) ((+ C) D))))

_______________________________________________________________________

Success at last! But two things are now wrong. First raise1 will not type check any more and (raise2 12 13) records a type error. raise1 does not type check because our symbolic evaluator is too puny. OK, lets beef it up.

(define symeval
[= X Y] -> (= (symeval X) (symeval Y))
[[+ X] Y] -> (+ X Y) where (and (number? X) (number? Y))
X -> X)

Not brilliant, but it will resurrect raise1. (raise2 12 13) fails because the type checker cannot place 12 or 13 in an arbitrary interval. Ok here is the default case. Every number belongs in the interval which comprises only itself.

if (number? N)
____________
N : (interval N N);

Now we try (raise2 12 13)

(44+) (raise2 12 13)
25 : (interval ((+ 12) 13) ((+ 12) 13))

Not exciting, but definitely true.

_______________________________________________________________________

Pythagoras's Theorem

Can we do anything more interesting than add numbers together in interval type theory? Well that's for you to explore, because the purpose of this page is not to argue for interval type theory, but for you to understand what Qi can do in helping you to explore type theory. Here is a problem you might like to think on.

The right-angled triangle ABC has sides A and B and hypotenuse C. If side A has the length 3' and side B has the length 2' does hypotenuse C have the length 4' (+/- .5')?

What we want to be able to do is write something like (hyp 3 2) : (interval 3.5 4.5) and get an answer or a type error. Sorry I cannot spend more time on Usenet. But this should be enough to start your experiments.

Happy hacking

Mark